proposition: Lemma RInt_gen_le {Fa Fb : (R -> Prop) -> Prop} {FFa : ProperFilter Fa} {FFb : ProperFilter Fb} (f : R -> R) (g : R -> R) (lf : R) (lg : R) : filter_prod Fa Fb (fun ab => fst ab <= snd ab) -> filter_prod Fa Fb (fun ab => forall x, fst ab <= x <= snd ab -> f x <= g x) -> is_RInt_gen f Fa Fb lf -> is_RInt_gen g Fa Fb lg -> lf <= lg.
proof: Proof. move => Hab Hle. move => Hlf Hlg. apply (filterlim_le (F := filter_prod Fa Fb) (fun x => RInt f x.1 x.2) (fun x => RInt g x.1 x.2) lf lg). apply: (filter_imp (fun x => ex_RInt f x.1 x.2 /\ ex_RInt g x.1 x.2 /\ (forall y, x.1 <= y <= x.2 -> f y <= g y) /\ x.1 <= x.2)). move => x [H1 [H2 [H3 H4]]]. apply: RInt_le => // . move => x0 Hx0. have:= H3 x0. apply. by split; now apply Rlt_le. apply: filter_and. apply: ex_RInt_ex_RInt_gen. now exists lf. apply: filter_and. apply: ex_RInt_ex_RInt_gen. now exists lg. apply: filter_and => // . exact: is_RInt_gen_filterlim. exact: is_RInt_gen_filterlim. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl