proposition: Lemma PSeries_eq (a : nat -> R) (x : R) : PSeries a x = Series (fun k => scal (pow_n x k) (a k)).
proof: Proof. apply Series_ext. intros n. apply Rmult_comm. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series