proposition: Lemma ex_RInt_gen_at_point f a b : @ex_RInt_gen V f (at_point a) (at_point b) <-> ex_RInt f a b.
proof: Proof. split; case => I. rewrite is_RInt_gen_at_point => HI. by exists I. rewrite -is_RInt_gen_at_point => HI. by exists I. Qed.
imports: Coq(Reals ssreflect) Rbar Hierarchy RInt Lim_seq Continuity Derive Rcomplements RInt_analysis