simpa only [add_comm x y]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inr.inl
n : ℕ
hn : 100 ≤ n
a : ℕ
hna : n ≤ a
x y : ℕ
hxy : x ≠ y
hcn : x ≤ 2 * n
h₂ : ∃ l, x + a = l ^ 2
hab : a < y
h₁ : ∃ k, a + y = k ^ 2
hbc : y < x
h₃ : ∃ m, y + x = m ^ 2
⊢ ∃ k, x + y = k ^ 2
no goals