calc |l - l'| = |(l-u (max N N')) + (u (max N N') -l')| := by ring_nf
_ ≤ |l - u (max N N')| + |u (max N N') - l'| := by apply abs_add
_ = |u (max N N') - l| + |u (max N N') - l'| := by rw [abs_sub_comm]
_ ≤ ε/2 + ε/2 := by linarith
_ = ε := by ring
case a.intro.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε
no goals