set l := (n + 1).sqrt - 1
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
h₁ : ((n + 1).sqrt - 1 + 1) ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ ((n + 1).sqrt - 1 + 1 + 1) ^ 2
h₃ : 10 ≤ (n + 1).sqrt - 1 + 1
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
l : ℕ := (n + 1).sqrt - 1
h₁ : (l + 1) ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ (l + 1 + 1) ^ 2
h₃ : 10 ≤ l + 1
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n