proposition: Lemma RInt_le (f g : R -> R) (a b : R) : a <= b -> ex_RInt f a b -> ex_RInt g a b-> (forall x, a < x < b -> f x <= g x) -> RInt f a b <= RInt g a b.
proof: Proof. intros Hab Hf Hg Hfg. apply: is_RInt_le Hab _ _ Hfg. exact: RInt_correct. exact: RInt_correct. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy