linarith
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
⊢ seqOf f m + seqOf g m - (seqOf f' m + seqOf g' m) = seqOf f m - seqOf f' m + (seqOf g m - seqOf g' m)
no goals