apply abs_sub_le
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
⊢ |l - l'| ≤ |l - u (max N N')| + |u (max N N') - l'|
no goals