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