proposition: Lemma RiemannInt_P22 : forall (f:R -> R) (a b c:R), Riemann_integrable f a b -> a <= c <= b -> Riemann_integrable f a c.
proof: Proof. unfold Riemann_integrable; intros; elim (X eps); clear X; intros phi [psi H0]; elim H; elim H0; clear H H0; intros; assert (H3 : IsStepFun phi a c). { apply StepFun_P44 with b. { apply (pre phi). } split; assumption. } assert (H4 : IsStepFun psi a c). { apply StepFun_P44 with b. { apply (pre psi). } split; assumption. } split with (mkStepFun H3); split with (mkStepFun H4); split. { simpl; intros; apply H. replace (Rmin a b) with (Rmin a c) by (rewrite 2!Rmin_left; eauto using Rle_trans). destruct H5; split; try assumption. apply Rle_trans with (Rmax a c); try assumption. apply Rle_max_compat_l; assumption. } rewrite Rabs_right. { assert (H5 : IsStepFun psi c b). { apply StepFun_P46 with a. { apply StepFun_P6; assumption. } apply (pre psi). } replace (RiemannInt_SF (mkStepFun H4)) with (RiemannInt_SF psi - RiemannInt_SF (mkStepFun H5)). { apply Rle_lt_trans with (RiemannInt_SF psi). { unfold Rminus; pattern (RiemannInt_SF psi) at 2; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge; replace 0 with (RiemannInt_SF (mkStepFun (StepFun_P4 c b 0))). { apply StepFun_P37; try assumption. intros; simpl; unfold fct_cte; apply Rle_trans with (Rabs (f x - phi x)). { apply Rabs_pos. } apply H. rewrite Rmin_left; eauto using Rle_trans. rewrite Rmax_right; eauto using Rle_trans. destruct H6; split; left. { apply Rle_lt_trans with c; assumption. } assumption. } rewrite StepFun_P18; ring. } apply Rle_lt_trans with (Rabs (RiemannInt_SF psi)). { apply RRle_abs. } assumption. } assert (H6 : IsStepFun psi a b). { apply (pre psi). } replace (RiemannInt_SF psi) with (RiemannInt_SF (mkStepFun H6)). { rewrite <- (StepFun_P43 H4 H5 H6); ring. } unfold RiemannInt_SF; case (Rle_dec a b); intro. { eapply StepFun_P17. { apply StepFun_P1. } simpl; apply StepFun_P1. } apply Ropp_eq_compat; eapply StepFun_P17. { apply StepFun_P1. } simpl; apply StepFun_P1. } apply Rle_ge. replace 0 with (RiemannInt_SF (mkStepFun (StepFun_P4 a c 0))) by (rewrite StepFun_P18; ring). apply StepFun_P37; try assumption. intros; simpl; unfold fct_cte; apply Rle_trans with (Rabs (f x - phi x)). { apply Rabs_pos. } apply H. rewrite Rmin_left; eauto using Rle_trans. rewrite Rmax_right; eauto using Rle_trans. destruct H5; split; left. { assumption. } apply Rlt_le_trans with c; assumption. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra