ring
case e_a
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
ngeNs : n ≥ Ns
ngeNt : n ≥ Nt
⊢ s n + t n - (a + b) = s n - a + (t n - b)
no goals