apply abs_add
u : ℕ → ℝ
l l' ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - u (max N N') + (u (max N N') - l')| ≤ |l - u (max N N')| + |u (max N N') - l'|
no goals