rcases cs (ε / 2) ε2pos with ⟨Ns, hs⟩
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
case intro
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε