proposition: Lemma ex_pseries_0 (a : nat -> V) : ex_pseries a zero.
proof: Proof. exists (a O) ; by apply is_pseries_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series