proposition: Lemma PSeries_ext (a b : nat -> R) (x : R) : (forall n, a n = b n) -> PSeries a x = PSeries b x.
proof: Proof. move => Heq. apply Series_ext. move => n ; by rewrite Heq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series