proposition: Lemma Series_scal_r (c : R) (a : nat -> R) : Series (fun n => a n * c) = Series a * c.
proof: Proof. rewrite Rmult_comm -Series_scal_l. apply Series_ext. move => n ; apply Rmult_comm. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy