proposition: Lemma PSeries_correct (a : nat -> R) (x : R) : ex_pseries a x -> is_pseries a x (PSeries a x).
proof: Proof. move => Ha; rewrite PSeries_eq. apply Series_correct. by apply Ha. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series