proposition: Lemma ex_pseries_scal (c : K) (a : nat -> V) (x : K) : mult x c = mult c x -> ex_pseries a x -> ex_pseries (PS_scal c a) x.
proof: Proof. move => Hx [l Ha]. exists (scal c l). by apply is_pseries_scal. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series