proposition: Lemma RInt_gen_neg {Fa : (R -> Prop) -> Prop} {FFa : ProperFilter Fa} {Fb : (R -> Prop) -> Prop} {FFb : ProperFilter Fb} (P Q : R -> Prop) (f : R -> R) (If : R) : (Fa P) -> (Fb Q) -> (forall x y z, P x -> Q y -> x <= z <= y -> f z <= 0) -> filter_prod Fa Fb (fun ab : R * R => ab.1 <= ab.2) -> is_RInt_gen f Fa Fb If -> If <= 0.
proof: Proof. move => HFa HFb Hfx Hle Hint. apply is_RInt_gen_opp in Hint. suff: 0 <= opp If. by rewrite /opp /=; lra. apply: (@RInt_gen_pos Fa FFa Fb FFb P Q (fun x => opp (f x)) (opp If)) => // . move => x y z HPx HQy Hxzy; move: (Hfx x y z HPx HQy Hxzy). by rewrite /opp /=; lra. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl