have h₁ : ConvergesTo (fun n ↦ s n * (t n + -b)) 0 := by
  apply aux cs
  convert convergesTo_add ct (convergesTo_const (-b))
  ring
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ 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
⊢ ConvergesTo (fun n => s n * t n) (a * b)