English
For any r and k, multichoose (r+1) (k+1) equals the sum of multichoose r (k+1) and multichoose (r+1) k; i.e., the standard binomial-type recurrence holds.
Русский
Для любых r и k выполняется равенство multichoose (r+1) (k+1) = multichoose r (k+1) + multichoose (r+1) k и т.д.
LaTeX
$$$multichoose (r+1) (k+1) = multichoose r (k+1) + multichoose (r+1) k$$$
Lean4
theorem multichoose_succ_succ (r : R) (k : ℕ) :
multichoose (r + 1) (k + 1) = multichoose r (k + 1) + multichoose (r + 1) k :=
by
rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1))]
simp only [factorial_nsmul_multichoose_eq_ascPochhammer, smul_add]
rw [add_comm (smeval (ascPochhammer ℕ (k + 1)) r), ascPochhammer_succ_succ r k]
