proposition: Lemma ex_RInt_inside {V : CompleteNormedModule R_AbsRing} : forall (f : R -> V) (a b x e : R), ex_RInt f (x-e) (x+e) -> Rabs (a-x) <= e -> Rabs (b-x) <= e -> ex_RInt f a b.
proof: Proof. intros f a b x e Hf Ha Hb. wlog: a b Ha Hb / (a <= b) => [Hw | Hab]. case (Rle_or_lt a b); intros H. now apply Hw. apply ex_RInt_swap. apply Hw; try easy. now left. apply (ex_RInt_Chasles_1 f a b) with (x+e). split. exact Hab. assert (x-e <= b <= x+e) by now apply Rabs_le_between'. apply H. apply ex_RInt_Chasles_2 with (x-e). now apply Rabs_le_between'. exact Hf. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy