have ε2pos : 0 < ε / 2 := by linarith
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
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)| < ε