intro ε₀ hε₀
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
⊢ f + g ≈ f' + g'
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
⊢ ∃ N, ∀ (m : ℕ), m ≥ N → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀