theorem
proved
term proof
current_chain_partition
show as:
view Lean formalization →
formal statement (Lean)
132theorem current_chain_partition :
133 13 + 2*11 + 2*6 + 8 = 55 := by norm_num
proof body
Term-mode proof.
134
135/-- The current chain has middle pair summing to W. -/