English
A Pascal-type identity holds: choose (r+1) (k+1) equals choose r k plus choose r (k+1).
Русский
Паскальево-типовая идентичность: choose (r+1) (k+1) = choose r k + choose r (k+1).
LaTeX
$$$ \forall R\ [NonAssocRing\ R]\ [Pow\ R\ Nat]\ [BinomialRing\ R]\ (r: R)\ (k:\mathbb{N}),\ \mathrm{choose}(r+1)(k+1) = \mathrm{choose} r k + \mathrm{choose} r (k+1)$$$
Lean4
theorem choose_succ_succ [NatPowAssoc R] (r : R) (k : ℕ) : choose (r + 1) (k + 1) = choose r k + choose r (k + 1) :=
by
rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1))]
simp only [smul_add, ← descPochhammer_eq_factorial_smul_choose]
rw [Nat.factorial_succ, mul_smul, ← descPochhammer_eq_factorial_smul_choose r, descPochhammer_succ_succ_smeval r k]
