fact: Definition ex_RInt (f : R -> V) (a b : R) := exists If : V, is_RInt f a b If.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy