choose_mul_succ_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem choose_mul_succ_eq (n k : ℕ) : n.choose k * (n + 1) = (n + 1).choose k * (n + 1 - k) := by
  cases k with
  | zero => simp
  | succ k =>
    obtain hk | hk := le_or_gt (k + 1) (n + 1)
    ·
      rw [choose_succ_succ, Nat.add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ,
        Nat.mul_sub_left_distrib, Nat.add_sub_cancel' (Nat.mul_le_mul_left _ hk)]
    · rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), Nat.zero_mul, Nat.zero_mul]

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