calc
  |s n| = |s n - a + a| := by
    congr
    abel
  _ ≤ |s n - a| + |a| := (abs_add _ _)
  _ < |a| + 1 := by linarith [h n ngt]
case h
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
n : ℕ
ngt : N ≤ n
⊢ |s n| < |a| + 1
no goals