English
For all n and k with k ≤ n, the product (n−k)! · n.descFactorial k equals n!, i.e. n! = (n−k)!(n)(n−1)⋯(n−k+1).
Русский
Для всех n,k с k ≤ n имеем (n−k)! · n↓k = n!, то есть n! = (n−k)!(n)(n−1)⋯(n−k+1).
LaTeX
$$$(n-k)! \\cdot n.descFactorial k = n! \\quad (k \\le n)$$$
Lean4
/-- `n.descFactorial k = n! / (n - k)!` but without ℕ-division. See `Nat.descFactorial_eq_div`
for the version using ℕ-division. -/
theorem factorial_mul_descFactorial : ∀ {n k : ℕ}, k ≤ n → (n - k)! * n.descFactorial k = n !
| n, 0 => fun _ => by rw [descFactorial_zero, Nat.mul_one, Nat.sub_zero]
| 0, succ k => fun h => by
exfalso
exact not_succ_le_zero k h
| succ n, succ k => fun h => by
rw [succ_descFactorial_succ, succ_sub_succ, ← Nat.mul_assoc, Nat.mul_comm (n - k)!, Nat.mul_assoc,
factorial_mul_descFactorial (Nat.succ_le_succ_iff.1 h), factorial_succ]
