choose_succ_right_eq — Mathlib

English

For all n,k: (nC(k+1)) (k+1) = (nCk) (n-k).

Русский

Для любых n,k: C(n,k+1) (k+1) = C(n,k) (n-k).

LaTeX

$$$\\\\binom{n}{k+1} (k+1) = \\\\binom{n}{k} (n - k)$$$

Lean4

theorem choose_succ_right_eq (n k : ℕ) : choose n (k + 1) * (k + 1) = choose n k * (n - k) :=
  by
  have e : (n + 1) * choose n k = choose n (k + 1) * (k + 1) + choose n k * (k + 1) := by
    rw [← Nat.add_mul, Nat.add_comm (choose _ _), ← choose_succ_succ, succ_mul_choose_eq]
  rw [← Nat.sub_eq_of_eq_add e, Nat.mul_comm, ← Nat.mul_sub_left_distrib, Nat.add_sub_add_right]

Похожие утверждения