lean_workbook_plus_67809
OpenThe sum of this from to is equal to 1 since must occur in one of those positions. So
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_67809 (n : ℕ) : ∑ k in Finset.Icc 3 51, (Nat.choose k 3 * Nat.choose (52 - k) 1) = Nat.choose 53 5 := by sorry
Source