proposition: Lemma PSeries_scal (c : R) (a : nat -> R) (x : R) : PSeries (PS_scal c a) x = c * PSeries a x.
proof: Proof. rewrite -Series_scal_l. apply Series_ext. move => n /=. apply Rmult_assoc. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series