proposition: Lemma PSeries_1 (a : nat -> R) : PSeries a 1 = Series a.
proof: Proof. apply Series_ext => n. by rewrite pow1 Rmult_1_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series