n k : ℕ
⊢ k ! * choose n k = k ! * (descFactorial n k / k !)
n k : ℕ
⊢ choose n k = descFactorial n k / k !
apply mul_left_cancel₀ (factorial_ne_zero k)
n k : ℕ
⊢ descFactorial n k = k ! * (descFactorial n k / k !)
n k : ℕ
⊢ k ! * choose n k = k ! * (descFactorial n k / k !)
rw [← descFactorial_eq_factorial_mul_choose]
no goals
n k : ℕ
⊢ descFactorial n k = k ! * (descFactorial n k / k !)
exact (Nat.mul_div_cancel' <| factorial_dvd_descFactorial _ _).symm