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