Pascals_Rule
Provedbinomial-coefficientspascal-s-ruleproofwiki
For positive integers n, k with 1 ≤ k ≤ n: C(n, k-1) + C(n, k) = C(n+1, k)
Preamble
import Mathlib.Data.Nat.Choose.Basic
Formal statement
theorem Pascals_Rule (n k : ℕ) (hk1 : 1 ≤ k) (hk2 : k ≤ n) : Nat.choose n (k - 1) + Nat.choose n k = Nat.choose (n + 1) k := by sorry
Source