proposition: Lemma ex_series_scal_r (c : R) (a : nat -> R) : ex_series a -> ex_series (fun n => a n * c).
proof: Proof. intros [l Ha]. exists (l * c). by apply is_series_scal_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy