intro n hn
case h
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
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
⊢ ∀ n ≥ max Ns Nt, |s n + t n - (a + b)| < ε
case h
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
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
⊢ |s n + t n - (a + b)| < ε