have h_ilk : i < k := by
  have hk : 0 < k := lt_of_lt_of_le four_pos h_4lek
  zify at hi_left
  zify
  norm_cast at hi_left ⊢
  exact Iff.mpr (lt_iff_le_pred hk) hi_left
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
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
⊢ i < n
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
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
h_ilk : i < k
⊢ i < n