have h_pl_div_fac : p^l ∣  (n.factorial / (k.factorial * (n-k).factorial)) := by
  rw [← Nat.choose_eq_factorial_div_factorial h_klen]
  exact h_pl_div_binom
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
⊢ 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)
⊢ p ^ l ∣ n.descFactorial k