have h₂ : 1 ≤ 2 * l := by omega
case intro.intro
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
⊢ ∃ a b c, n ≤ a ∧ a < b ∧ b < c ∧ c ≤ 2 * n ∧ (∃ k, a + b = k ^ 2) ∧ (∃ l, c + a = l ^ 2) ∧ ∃ m, b + c = m ^ 2
case intro.intro
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
⊢ ∃ a b c, n ≤ a ∧ a < b ∧ b < c ∧ c ≤ 2 * n ∧ (∃ k, a + b = k ^ 2) ∧ (∃ l, c + a = l ^ 2) ∧ ∃ m, b + c = m ^ 2