proposition: Lemma ex_pseries_dec {V : NormedModule R_AbsRing} (a : nat -> R) (x : R) : {ex_pseries a x} + {~ ex_pseries a x}.
proof: Proof. apply ex_series_dec. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series