proposition: Lemma CV_radius_Int (a : nat -> R) : CV_radius (PS_Int a) = CV_radius a.
proof: Proof. rewrite -CV_radius_derive. apply CV_radius_ext. rewrite /PS_derive /PS_Int => n ; rewrite S_INR. field. apply Rgt_not_eq, INRp1_pos. 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