English
For all n ≥ k ≥ s ≥ 0, C(n,k) C(k,s) = C(n,s) C(n-s, k-s).
Русский
Для всех n ≥ k ≥ s ≥ 0 выполняется C(n,k) C(k,s) = C(n,s) C(n-s, k-s).
LaTeX
$$$\\\\binom{n}{k} \\\\binom{k}{s} = \\\\binom{n}{s} \\\\binom{n-s}{k-s}$$$
Lean4
theorem choose_mul_factorial_mul_factorial : ∀ {n k}, k ≤ n → choose n k * k ! * (n - k)! = n !
| 0, _, hk => by simp [Nat.eq_zero_of_le_zero hk]
| n + 1, 0, _ => by simp
| n + 1, succ k, hk => by
rcases lt_or_eq_of_le hk with hk₁ | hk₁
· have h : choose n k * k.succ ! * (n - k)! = (k + 1) * n ! :=
by
rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)]
simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
have h₁ : (n - k)! = (n - k) * (n - k.succ)! := by
rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
have h₂ : choose n (succ k) * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n ! :=
by
rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]
simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
have h₃ : k * n ! ≤ n * n ! := Nat.mul_le_mul_right _ (le_of_succ_le_succ hk)
rw [choose_succ_succ, Nat.add_mul, Nat.add_mul, succ_sub_succ, h, h₁, h₂, Nat.add_mul, Nat.mul_sub_right_distrib,
factorial_succ, ← Nat.add_sub_assoc h₃, Nat.add_assoc, ← Nat.add_mul, Nat.add_sub_cancel_left, Nat.add_comm]
· rw [hk₁]; simp [Nat.mul_comm, choose, Nat.sub_self]
