proposition: Lemma is_pseries_RInt (a : nat -> R) : forall x, Rbar_lt (Rabs x) (CV_radius a) -> is_pseries (PS_Int a) x (RInt (PSeries a) 0 x).
proof: Proof. move => x Hx. erewrite is_RInt_unique. apply PSeries_correct. apply CV_radius_inside. by rewrite CV_radius_Int. exact: 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