exact ⟨⟨hab.ne, (hab.trans hbc).ne⟩, hbc.ne⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
n : ℕ
hn : 100 ≤ n
a b c : ℕ
hna : n ≤ a
hab : a < b
hbc : b < c
hcn : c ≤ 2 * n
h₁ : ∃ k, a + b = k ^ 2
h₂ : ∃ l, c + a = l ^ 2
h₃ : ∃ m, b + c = m ^ 2
⊢ (a ≠ b ∧ a ≠ c) ∧ b ≠ c
no goals