simp [h_k'_def]
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
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
⊢ k' ≤ n - 4
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
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
⊢ n ≤ n - 4 + k