apply aux cs
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ ConvergesTo (fun n => s n * (t n + -b)) 0
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ ConvergesTo (fun n => t n + -b) 0