lean_workbook_plus_11632
ProvedProve that for all integers .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_11632 (n : ℕ) (h : n ≥ 2) : (n + 1).choose 2 = n * (n + 1) / 2 := by sorry
Source
Prove that for all integers .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_11632 (n : ℕ) (h : n ≥ 2) : (n + 1).choose 2 = n * (n + 1) / 2 := by sorry