proposition: Lemma RInt_PSeries (a : nat -> R) (x : R) : Rbar_lt (Rabs x) (CV_radius a) -> RInt (PSeries a) 0 x = PSeries (PS_Int a) x.
proof: Proof. move => Hx. apply is_RInt_unique. 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