English
For any n,m,k with k ≤ m, the descending factorial satisfies n−k down (m−k) times n↓k equals n↓m; i.e. (n−k)↓(m−k) · n↓k = n↓m.
Русский
Для любых n,m,k с k ≤ m выполняется (n−k)↓(m−k) · n↓k = n↓m.
LaTeX
$$(n - k) descFactorial (m - k) * n descFactorial k = n descFactorial m \\\\ (k ≤ m)$$
Lean4
theorem descFactorial_mul_descFactorial {k m n : ℕ} (hkm : k ≤ m) :
(n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m :=
by
by_cases hmn : m ≤ n
· apply Nat.mul_left_cancel (n - m).factorial_pos
rw [factorial_mul_descFactorial hmn, show n - m = (n - k) - (m - k) by cutsat, ← Nat.mul_assoc,
factorial_mul_descFactorial (show m - k ≤ n - k by cutsat), factorial_mul_descFactorial (le_trans hkm hmn)]
· rw [descFactorial_eq_zero_iff_lt.mpr (show n < m by cutsat)]
by_cases hkn : k ≤ n
· rw [descFactorial_eq_zero_iff_lt.mpr (show n - k < m - k by cutsat), Nat.zero_mul]
· rw [descFactorial_eq_zero_iff_lt.mpr (show n < k by cutsat), Nat.mul_zero]
