proposition: Lemma StepFun_P32 : forall (a b:R) (f:StepFun a b), IsStepFun (fun x:R => Rabs (f x)) a b.
proof: Proof. intros a b f; unfold IsStepFun; apply existT with (subdivision f); unfold is_subdivision; apply existT with (map Rabs (subdivision_val f)); apply StepFun_P31; apply StepFun_P1. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra