proposition: Lemma RInt_Reals (f : R -> R) (a b : R) : forall pr, RInt f a b = @RiemannInt f a b pr.
proof: Proof. intros pr. apply is_RInt_unique. apply 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