proposition: Lemma ex_series_scal_l : forall (c : K) (a : nat -> V), ex_series a -> ex_series (fun n => scal c (a n)).
proof: Proof. exact ex_series_scal. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy