proposition: Lemma RInt_gen_ext_eq {Fa Fb : (R -> Prop) -> Prop} {FFa : ProperFilter Fa} {FFb : ProperFilter Fb} (f g : R -> V): (forall x, f x = g x) -> ex_RInt_gen f Fa Fb -> RInt_gen f Fa Fb = RInt_gen g Fa Fb.
proof: Proof. move => Heq. apply: (RInt_gen_ext f g). exact: filter_forall => bnds x _. Qed.
imports: Coq(Reals ssreflect) Rbar Hierarchy RInt Lim_seq Continuity Derive Rcomplements RInt_analysis