proposition: Lemma RInt_gen_pos {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 -> 0 <= f z) -> filter_prod Fa Fb (fun ab : R * R => ab.1 <= ab.2) -> is_RInt_gen f Fa Fb If -> 0 <= If.
proof: Proof. move => HFa HFb Hfx Hle Hint. have -> : 0 = norm 0 by rewrite norm_zero. apply: (RInt_gen_norm (fun _ => 0) f 0 If _ _ _ Hint) => // . apply: (Filter_prod _ _ _ P Q HFa HFb) => x y HPx HQy x0 /= Hx0. rewrite norm_zero; apply: (Hfx _ _ _ HPx HQy) => // . exact: is_RInt_gen_0. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl