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