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