specialize hN n hn
case h
u : ℕ → ℝ
x ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
n : ℕ
hn : n ≥ N
h : |u n - x| ≤ 1 / (↑n + 1)
⊢ |u n - x| ≤ ε
case h
u : ℕ → ℝ
x ε : ℝ
ε_pos : ε > 0
N n : ℕ
hn : n ≥ N
h : |u n - x| ≤ 1 / (↑n + 1)
hN : 1 / (↑n + 1) ≤ ε
⊢ |u n - x| ≤ ε