rcases inv_succ_le_all ε ε_pos with ⟨N, hN⟩
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |u n - x| ≤ ε
case intro
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
⊢ ∃ N, ∀ n ≥ N, |u n - x| ≤ ε