n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ choose n k * (k ! * (n - k)!)
n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n !
rw [← choose_mul_factorial_mul_factorial hk, mul_assoc]
no goals
n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ choose n k * (k ! * (n - k)!)
exact dvd_mul_left _ _