rw [abs_le] at hN
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : |u N - x| ≤ ε
ineg : u N ≤ y
⊢ x ≤ y + ε
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : -ε ≤ u N - x ∧ u N - x ≤ ε
ineg : u N ≤ y
⊢ x ≤ y + ε