n k : ℕ
h : k ≤ n
⊢ (n - k)! * descFactorial n k = (n - k)! * (n ! / (n - k)!)
n k : ℕ
h : k ≤ n
⊢ descFactorial n k = n ! / (n - k)!
apply mul_left_cancel₀ (factorial_ne_zero (n - k))
n k : ℕ
h : k ≤ n
⊢ n ! = (n - k)! * (n ! / (n - k)!)
n k : ℕ
h : k ≤ n
⊢ (n - k)! * descFactorial n k = (n - k)! * (n ! / (n - k)!)
rw [factorial_mul_descFactorial h]
no goals
n k : ℕ
h : k ≤ n
⊢ n ! = (n - k)! * (n ! / (n - k)!)
exact (Nat.mul_div_cancel' <| factorial_dvd_factorial <| Nat.sub_le n k).symm