have h_pl_div_ml : p^l ∣ m^l := by
  exact pow_dvd_pow_of_dvd (Nat.Prime.dvd_of_dvd_pow (h_p) (h_p_div_ml)) l
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
⊢ p ^ l ∣ n.descFactorial k
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
⊢ p ^ l ∣ n.descFactorial k