apply le_max_right
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ N ≥ Nb
no goals