proposition: Lemma RInt_point (a : R) (f : R -> V) : RInt f a a = zero.
proof: Proof. apply is_RInt_unique. exact: is_RInt_point. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy