proposition: Lemma StepFun_P43 : forall (f:R -> R) (a b c:R) (pr1:IsStepFun f a b) (pr2:IsStepFun f b c) (pr3:IsStepFun f a c), RiemannInt_SF (mkStepFun pr1) + RiemannInt_SF (mkStepFun pr2) = RiemannInt_SF (mkStepFun pr3).
proof: Proof. intros f; intros. pose proof pr1 as (l1,(lf1,H1)). pose proof pr2 as (l2,(lf2,H2)). pose proof pr3 as (l3,(lf3,H3)). replace (RiemannInt_SF (mkStepFun pr1)) with match Rle_dec a b with | left _ => Int_SF lf1 l1 | right _ => - Int_SF lf1 l1 end. 1:replace (RiemannInt_SF (mkStepFun pr2)) with match Rle_dec b c with | left _ => Int_SF lf2 l2 | right _ => - Int_SF lf2 l2 end. 1:replace (RiemannInt_SF (mkStepFun pr3)) with match Rle_dec a c with | left _ => Int_SF lf3 l3 | right _ => - Int_SF lf3 l3 end. 2,3,4:unfold RiemannInt_SF; case (Rle_dec _ _); intro;[|apply Ropp_eq_compat]; (eapply StepFun_P17;[|apply StepFun_P1]);assumption. case (Rle_dec a b) as [Hle|Hnle]; case (Rle_dec b c) as [Hle'|Hnle']; case (Rle_dec a c) as [Hle''|Hnle'']. - elim Hle; intro. 1:elim Hle'; intro. + replace (Int_SF lf3 l3) with (Int_SF (FF (app l1 l2) f) (app l1 l2)). 2:{ eapply StepFun_P17; [ apply (StepFun_P40 H H0 H1 H2) | apply H3 ]. } replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). { replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). { symmetry ; apply StepFun_P42. unfold adapted_couple in H1, H2; decompose [and] H1; decompose [and] H2; clear H1 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin; decide (Rle_dec a b) with Hle; decide (Rle_dec b c) with Hle'; reflexivity. } eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf2; apply H2; assumption | assumption ]. } eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf1; apply H1 | assumption ]. + replace (Int_SF lf2 l2) with 0. { rewrite Rplus_0_r; eapply StepFun_P17; [ apply H1 | rewrite <- H0 in H3; apply H3 ]. } symmetry ; eapply StepFun_P8; [ apply H2 | assumption ]. + replace (Int_SF lf1 l1) with 0. { rewrite Rplus_0_l; eapply StepFun_P17; [ apply H2 | rewrite H in H3; apply H3 ]. } symmetry ; eapply StepFun_P8; [ apply H1 | assumption ]. - elim Hnle''; apply Rle_trans with b; assumption. - apply Rplus_eq_reg_l with (Int_SF lf2 l2); replace (Int_SF lf2 l2 + (Int_SF lf1 l1 + - Int_SF lf2 l2)) with (Int_SF lf1 l1); [ idtac | ring ]. assert (H : c < b). { auto with real. } elim Hle''; intro. { rewrite Rplus_comm; replace (Int_SF lf1 l1) with (Int_SF (FF (app l3 l2) f) (app l3 l2)). { replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). { replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). { apply StepFun_P42. unfold adapted_couple in H2, H3; decompose [and] H2; decompose [and] H3; clear H3 H2; rewrite H10; rewrite H6; unfold Rmax, Rmin. decide (Rle_dec a c) with Hle''; decide (Rle_dec b c) with Hnle'; reflexivity. } eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf2; apply H2 | assumption ]. } eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf3; apply H3 | assumption ]. } eapply StepFun_P17; [ apply (StepFun_P40 H0 H H3 (StepFun_P2 H2)) | apply H1 ]. } replace (Int_SF lf3 l3) with 0. { rewrite Rplus_0_r; eapply StepFun_P17; [ apply H1 | apply StepFun_P2; rewrite <- H0 in H2; apply H2 ]. } symmetry ; eapply StepFun_P8; [ apply H3 | assumption ]. - replace (Int_SF lf2 l2) with (Int_SF lf3 l3 + Int_SF lf1 l1). { ring. } elim Hle; intro. { replace (Int_SF lf2 l2) with (Int_SF (FF (app l3 l1) f) (app l3 l1)). { replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). { replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). { symmetry ; apply StepFun_P42. unfold adapted_couple in H1, H3; decompose [and] H1; decompose [and] H3; clear H3 H1; rewrite H9; rewrite H5; unfold Rmax, Rmin; decide (Rle_dec a c) with Hnle''; decide (Rle_dec a b) with Hle; reflexivity. } eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf1; apply H1 | assumption ]. } eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf3; apply H3 | assumption ]. } eapply StepFun_P17. { assert (H0 : c < a). { auto with real. } apply (StepFun_P40 H0 H (StepFun_P2 H3) H1). } apply StepFun_P2; apply H2. } replace (Int_SF lf1 l1) with 0. { rewrite Rplus_0_r; eapply StepFun_P17; [ apply H3 | rewrite <- H in H2; apply H2 ]. } symmetry ; eapply StepFun_P8; [ apply H1 | assumption ]. - assert (H : b < a). { auto with real. } replace (Int_SF lf2 l2) with (Int_SF lf3 l3 + Int_SF lf1 l1). { ring. } rewrite Rplus_comm; elim Hle''; intro. { replace (Int_SF lf2 l2) with (Int_SF (FF (app l1 l3) f) (app l1 l3)). { replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). { replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). { symmetry ; apply StepFun_P42. unfold adapted_couple in H1, H3; decompose [and] H1; decompose [and] H3; clear H3 H1; rewrite H11; rewrite H5; unfold Rmax, Rmin; decide (Rle_dec a c) with Hle''; decide (Rle_dec a b) with Hnle; reflexivity. } eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf1; apply H1 | assumption ]. } eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf3; apply H3 | assumption ]. } eapply StepFun_P17. { apply (StepFun_P40 H H0 (StepFun_P2 H1) H3). } apply H2. } replace (Int_SF lf3 l3) with 0. { rewrite Rplus_0_r; eapply StepFun_P17; [ apply H1 | rewrite <- H0 in H2; apply StepFun_P2; apply H2 ]. } symmetry ; eapply StepFun_P8; [ apply H3 | assumption ]. - assert (H : c < a). { auto with real. } replace (Int_SF lf1 l1) with (Int_SF lf2 l2 + Int_SF lf3 l3). { ring. } elim Hle'; intro. { replace (Int_SF lf1 l1) with (Int_SF (FF (app l2 l3) f) (app l2 l3)). { replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). { replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). { symmetry ; apply StepFun_P42. unfold adapted_couple in H2, H3; decompose [and] H2; decompose [and] H3; clear H3 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin; decide (Rle_dec a c) with Hnle''; decide (Rle_dec b c) with Hle'; reflexivity. } eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf2; apply H2 | assumption ]. } eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf3; apply H3 | assumption ]. } eapply StepFun_P17. { apply (StepFun_P40 H0 H H2 (StepFun_P2 H3)). } apply StepFun_P2; apply H1. } replace (Int_SF lf2 l2) with 0. { rewrite Rplus_0_l; eapply StepFun_P17; [ apply H3 | rewrite H0 in H1; apply H1 ]. } symmetry; eapply StepFun_P8; [ apply H2 | assumption ]. - elim Hnle'; apply Rle_trans with a; try assumption. auto with real. - assert (H : c < b). { auto with real. } assert (H0 : b < a). { auto with real. } replace (Int_SF lf3 l3) with (Int_SF lf2 l2 + Int_SF lf1 l1). { ring. } replace (Int_SF lf3 l3) with (Int_SF (FF (app l2 l1) f) (app l2 l1)). { replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). { replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). { symmetry ; apply StepFun_P42. unfold adapted_couple in H2, H1; decompose [and] H2; decompose [and] H1; clear H1 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin; decide (Rle_dec a b) with Hnle; decide (Rle_dec b c) with Hnle'; reflexivity. } eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf2; apply H2 | assumption ]. } eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf1; apply H1 | assumption ]. } eapply StepFun_P17. { apply (StepFun_P40 H H0 (StepFun_P2 H2) (StepFun_P2 H1)). } apply StepFun_P2; apply H3. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra