intro n ngt
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 ≥ Ns, |c * s n - c * a| < ε
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| < ε