thm_1_2_n_n_1_1_n_2
Proved1-2-n-n-1-1-n-2proofwikiretrysquare-numberssums-of-sequences
A sum identity involving n^2.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem thm_1_2_n_n_1_1_n_2 (n : ℕ) : (Finset.range n).sum (fun i => (i + 1)) + (Finset.range (n - 1)).sum (fun i => (n - 1 - i)) = n ^ 2 := by sorry