proposition: Lemma ex_RInt_locally {V : CompleteNormedModule R_AbsRing} (f : R -> V) (a b : R) : ex_RInt f a b -> (exists eps : posreal, ex_RInt f (a - eps) (a + eps)) -> (exists eps : posreal, ex_RInt f (b - eps) (b + eps)) -> locally (a,b) (fun z : R * R => ex_RInt f (fst z) (snd z)).
proof: Proof. intros Hf (ea,Hea) (eb,Heb). exists (mkposreal _ (Rmin_stable_in_posreal ea eb)) => [[a' b'] [Ha' Hb']] ; simpl in *. apply ex_RInt_Chasles with (a - ea). eapply ex_RInt_swap, ex_RInt_Chasles_1 ; try eassumption. apply Rabs_le_between'. eapply Rlt_le, Rlt_le_trans, Rmin_l. by apply Ha'. apply ex_RInt_Chasles with a. eapply ex_RInt_Chasles_1 ; try eassumption. apply Rabs_le_between'. rewrite Rminus_eq_0 Rabs_R0. by apply Rlt_le, ea. apply ex_RInt_Chasles with b => //. apply ex_RInt_Chasles with (b - eb). eapply ex_RInt_swap, ex_RInt_Chasles_1; try eassumption. apply Rabs_le_between'. rewrite Rminus_eq_0 Rabs_R0. by apply Rlt_le, eb. eapply ex_RInt_Chasles_1 ; try eassumption. apply Rabs_le_between'. eapply Rlt_le, Rlt_le_trans, Rmin_r. by apply Hb'. 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