proposition: Lemma RiemannInt_P1 : forall (f:R -> R) (a b:R), Riemann_integrable f a b -> Riemann_integrable f b a.
proof: Proof. unfold Riemann_integrable; intros; elim (X eps); clear X; intros. elim p; clear p; intros x0 p; exists (mkStepFun (StepFun_P6 (pre x))); exists (mkStepFun (StepFun_P6 (pre x0))); elim p; clear p; intros; split. - intros; apply (H t); elim H1; clear H1; intros; split; [ apply Rle_trans with (Rmin b a); try assumption; right; unfold Rmin | apply Rle_trans with (Rmax b a); try assumption; right; unfold Rmax ]; (case (Rle_dec a b); case (Rle_dec b a); intros; try reflexivity || apply Rle_antisym; [ assumption | assumption | auto with real | auto with real ]). - generalize H0; unfold RiemannInt_SF; case (Rle_dec a b); case (Rle_dec b a); intros; (replace (Int_SF (subdivision_val (mkStepFun (StepFun_P6 (pre x0)))) (subdivision (mkStepFun (StepFun_P6 (pre x0))))) with (Int_SF (subdivision_val x0) (subdivision x0)); [ idtac | apply StepFun_P17 with (fe x0) a b; [ apply StepFun_P1 | apply StepFun_P2; apply (StepFun_P1 (mkStepFun (StepFun_P6 (pre x0)))) ] ]). + apply H1. + rewrite Rabs_Ropp; apply H1. + rewrite Rabs_Ropp in H1; apply H1. + apply H1. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra