proposition: Lemma ex_RInt_ex_RInt_gen {V : CompleteNormedModule R_AbsRing} {Fa Fb : (R -> Prop) -> Prop} {FFa : ProperFilter Fa} {FFb : ProperFilter Fb} (f : R -> V) : ex_RInt_gen f Fa Fb -> (filter_prod Fa Fb (fun ab => ex_RInt f ab.1 ab.2)).
proof: Proof. intros [lf Hlf]. have := (Hlf (fun _ => True)). case. now exists (mkposreal _ Rlt_0_1). move => Q R HFaQ HFbR His_RInt. apply: Filter_prod HFaQ HFbR _. move => x y HQx HRy. case: (His_RInt x y HQx HRy) => I [H _]. now exists I. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl