linarith
case intro.intro.refine_7
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * ↑l ^ 2 + 1 + (2 * ↑l ^ 2 + 4 * ↑l) = (2 * ↑l + 1) ^ 2
no goals