proposition: Lemma StepFun_P33 : forall l2 l1:list R, ordered_Rlist l1 -> Rabs (Int_SF l2 l1) <= Int_SF (map Rabs l2) l1.
proof: Proof. induction l2 as [ | r r0 H]; intros. - simpl; rewrite Rabs_R0; right; reflexivity. - simpl; induction l1 as [| r1 l1 Hrecl1]. + rewrite Rabs_R0; right; reflexivity. + induction l1 as [| r2 l1 Hrecl0]. * rewrite Rabs_R0; right; reflexivity. * apply Rle_trans with (Rabs (r * (r2 - r1)) + Rabs (Int_SF r0 (cons r2 l1))). -- apply Rabs_triang. -- rewrite Rabs_mult; rewrite (Rabs_right (r2 - r1)); [ apply Rplus_le_compat_l; apply H; apply RList_P4 with r1; assumption | apply Rge_minus; apply Rle_ge; apply (H0 0%nat); simpl; apply Nat.lt_0_succ ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra