cases' em (n ≥ 2*k) with h_2k h
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
⊢ n.choose k ≠ m ^ l
case inl
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h_2k : n ≥ 2 * k
⊢ n.choose k ≠ m ^ l

case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : ¬n ≥ 2 * k
⊢ n.choose k ≠ m ^ l