have := convergesTo_add h₁ (convergesTo_mul_const b cs)
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
⊢ ConvergesTo (fun n => s n * t n) (a * b)
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
⊢ ConvergesTo (fun n => s n * t n) (a * b)