theorem proved term proof

`sum_of_squares_five`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

1558theorem sum_of_squares_five : (5 : ℕ) = 1^2 + 2^2 := by native_decide

Term-mode proof.

1559
1560/-- 13 = 2² + 3². -/