rcases cs 1 zero_lt_one with ⟨N, h⟩
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
⊢ ∃ N b, ∀ (n : ℕ), N ≤ n → |s n| < b
case intro
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
⊢ ∃ N b, ∀ (n : ℕ), N ≤ n → |s n| < b