have h₂ := Nat.succ_le_succ_sqrt' (n + 1)
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
h₁ : (n + 1).sqrt ^ 2 ≤ n + 1
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
h₁ : (n + 1).sqrt ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ ((n + 1).sqrt + 1) ^ 2
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n