calc
  |c * s n - c * a| = |c| * |s n - a| := by rw [← abs_mul, mul_sub]
  _ < |c| * (ε / |c|) := (mul_lt_mul_of_pos_left (hs n ngt) acpos)
  _ = ε := mul_div_cancel₀ _ (ne_of_lt acpos).symm
case h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / |c|
n : ℕ
ngt : n ≥ Ns
⊢ |c * s n - c * a| < ε
no goals