theorem
other
other
si_partition
show as:
view Lean formalization →
formal statement (Lean)
30theorem si_partition : (7 : ℕ) = 5 + 2 := by decide
proof body
31