English
If k ≤ n and s ≤ k, then C(n,k) C(k,s) = C(n,s) C(n-s, k-s).
Русский
Если k ≤ n и s ≤ k, то 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 {n k s : ℕ} (hkn : k ≤ n) (hsk : s ≤ k) :
n.choose k * k.choose s = n.choose s * (n - s).choose (k - s) :=
have h : 0 < (n - k)! * (k - s)! * s ! := by apply_rules [factorial_pos, Nat.mul_pos]
Nat.mul_right_cancel h <|
calc
n.choose k * k.choose s * ((n - k)! * (k - s)! * s !) = n.choose k * (k.choose s * s ! * (k - s)!) * (n - k)! :=
by
rw [Nat.mul_assoc, Nat.mul_assoc, Nat.mul_assoc, Nat.mul_assoc _ s !, Nat.mul_assoc, Nat.mul_comm (n - k)!,
Nat.mul_comm s !]
_ = n ! := by rw [choose_mul_factorial_mul_factorial hsk, choose_mul_factorial_mul_factorial hkn]
_ = n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) := by
rw [choose_mul_factorial_mul_factorial (Nat.sub_le_sub_right hkn _),
choose_mul_factorial_mul_factorial (hsk.trans hkn)]
_ = n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !) := by
rw [Nat.sub_sub_sub_cancel_right hsk, Nat.mul_assoc, Nat.mul_left_comm s !, Nat.mul_assoc,
Nat.mul_comm (k - s)!, Nat.mul_comm s !, Nat.mul_right_comm, ← Nat.mul_assoc]
