proposition: Lemma StepFun_P35 : forall (l:list R) (a b:R) (f g:R -> R), ordered_Rlist l -> pos_Rl l 0 = a -> pos_Rl l (pred (length l)) = b -> (forall x:R, a < x < b -> f x <= g x) -> Int_SF (FF l f) l <= Int_SF (FF l g) l.
proof: Proof. induction l as [ | r r0 H]; intros. { right; reflexivity. } simpl; induction r0 as [| r0 r1 Hrecr0]. { right; reflexivity. } simpl; apply Rplus_le_compat. 2:{ simpl in H; apply H with r0 b. - apply RList_P4 with r; assumption. - reflexivity. - rewrite <- H2; reflexivity. - intros; apply H3; elim H4; intros; split; try assumption. apply Rle_lt_trans with r0; try assumption. rewrite <- H1. simpl; apply (H0 0%nat); simpl; apply Nat.lt_0_succ. } case (Req_dec r r0); intro. { rewrite H4; right; ring. } do 2 rewrite <- (Rmult_comm (r0 - r)); apply Rmult_le_compat_l. { apply Rge_le; apply Rge_minus; apply Rle_ge; apply (H0 0%nat); simpl; apply Nat.lt_0_succ. } apply H3; split. { apply Rmult_lt_reg_l with 2. { prove_sup0. } unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite Rinv_r. 2:discrR. simpl in H1. assert (H6 := H0 0%nat (Nat.lt_0_succ _)). simpl in H6. lra. } apply Rmult_lt_reg_l with 2. { prove_sup0. } unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite Rinv_r. 2:discrR. rewrite Rmult_1_l; rewrite <-Rplus_diag; assert (H5 : r0 <= b). { replace b with (pos_Rl (cons r (cons r0 r1)) (pred (length (cons r (cons r0 r1))))). replace r0 with (pos_Rl (cons r (cons r0 r1)) 1). { elim (RList_P6 (cons r (cons r0 r1))); intros; apply H5. { assumption. } { simpl; lia. } simpl; apply Nat.lt_succ_diag_r. } reflexivity. } apply Rle_lt_trans with (r + b). { apply Rplus_le_compat_l; assumption. } rewrite (Rplus_comm r); apply Rplus_lt_compat_l. apply Rlt_le_trans with r0. { assert (H6 := H0 0%nat (Nat.lt_0_succ _)). simpl in H6. lra. } assumption. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra