proposition: Lemma is_RInt_gen_unique {Fa Fb : (R -> Prop) -> Prop} {FFa : ProperFilter' Fa} {FFb : ProperFilter' Fb} (f : R -> V) (l : V) : is_RInt_gen f Fa Fb l -> RInt_gen f Fa Fb = l.
proof: Proof. apply iota_filterlimi_locally. apply filter_forall. intros [a b] y1 u2 H1 H2. rewrite -(is_RInt_unique _ _ _ _ H1). now apply is_RInt_unique. Qed.
imports: Coq(Reals ssreflect) Rbar Hierarchy RInt Lim_seq Continuity Derive Rcomplements RInt_analysis