proposition: Lemma RInt_lt (f g : R -> R) (a b : R) : a < b -> (forall x : R, a <= x <= b ->continuous g x) -> (forall x : R, a <= x <= b ->continuous f x) -> (forall x : R, a < x < b -> f x < g x) -> RInt f a b < RInt g a b.
proof: Proof. intros Hab Cg Cf Hfg. apply Rminus_lt_0. assert (Ig : ex_RInt g a b). apply @ex_RInt_continuous. rewrite Rmin_left. rewrite Rmax_right. intros. now apply Cg. by apply Rlt_le. by apply Rlt_le. assert (ex_RInt f a b). apply @ex_RInt_continuous. rewrite Rmin_left. rewrite Rmax_right. intros. now apply Cf. by apply Rlt_le. by apply Rlt_le. rewrite -[Rminus]/(@minus R_AbelianGroup) -RInt_minus //. apply RInt_gt_0 => //. now intros ; apply -> Rminus_lt_0 ; apply Hfg. intros. apply @continuous_minus. by apply Cg. by apply Cf. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy