intros ε ε_pos
case a
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
⊢ ∀ ε > 0, x ≤ y + ε
case a
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
ε : ℝ
ε_pos : ε > 0
⊢ x ≤ y + ε