proposition: Lemma ex_series_scal (c : K) (a : nat -> V) : ex_series a -> ex_series (fun n => scal c (a n)).
proof: Proof. move => [l Ha]. exists (scal c l). by apply: is_series_scal_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy