proposition: Lemma is_RInt_gen_filterlim {V : CompleteNormedModule R_AbsRing} {Fa Fb : (R -> Prop) -> Prop} {FFa : ProperFilter Fa} {FFb : ProperFilter Fb} (f : R -> V) (lf : V) : is_RInt_gen f Fa Fb lf -> filterlim (fun x => RInt f x.1 x.2) (filter_prod Fa Fb) (locally lf).
proof: Proof. move => Hlf P HlfP. have := (Hlf P HlfP). case => Q R HFa HFb. econstructor. exact: HFa. exact: HFb. move => x y HQx HRy. case : (p x y HQx HRy) => x0 [HRInt HP]. by move: (is_RInt_unique f x y _ HRInt ) => ->. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl