proposition: Lemma RInt_gen_ext : forall {V : CompleteNormedModule R_AbsRing} {Fa Fb : (R -> Prop) -> Prop} {FFa : ProperFilter Fa} {FFb : ProperFilter Fb} (f g : R -> V), filter_prod Fa Fb (fun ab => forall x, Rmin (fst ab) (snd ab) < x < Rmax (fst ab) (snd ab) -> f x = g x) -> RInt_gen f Fa Fb = RInt_gen g Fa Fb.
proof: Proof. intros V Fa Fb FFa FFb f g Heq. apply eq_close. apply @close_iota. split. now apply is_RInt_gen_ext. apply is_RInt_gen_ext. revert Heq. apply filter_imp. intros [u v] H t Ht. now rewrite <- H. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp