proposition: Lemma ex_RInt_PSeries (a : nat -> R) (x : R) : Rbar_lt (Rabs x) (CV_radius a) -> ex_RInt (PSeries a) 0 x.
proof: Proof. move => Hx. exists (PSeries (PS_Int a) x). by apply is_RInt_PSeries. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(eqtype seq) Markov Rcomplements Rbar Lub Lim_seq Derive SF_seq Continuity Hierarchy Seq_fct RInt PSeries