fact: Definition Riemann_integrable (f:R -> R) (a b:R) : Type := forall eps:posreal, { phi:StepFun a b & { psi:StepFun a b | (forall t:R, Rmin a b <= t <= Rmax a b -> Rabs (f t - phi t) <= psi t) /\ Rabs (RiemannInt_SF psi) < eps } }.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra