lean_workbook_plus_69256
OpenProve the identity:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_69256 (n m : ℕ) : ∑ k in Finset.range (m+1), choose (n + k) k = choose (n + m + 1) m := by sorry
Source
Prove the identity:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_69256 (n m : ℕ) : ∑ k in Finset.range (m+1), choose (n + k) k = choose (n + m + 1) m := by sorry