proposition: Lemma ex_RInt_Chasles_2 {V : CompleteNormedModule R_AbsRing} (f : R -> V) (a b c : R) : a <= b <= c -> ex_RInt f a c -> ex_RInt f b c.
proof: Proof. intros. rewrite -(Ropp_involutive a) -(Ropp_involutive c) in H0. apply ex_RInt_comp_opp in H0. apply ex_RInt_swap in H0. eapply ex_RInt_Chasles_1 in H0. apply ex_RInt_comp_opp in H0. apply ex_RInt_swap in H0. move: H0 ; apply ex_RInt_ext => x _. by rewrite opp_opp Ropp_involutive. split ; apply Ropp_le_contravar ; apply H. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy