proposition: Lemma RInt_gen_at_point f a b : ex_RInt f a b -> @RInt_gen V f (at_point a) (at_point b) = RInt f a b.
proof: Proof. move => Hfint. apply is_RInt_gen_unique. apply is_RInt_gen_at_point. exact: RInt_correct. Qed.
imports: Coq(Reals ssreflect) Rbar Hierarchy RInt Lim_seq Continuity Derive Rcomplements RInt_analysis