proposition: Lemma ex_RInt_point : forall (f : R -> V) a, ex_RInt f a a.
proof: Proof. intros f a. exists zero ; by apply is_RInt_point. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy