have h_fac_div : ((↑k ! * ↑(n - k)!) : ℤ)  ∣ (n ! : ℤ) := by
  norm_cast
  exact factorial_mul_factorial_dvd_factorial h_klen
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
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
⊢ 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
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
⊢ p ^ l ∣ n.descFactorial k