proposition: Lemma PSeries_0 (a : nat -> R) : PSeries a 0 = a O.
proof: Proof. rewrite PSeries_eq. apply is_series_unique. apply @is_pseries_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series