proposition: Lemma ex_RInt_Reals_1 (f : R -> R) (a b : R) : Riemann_integrable f a b -> ex_RInt f a b.
proof: Proof. move => pr ; exists (RiemannInt pr). exact: ex_RInt_Reals_aux_1. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy