by_cases h : c = 0
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
⊢ ConvergesTo (fun n => c * s n) (c * a)
case pos
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
⊢ ConvergesTo (fun n => c * s n) (c * a)

case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
⊢ ConvergesTo (fun n => c * s n) (c * a)