proposition: Lemma RInt_gen_correct {Fa Fb : (R -> Prop) -> Prop} {FFa : ProperFilter' Fa} {FFb : ProperFilter' Fb} (f : R -> V) : ex_RInt_gen f Fa Fb -> is_RInt_gen f Fa Fb (RInt_gen f Fa Fb).
proof: Proof. intros [If HIf]. erewrite is_RInt_gen_unique ; exact HIf. Qed.
imports: Coq(Reals ssreflect) Rbar Hierarchy RInt Lim_seq Continuity Derive Rcomplements RInt_analysis