proposition: Lemma RiemannInt_P16 : forall (f:R -> R) (a b:R), Riemann_integrable f a b -> Riemann_integrable (fun x:R => Rabs (f x)) a b.
proof: Proof. unfold Riemann_integrable; intro f; intros; elim (X eps); clear X; intros phi [psi [H H0]]; split with (mkStepFun (StepFun_P32 phi)); split with psi; split; try assumption; intros; simpl; apply Rle_trans with (Rabs (f t - phi t)); [ apply Rabs_triang_inv2 | apply H; assumption ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra