proposition: Lemma is_RInt_gen_point (f : R -> V) (a : R) : is_RInt_gen f (at_point a) (at_point a) zero.
proof: Proof. apply is_RInt_gen_at_point. exact: is_RInt_point. Qed.
imports: Coq(Reals ssreflect) Rbar Hierarchy RInt Lim_seq Continuity Derive Rcomplements RInt_analysis