theorem
proved
term proof
current_chain_middle
show as:
view Lean formalization →
formal statement (Lean)
136theorem current_chain_middle : 11 + 6 = 17 := by norm_num
proof body
Term-mode proof.
137
138/-- The current chain has endpoint sum = 21. -/