proposition: Lemma is_RInt_le (f g : R -> R) (a b If Ig : R) : a <= b -> is_RInt f a b If -> is_RInt g a b Ig -> (forall x, a < x < b -> f x <= g x) -> If <= Ig.
proof: Proof. intros Hab Hf Hg Hfg. apply Rminus_le_0. apply: is_RInt_ge_0 Hab _ _. apply: is_RInt_minus Hg Hf. intros x Hx. apply -> Rminus_le_0. apply Hfg, Hx. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy