proposition: Lemma RiemannInt_le_ext : forall (f g:R -> R) (a b:R) (pr1:Riemann_integrable f a b) (pr2:Riemann_integrable g a b), a <= b -> (forall x:R, a < x < b -> f x <= g x) -> RiemannInt pr1 <= RiemannInt pr2.
proof: Proof. apply RiemannInt_P19. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality