proposition: Lemma is_series_scal_r (c : R) (a : nat -> R) (l : R) : is_series a l -> is_series (fun n => (a n) * c) (l * c).
proof: Proof. move => Ha. rewrite Rmult_comm. apply is_series_ext with (fun n : nat => c * a n). move => n ; apply Rmult_comm. apply (is_series_scal_l _ _ _ Ha). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy