have h_pl_div_desc: p^l ∣ n.descFactorial k :=
    prime_div_descFactorial n k m l p  h_klen h_p h_p_div_binom H
case h.refine'_1
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
⊢ p ^ l ≤ n
case h.refine'_1
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
⊢ p ^ l ≤ n