n k : ℕ
⊢ n ! * ascFactorial n k = n ! * ((n + k)! / n !)
n k : ℕ
⊢ ascFactorial n k = (n + k)! / n !
apply mul_left_cancel₀ n.factorial_ne_zero
n k : ℕ
⊢ (n + k)! = n ! * ((n + k)! / n !)
n k : ℕ
⊢ n ! * ascFactorial n k = n ! * ((n + k)! / n !)
rw [factorial_mul_ascFactorial]
no goals
n k : ℕ
⊢ (n + k)! = n ! * ((n + k)! / n !)
exact (Nat.mul_div_cancel' <| factorial_dvd_factorial <| le.intro rfl).symm