# Library Coq.Reals.RiemannInt_SF

``` Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis. Require Import Classical_Prop. Open Local Scope R_scope. Set Implicit Arguments. Definition Nbound (I:nat -> Prop) : Prop :=    exists n : nat, (forall i:nat, I i -> (i <= n)%nat). Lemma IZN_var : forall z:Z, (0 <= z)%Z -> {n : nat | z = Z_of_nat n}. intros; apply Z_of_nat_complete_inf; assumption. Qed. Lemma Nzorn :  forall I:nat -> Prop,    (exists n : nat, I n) ->    Nbound I -> sigT (fun n:nat => I n /\ (forall i:nat, I i -> (i <= n)%nat)). intros I H H0; set (E := fun x:R => exists i : nat, I i /\ INR i = x);  assert (H1 : bound E). unfold Nbound in H0; elim H0; intros N H1; unfold bound in |- *;  exists (INR N); unfold is_upper_bound in |- *; intros;  unfold E in H2; elim H2; intros; elim H3; intros;  rewrite <- H5; apply le_INR; apply H1; assumption. assert (H2 : exists x : R, E x). elim H; intros; exists (INR x); unfold E in |- *; exists x; split;  [ assumption | reflexivity ]. assert (H3 := completeness E H1 H2); elim H3; intros; unfold is_lub in p;  elim p; clear p; intros; unfold is_upper_bound in H4, H5;  assert (H6 : 0 <= x). elim H2; intros; unfold E in H6; elim H6; intros; elim H7; intros;  apply Rle_trans with x0;  [ rewrite <- H9; change (INR 0 <= INR x1) in |- *; apply le_INR; apply le_O_n | apply H4; assumption ]. assert (H7 := archimed x); elim H7; clear H7; intros;  assert (H9 : x <= IZR (up x) - 1). apply H5; intros; assert (H10 := H4 _ H9); unfold E in H9; elim H9; intros;  elim H11; intros; rewrite <- H13; apply Rplus_le_reg_l with 1;  replace (1 + (IZR (up x) - 1)) with (IZR (up x));  [ idtac | ring ]; replace (1 + INR x1) with (INR (S x1));  [ idtac | rewrite S_INR; ring ]. assert (H14 : (0 <= up x)%Z). apply le_IZR; apply Rle_trans with x; [ apply H6 | left; assumption ]. assert (H15 := IZN _ H14); elim H15; clear H15; intros; rewrite H15;  rewrite <- INR_IZR_INZ; apply le_INR; apply lt_le_S;  apply INR_lt; rewrite H13; apply Rle_lt_trans with x;  [ assumption | rewrite INR_IZR_INZ; rewrite <- H15; assumption ]. assert (H10 : x = IZR (up x) - 1). apply Rle_antisym;  [ assumption  | apply Rplus_le_reg_l with (- x + 1);     replace (- x + 1 + (IZR (up x) - 1)) with (IZR (up x) - x);     [ idtac | ring ]; replace (- x + 1 + x) with 1;     [ assumption | ring ] ]. assert (H11 : (0 <= up x)%Z). apply le_IZR; apply Rle_trans with x; [ apply H6 | left; assumption ]. assert (H12 := IZN_var H11); elim H12; clear H12; intros; assert (H13 : E x). elim (classic (E x)); intro; try assumption. cut (forall y:R, E y -> y <= x - 1). intro; assert (H14 := H5 _ H13); cut (x - 1 < x). intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H15)). apply Rminus_lt; replace (x - 1 - x) with (-1); [ idtac | ring ];  rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; apply Rlt_0_1. intros; assert (H14 := H4 _ H13); elim H14; intro; unfold E in H13; elim H13;  intros; elim H16; intros; apply Rplus_le_reg_l with 1. replace (1 + (x - 1)) with x; [ idtac | ring ]; rewrite <- H18;  replace (1 + INR x1) with (INR (S x1)); [ idtac | rewrite S_INR; ring ]. cut (x = INR (pred x0)). intro; rewrite H19; apply le_INR; apply lt_le_S; apply INR_lt; rewrite H18;  rewrite <- H19; assumption. rewrite H10; rewrite p; rewrite <- INR_IZR_INZ; replace 1 with (INR 1);  [ idtac | reflexivity ]; rewrite <- minus_INR. replace (x0 - 1)%nat with (pred x0);  [ reflexivity  | case x0; [ reflexivity | intro; simpl in |- *; apply minus_n_O ] ]. induction x0 as [| x0 Hrecx0];  [ rewrite p in H7; rewrite <- INR_IZR_INZ in H7; simpl in H7; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H7)) | apply le_n_S; apply le_O_n ]. rewrite H15 in H13; elim H12; assumption. split with (pred x0); unfold E in H13; elim H13; intros; elim H12; intros;  rewrite H10 in H15; rewrite p in H15; rewrite <- INR_IZR_INZ in H15;  assert (H16 : INR x0 = INR x1 + 1). rewrite H15; ring. rewrite <- S_INR in H16; assert (H17 := INR_eq _ _ H16); rewrite H17;  simpl in |- *; split. assumption. intros; apply INR_le; rewrite H15; rewrite <- H15; elim H12; intros;  rewrite H20; apply H4; unfold E in |- *; exists i;  split; [ assumption | reflexivity ]. Qed. Definition open_interval (a b x:R) : Prop := a < x < b. Definition co_interval (a b x:R) : Prop := a <= x < b. Definition adapted_couple (f:R -> R) (a b:R) (l lf:Rlist) : Prop :=   ordered_Rlist l /\   pos_Rl l 0 = Rmin a b /\   pos_Rl l (pred (Rlength l)) = Rmax a b /\   Rlength l = S (Rlength lf) /\   (forall i:nat,      (i < pred (Rlength l))%nat ->      constant_D_eq f (open_interval (pos_Rl l i) (pos_Rl l (S i)))        (pos_Rl lf i)). Definition adapted_couple_opt (f:R -> R) (a b:R) (l lf:Rlist) :=   adapted_couple f a b l lf /\   (forall i:nat,      (i < pred (Rlength lf))%nat ->      pos_Rl lf i <> pos_Rl lf (S i) \/ f (pos_Rl l (S i)) <> pos_Rl lf i) /\   (forall i:nat, (i < pred (Rlength l))%nat -> pos_Rl l i <> pos_Rl l (S i)). Definition is_subdivision (f:R -> R) (a b:R) (l:Rlist) : Type :=   sigT (fun l0:Rlist => adapted_couple f a b l l0). Definition IsStepFun (f:R -> R) (a b:R) : Type :=   sigT (fun l:Rlist => is_subdivision f a b l). Record StepFun (a b:R) : Type := mkStepFun   {fe :> R -> R; pre : IsStepFun fe a b}. Definition subdivision (a b:R) (f:StepFun a b) : Rlist := projT1 (pre f). Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist :=   match projT2 (pre f) with   | existT a b => a   end. Boxed Fixpoint Int_SF (l k:Rlist) {struct l} : R :=   match l with   | nil => 0   | cons a l' =>       match k with       | nil => 0       | cons x nil => 0       | cons x (cons y k') => a * (y - x) + Int_SF l' (cons y k')       end   end. Definition RiemannInt_SF (a b:R) (f:StepFun a b) : R :=   match Rle_dec a b with   | left _ => Int_SF (subdivision_val f) (subdivision f)   | right _ => - Int_SF (subdivision_val f) (subdivision f)   end. Lemma StepFun_P1 :  forall (a b:R) (f:StepFun a b),    adapted_couple f a b (subdivision f) (subdivision_val f). intros a b f; unfold subdivision_val in |- *; case (projT2 (pre f)); intros;  apply a0. Qed. Lemma StepFun_P2 :  forall (a b:R) (f:R -> R) (l lf:Rlist),    adapted_couple f a b l lf -> adapted_couple f b a l lf. unfold adapted_couple in |- *; intros; decompose [and] H; clear H;  repeat split; try assumption. rewrite H2; unfold Rmin in |- *; case (Rle_dec a b); intro;  case (Rle_dec b a); intro; try reflexivity. apply Rle_antisym; assumption. apply Rle_antisym; auto with real. rewrite H1; unfold Rmax in |- *; case (Rle_dec a b); intro;  case (Rle_dec b a); intro; try reflexivity. apply Rle_antisym; assumption. apply Rle_antisym; auto with real. Qed. Lemma StepFun_P3 :  forall a b c:R,    a <= b ->    adapted_couple (fct_cte c) a b (cons a (cons b nil)) (cons c nil). intros; unfold adapted_couple in |- *; repeat split. unfold ordered_Rlist in |- *; intros; simpl in H0; inversion H0;  [ simpl in |- *; assumption | elim (le_Sn_O _ H2) ]. simpl in |- *; unfold Rmin in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. simpl in |- *; unfold Rmax in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. unfold constant_D_eq, open_interval in |- *; intros; simpl in H0;  inversion H0; [ reflexivity | elim (le_Sn_O _ H3) ]. Qed. Lemma StepFun_P4 : forall a b c:R, IsStepFun (fct_cte c) a b. intros; unfold IsStepFun in |- *; case (Rle_dec a b); intro. apply existT with (cons a (cons b nil)); unfold is_subdivision in |- *;  apply existT with (cons c nil); apply (StepFun_P3 c r). apply existT with (cons b (cons a nil)); unfold is_subdivision in |- *;  apply existT with (cons c nil); apply StepFun_P2;  apply StepFun_P3; auto with real. Qed. Lemma StepFun_P5 :  forall (a b:R) (f:R -> R) (l:Rlist),    is_subdivision f a b l -> is_subdivision f b a l. destruct 1 as (x,(H0,(H1,(H2,(H3,H4))))); exists x;   repeat split; try assumption. rewrite H1; apply Rmin_comm. rewrite H2; apply Rmax_comm. Qed. Lemma StepFun_P6 :  forall (f:R -> R) (a b:R), IsStepFun f a b -> IsStepFun f b a. unfold IsStepFun in |- *; intros; elim X; intros; apply existT with x;  apply StepFun_P5; assumption. Qed. Lemma StepFun_P7 :  forall (a b r1 r2 r3:R) (f:R -> R) (l lf:Rlist),    a <= b ->    adapted_couple f a b (cons r1 (cons r2 l)) (cons r3 lf) ->    adapted_couple f r2 b (cons r2 l) lf. unfold adapted_couple in |- *; intros; decompose [and] H0; clear H0;  assert (H5 : Rmax a b = b). unfold Rmax in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. assert (H7 : r2 <= b). rewrite H5 in H2; rewrite <- H2; apply RList_P7;  [ assumption | simpl in |- *; right; left; reflexivity ]. repeat split. apply RList_P4 with r1; assumption. rewrite H5 in H2; unfold Rmin in |- *; case (Rle_dec r2 b); intro;  [ reflexivity | elim n; assumption ]. unfold Rmax in |- *; case (Rle_dec r2 b); intro;  [ rewrite H5 in H2; rewrite <- H2; reflexivity | elim n; assumption ]. simpl in H4; simpl in |- *; apply INR_eq; apply Rplus_eq_reg_l with 1;  do 2 rewrite (Rplus_comm 1); do 2 rewrite <- S_INR;  rewrite H4; reflexivity. intros; unfold constant_D_eq, open_interval in |- *; intros;  unfold constant_D_eq, open_interval in H6;  assert (H9 : (S i < pred (Rlength (cons r1 (cons r2 l))))%nat). simpl in |- *; simpl in H0; apply lt_n_S; assumption. assert (H10 := H6 _ H9); apply H10; assumption. Qed. Lemma StepFun_P8 :  forall (f:R -> R) (l1 lf1:Rlist) (a b:R),    adapted_couple f a b l1 lf1 -> a = b -> Int_SF lf1 l1 = 0. simple induction l1. intros; induction lf1 as [| r lf1 Hreclf1]; reflexivity. simple induction r0. intros; induction lf1 as [| r1 lf1 Hreclf1]. reflexivity. unfold adapted_couple in H0; decompose [and] H0; clear H0; simpl in H5;  discriminate. intros; induction lf1 as [| r3 lf1 Hreclf1]. reflexivity. simpl in |- *; cut (r = r1). intro; rewrite H3; rewrite (H0 lf1 r b). ring. rewrite H3; apply StepFun_P7 with a r r3; [ right; assumption | assumption ]. clear H H0 Hreclf1 r0; unfold adapted_couple in H1; decompose [and] H1;  intros; simpl in H4; rewrite H4; unfold Rmin in |- *;  case (Rle_dec a b); intro; [ assumption | reflexivity ]. unfold adapted_couple in H1; decompose [and] H1; intros; apply Rle_antisym. apply (H3 0%nat); simpl in |- *; apply lt_O_Sn. simpl in H5; rewrite H2 in H5; rewrite H5; replace (Rmin b b) with (Rmax a b);  [ rewrite <- H4; apply RList_P7;     [ assumption | simpl in |- *; right; left; reflexivity ]  | unfold Rmin, Rmax in |- *; case (Rle_dec b b); case (Rle_dec a b); intros;     try assumption || reflexivity ]. Qed. Lemma StepFun_P9 :  forall (a b:R) (f:R -> R) (l lf:Rlist),    adapted_couple f a b l lf -> a <> b -> (2 <= Rlength l)%nat. intros; unfold adapted_couple in H; decompose [and] H; clear H;  induction l as [| r l Hrecl];  [ simpl in H4; discriminate  | induction l as [| r0 l Hrecl0];     [ simpl in H3; simpl in H2; generalize H3; generalize H2; unfold Rmin, Rmax in |- *; case (Rle_dec a b); intros; elim H0; rewrite <- H5; rewrite <- H7; reflexivity | simpl in |- *; do 2 apply le_n_S; apply le_O_n ] ]. Qed. Lemma StepFun_P10 :  forall (f:R -> R) (l lf:Rlist) (a b:R),    a <= b ->    adapted_couple f a b l lf ->     exists l' : Rlist,      (exists lf' : Rlist, adapted_couple_opt f a b l' lf'). simple induction l. intros; unfold adapted_couple in H0; decompose [and] H0; simpl in H4;  discriminate. intros; case (Req_dec a b); intro. exists (cons a nil); exists nil; unfold adapted_couple_opt in |- *;  unfold adapted_couple in |- *; unfold ordered_Rlist in |- *;  repeat split; try (intros; simpl in H3; elim (lt_n_O _ H3)). simpl in |- *; rewrite <- H2; unfold Rmin in |- *; case (Rle_dec a a); intro;  reflexivity. simpl in |- *; rewrite <- H2; unfold Rmax in |- *; case (Rle_dec a a); intro;  reflexivity. elim (RList_P20 _ (StepFun_P9 H1 H2)); intros t1 [t2 [t3 H3]];  induction lf as [| r1 lf Hreclf]. unfold adapted_couple in H1; decompose [and] H1; rewrite H3 in H7;  simpl in H7; discriminate. clear Hreclf; assert (H4 : adapted_couple f t2 b r0 lf). rewrite H3 in H1; assert (H4 := RList_P21 _ _ H3); simpl in H4; rewrite H4;  eapply StepFun_P7; [ apply H0 | apply H1 ]. cut (t2 <= b). intro; assert (H6 := H _ _ _ H5 H4); case (Req_dec t1 t2); intro Hyp_eq. replace a with t2. apply H6. rewrite <- Hyp_eq; rewrite H3 in H1; unfold adapted_couple in H1;  decompose [and] H1; clear H1; simpl in H9; rewrite H9;  unfold Rmin in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. elim H6; clear H6; intros l' [lf' H6]; case (Req_dec t2 b); intro. exists (cons a (cons b nil)); exists (cons r1 nil);  unfold adapted_couple_opt in |- *; unfold adapted_couple in |- *;  repeat split. unfold ordered_Rlist in |- *; intros; simpl in H8; inversion H8;  [ simpl in |- *; assumption | elim (le_Sn_O _ H10) ]. simpl in |- *; unfold Rmin in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. simpl in |- *; unfold Rmax in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. intros; simpl in H8; inversion H8. unfold constant_D_eq, open_interval in |- *; intros; simpl in |- *;  simpl in H9; rewrite H3 in H1; unfold adapted_couple in H1;  decompose [and] H1; apply (H16 0%nat). simpl in |- *; apply lt_O_Sn. unfold open_interval in |- *; simpl in |- *; rewrite H7; simpl in H13;  rewrite H13; unfold Rmin in |- *; case (Rle_dec a b);  intro; [ assumption | elim n; assumption ]. elim (le_Sn_O _ H10). intros; simpl in H8; elim (lt_n_O _ H8). intros; simpl in H8; inversion H8;  [ simpl in |- *; assumption | elim (le_Sn_O _ H10) ]. assert (Hyp_min : Rmin t2 b = t2). unfold Rmin in |- *; case (Rle_dec t2 b); intro;  [ reflexivity | elim n; assumption ]. unfold adapted_couple in H6; elim H6; clear H6; intros;  elim (RList_P20 _ (StepFun_P9 H6 H7)); intros s1 [s2 [s3 H9]];  induction lf' as [| r2 lf' Hreclf']. unfold adapted_couple in H6; decompose [and] H6; rewrite H9 in H13;  simpl in H13; discriminate. clear Hreclf'; case (Req_dec r1 r2); intro. case (Req_dec (f t2) r1); intro. exists (cons t1 (cons s2 s3)); exists (cons r1 lf'); rewrite H3 in H1;  rewrite H9 in H6; unfold adapted_couple in H6, H1;  decompose [and] H1; decompose [and] H6; clear H1 H6;  unfold adapted_couple_opt in |- *; unfold adapted_couple in |- *;  repeat split. unfold ordered_Rlist in |- *; intros; simpl in H1;  induction i as [| i Hreci]. simpl in |- *; apply Rle_trans with s1. replace s1 with t2. apply (H12 0%nat). simpl in |- *; apply lt_O_Sn. simpl in H19; rewrite H19; symmetry in |- *; apply Hyp_min. apply (H16 0%nat); simpl in |- *; apply lt_O_Sn. change (pos_Rl (cons s2 s3) i <= pos_Rl (cons s2 s3) (S i)) in |- *;  apply (H16 (S i)); simpl in |- *; assumption. simpl in |- *; simpl in H14; rewrite H14; reflexivity. simpl in |- *; simpl in H18; rewrite H18; unfold Rmax in |- *;  case (Rle_dec a b); case (Rle_dec t2 b); intros; reflexivity || elim n;  assumption. simpl in |- *; simpl in H20; apply H20. intros; simpl in H1; unfold constant_D_eq, open_interval in |- *; intros;  induction i as [| i Hreci]. simpl in |- *; simpl in H6; case (total_order_T x t2); intro. elim s; intro. apply (H17 0%nat);  [ simpl in |- *; apply lt_O_Sn | unfold open_interval in |- *; simpl in |- *; elim H6; intros; split; assumption ]. rewrite b0; assumption. rewrite H10; apply (H22 0%nat);  [ simpl in |- *; apply lt_O_Sn  | unfold open_interval in |- *; simpl in |- *; replace s1 with t2;     [ elim H6; intros; split; assumption | simpl in H19; rewrite H19; rewrite Hyp_min; reflexivity ] ]. simpl in |- *; simpl in H6; apply (H22 (S i));  [ simpl in |- *; assumption | unfold open_interval in |- *; simpl in |- *; apply H6 ]. intros; simpl in H1; rewrite H10;  change    (pos_Rl (cons r2 lf') i <> pos_Rl (cons r2 lf') (S i) \/     f (pos_Rl (cons s1 (cons s2 s3)) (S i)) <> pos_Rl (cons r2 lf') i)   in |- *; rewrite <- H9; elim H8; intros; apply H6;  simpl in |- *; apply H1. intros; induction i as [| i Hreci]. simpl in |- *; red in |- *; intro; elim Hyp_eq; apply Rle_antisym. apply (H12 0%nat); simpl in |- *; apply lt_O_Sn. rewrite <- Hyp_min; rewrite H6; simpl in H19; rewrite <- H19;  apply (H16 0%nat); simpl in |- *; apply lt_O_Sn. elim H8; intros; rewrite H9 in H21; apply (H21 (S i)); simpl in |- *;  simpl in H1; apply H1. exists (cons t1 l'); exists (cons r1 (cons r2 lf')); rewrite H9 in H6;  rewrite H3 in H1; unfold adapted_couple in H1, H6;  decompose [and] H6; decompose [and] H1; clear H6 H1;  unfold adapted_couple_opt in |- *; unfold adapted_couple in |- *;  repeat split. rewrite H9; unfold ordered_Rlist in |- *; intros; simpl in H1;  induction i as [| i Hreci]. simpl in |- *; replace s1 with t2. apply (H16 0%nat); simpl in |- *; apply lt_O_Sn. simpl in H14; rewrite H14; rewrite Hyp_min; reflexivity. change   (pos_Rl (cons s1 (cons s2 s3)) i <= pos_Rl (cons s1 (cons s2 s3)) (S i))  in |- *; apply (H12 i); simpl in |- *; apply lt_S_n;  assumption. simpl in |- *; simpl in H19; apply H19. rewrite H9; simpl in |- *; simpl in H13; rewrite H13; unfold Rmax in |- *;  case (Rle_dec t2 b); case (Rle_dec a b); intros; reflexivity || elim n;  assumption. rewrite H9; simpl in |- *; simpl in H15; rewrite H15; reflexivity. intros; simpl in H1; unfold constant_D_eq, open_interval in |- *; intros;  induction i as [| i Hreci]. simpl in |- *; rewrite H9 in H6; simpl in H6; apply (H22 0%nat). simpl in |- *; apply lt_O_Sn. unfold open_interval in |- *; simpl in |- *. replace t2 with s1. assumption. simpl in H14; rewrite H14; rewrite Hyp_min; reflexivity. change (f x = pos_Rl (cons r2 lf') i) in |- *; clear Hreci; apply (H17 i). simpl in |- *; rewrite H9 in H1; simpl in H1; apply lt_S_n; apply H1. rewrite H9 in H6; unfold open_interval in |- *; apply H6. intros; simpl in H1; induction i as [| i Hreci]. simpl in |- *; rewrite H9; right; simpl in |- *; replace s1 with t2. assumption. simpl in H14; rewrite H14; rewrite Hyp_min; reflexivity. elim H8; intros; apply (H6 i). simpl in |- *; apply lt_S_n; apply H1. intros; rewrite H9; induction i as [| i Hreci]. simpl in |- *; red in |- *; intro; elim Hyp_eq; apply Rle_antisym. apply (H16 0%nat); simpl in |- *; apply lt_O_Sn. rewrite <- Hyp_min; rewrite H6; simpl in H14; rewrite <- H14; right;  reflexivity. elim H8; intros; rewrite <- H9; apply (H21 i); rewrite H9; rewrite H9 in H1;  simpl in |- *; simpl in H1; apply lt_S_n; apply H1. exists (cons t1 l'); exists (cons r1 (cons r2 lf')); rewrite H9 in H6;  rewrite H3 in H1; unfold adapted_couple in H1, H6;  decompose [and] H6; decompose [and] H1; clear H6 H1;  unfold adapted_couple_opt in |- *; unfold adapted_couple in |- *;  repeat split. rewrite H9; unfold ordered_Rlist in |- *; intros; simpl in H1;  induction i as [| i Hreci]. simpl in |- *; replace s1 with t2. apply (H15 0%nat); simpl in |- *; apply lt_O_Sn. simpl in H13; rewrite H13; rewrite Hyp_min; reflexivity. change   (pos_Rl (cons s1 (cons s2 s3)) i <= pos_Rl (cons s1 (cons s2 s3)) (S i))  in |- *; apply (H11 i); simpl in |- *; apply lt_S_n;  assumption. simpl in |- *; simpl in H18; apply H18. rewrite H9; simpl in |- *; simpl in H12; rewrite H12; unfold Rmax in |- *;  case (Rle_dec t2 b); case (Rle_dec a b); intros; reflexivity || elim n;  assumption. rewrite H9; simpl in |- *; simpl in H14; rewrite H14; reflexivity. intros; simpl in H1; unfold constant_D_eq, open_interval in |- *; intros;  induction i as [| i Hreci]. simpl in |- *; rewrite H9 in H6; simpl in H6; apply (H21 0%nat). simpl in |- *; apply lt_O_Sn. unfold open_interval in |- *; simpl in |- *; replace t2 with s1. assumption. simpl in H13; rewrite H13; rewrite Hyp_min; reflexivity. change (f x = pos_Rl (cons r2 lf') i) in |- *; clear Hreci; apply (H16 i). simpl in |- *; rewrite H9 in H1; simpl in H1; apply lt_S_n; apply H1. rewrite H9 in H6; unfold open_interval in |- *; apply H6. intros; simpl in H1; induction i as [| i Hreci]. simpl in |- *; left; assumption. elim H8; intros; apply (H6 i). simpl in |- *; apply lt_S_n; apply H1. intros; rewrite H9; induction i as [| i Hreci]. simpl in |- *; red in |- *; intro; elim Hyp_eq; apply Rle_antisym. apply (H15 0%nat); simpl in |- *; apply lt_O_Sn. rewrite <- Hyp_min; rewrite H6; simpl in H13; rewrite <- H13; right;  reflexivity. elim H8; intros; rewrite <- H9; apply (H20 i); rewrite H9; rewrite H9 in H1;  simpl in |- *; simpl in H1; apply lt_S_n; apply H1. rewrite H3 in H1; clear H4; unfold adapted_couple in H1; decompose [and] H1;  clear H1; clear H H7 H9; cut (Rmax a b = b);  [ intro; rewrite H in H5; rewrite <- H5; apply RList_P7;     [ assumption | simpl in |- *; right; left; reflexivity ]  | unfold Rmax in |- *; case (Rle_dec a b); intro;     [ reflexivity | elim n; assumption ] ]. Qed. Lemma StepFun_P11 :  forall (a b r r1 r3 s1 s2 r4:R) (r2 lf1 s3 lf2:Rlist)    (f:R -> R),    a < b ->    adapted_couple f a b (cons r (cons r1 r2)) (cons r3 lf1) ->    adapted_couple_opt f a b (cons s1 (cons s2 s3)) (cons r4 lf2) -> r1 <= s2. intros; unfold adapted_couple_opt in H1; elim H1; clear H1; intros;  unfold adapted_couple in H0, H1; decompose [and] H0;  decompose [and] H1; clear H0 H1; assert (H12 : r = s1). simpl in H10; simpl in H5; rewrite H10; rewrite H5; reflexivity. assert (H14 := H3 0%nat (lt_O_Sn _)); simpl in H14; elim H14; intro. assert (H15 := H7 0%nat (lt_O_Sn _)); simpl in H15; elim H15; intro. rewrite <- H12 in H1; case (Rle_dec r1 s2); intro; try assumption. assert (H16 : s2 < r1); auto with real. induction s3 as [| r0 s3 Hrecs3]. simpl in H9; rewrite H9 in H16; cut (r1 <= Rmax a b). intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H17 H16)). rewrite <- H4; apply RList_P7;  [ assumption | simpl in |- *; right; left; reflexivity ]. clear Hrecs3; induction lf2 as [| r5 lf2 Hreclf2]. simpl in H11; discriminate. clear Hreclf2; assert (H17 : r3 = r4). set (x := (r + s2) / 2); assert (H17 := H8 0%nat (lt_O_Sn _));  assert (H18 := H13 0%nat (lt_O_Sn _));  unfold constant_D_eq, open_interval in H17, H18; simpl in H17;  simpl in H18; rewrite <- (H17 x). rewrite <- (H18 x). reflexivity. rewrite <- H12; unfold x in |- *; split. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite (Rplus_comm r); rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. unfold x in |- *; split. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. apply Rlt_trans with s2;  [ apply Rmult_lt_reg_l with 2;     [ prove_sup0     | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2));        rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym;        [ rewrite Rmult_1_l; rewrite (Rplus_comm r); rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]  | assumption ]. assert (H18 : f s2 = r3). apply (H8 0%nat);  [ simpl in |- *; apply lt_O_Sn | unfold open_interval in |- *; simpl in |- *; split; assumption ]. assert (H19 : r3 = r5). assert (H19 := H7 1%nat); simpl in H19;  assert (H20 := H19 (lt_n_S _ _ (lt_O_Sn _))); elim H20;  intro. set (x := (s2 + Rmin r1 r0) / 2); assert (H22 := H8 0%nat);  assert (H23 := H13 1%nat); simpl in H22; simpl in H23;  rewrite <- (H22 (lt_O_Sn _) x). rewrite <- (H23 (lt_n_S _ _ (lt_O_Sn _)) x). reflexivity. unfold open_interval in |- *; simpl in |- *; unfold x in |- *; split. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; unfold Rmin in |- *; case (Rle_dec r1 r0); intro; assumption | discrR ] ]. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite double;        apply Rlt_le_trans with (r0 + Rmin r1 r0);        [ do 2 rewrite <- (Rplus_comm (Rmin r1 r0)); apply Rplus_lt_compat_l; assumption | apply Rplus_le_compat_l; apply Rmin_r ]     | discrR ] ]. unfold open_interval in |- *; simpl in |- *; unfold x in |- *; split. apply Rlt_trans with s2;  [ assumption  | apply Rmult_lt_reg_l with 2;     [ prove_sup0     | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2));        rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym;        [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; unfold Rmin in |- *; case (Rle_dec r1 r0); intro; assumption | discrR ] ] ]. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite double;        apply Rlt_le_trans with (r1 + Rmin r1 r0);        [ do 2 rewrite <- (Rplus_comm (Rmin r1 r0)); apply Rplus_lt_compat_l; assumption | apply Rplus_le_compat_l; apply Rmin_l ]     | discrR ] ]. elim H2; clear H2; intros; assert (H23 := H22 1%nat); simpl in H23;  assert (H24 := H23 (lt_n_S _ _ (lt_O_Sn _))); elim H24;  assumption. elim H2; intros; assert (H22 := H20 0%nat); simpl in H22;  assert (H23 := H22 (lt_O_Sn _)); elim H23; intro;  [ elim H24; rewrite <- H17; rewrite <- H19; reflexivity | elim H24; rewrite <- H17; assumption ]. elim H2; clear H2; intros; assert (H17 := H16 0%nat); simpl in H17;  elim (H17 (lt_O_Sn _)); assumption. rewrite <- H0; rewrite H12; apply (H7 0%nat); simpl in |- *; apply lt_O_Sn. Qed. Lemma StepFun_P12 :  forall (a b:R) (f:R -> R) (l lf:Rlist),    adapted_couple_opt f a b l lf -> adapted_couple_opt f b a l lf. unfold adapted_couple_opt in |- *; unfold adapted_couple in |- *; intros;  decompose [and] H; clear H; repeat split; try assumption. rewrite H0; unfold Rmin in |- *; case (Rle_dec a b); intro;  case (Rle_dec b a); intro; try reflexivity. apply Rle_antisym; assumption. apply Rle_antisym; auto with real. rewrite H3; unfold Rmax in |- *; case (Rle_dec a b); intro;  case (Rle_dec b a); intro; try reflexivity. apply Rle_antisym; assumption. apply Rle_antisym; auto with real. Qed. Lemma StepFun_P13 :  forall (a b r r1 r3 s1 s2 r4:R) (r2 lf1 s3 lf2:Rlist)    (f:R -> R),    a <> b ->    adapted_couple f a b (cons r (cons r1 r2)) (cons r3 lf1) ->    adapted_couple_opt f a b (cons s1 (cons s2 s3)) (cons r4 lf2) -> r1 <= s2. intros; case (total_order_T a b); intro. elim s; intro. eapply StepFun_P11; [ apply a0 | apply H0 | apply H1 ]. elim H; assumption. eapply StepFun_P11;  [ apply r0 | apply StepFun_P2; apply H0 | apply StepFun_P12; apply H1 ]. Qed. Lemma StepFun_P14 :  forall (f:R -> R) (l1 l2 lf1 lf2:Rlist) (a b:R),    a <= b ->    adapted_couple f a b l1 lf1 ->    adapted_couple_opt f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2. simple induction l1. intros l2 lf1 lf2 a b Hyp H H0; unfold adapted_couple in H; decompose [and] H;  clear H H0 H2 H3 H1 H6; simpl in H4; discriminate. simple induction r0. intros; case (Req_dec a b); intro. unfold adapted_couple_opt in H2; elim H2; intros; rewrite (StepFun_P8 H4 H3);  rewrite (StepFun_P8 H1 H3); reflexivity. assert (H4 := StepFun_P9 H1 H3); simpl in H4;  elim (le_Sn_O _ (le_S_n _ _ H4)). intros; clear H; unfold adapted_couple_opt in H3; elim H3; clear H3; intros;  case (Req_dec a b); intro. rewrite (StepFun_P8 H2 H4); rewrite (StepFun_P8 H H4); reflexivity. assert (Hyp_min : Rmin a b = a). unfold Rmin in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. assert (Hyp_max : Rmax a b = b). unfold Rmax in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. elim (RList_P20 _ (StepFun_P9 H H4)); intros s1 [s2 [s3 H5]]; rewrite H5 in H;  rewrite H5; induction lf1 as [| r3 lf1 Hreclf1]. unfold adapted_couple in H2; decompose [and] H2;  clear H H2 H4 H5 H3 H6 H8 H7 H11; simpl in H9; discriminate. clear Hreclf1; induction lf2 as [| r4 lf2 Hreclf2]. unfold adapted_couple in H; decompose [and] H;  clear H H2 H4 H5 H3 H6 H8 H7 H11; simpl in H9; discriminate. clear Hreclf2; assert (H6 : r = s1). unfold adapted_couple in H, H2; decompose [and] H; decompose [and] H2;  clear H H2; simpl in H13; simpl in H8; rewrite H13;  rewrite H8; reflexivity. assert (H7 : r3 = r4 \/ r = r1). case (Req_dec r r1); intro. right; assumption. left; cut (r1 <= s2). intro; unfold adapted_couple in H2, H; decompose [and] H; decompose [and] H2;  clear H H2; set (x := (r + r1) / 2); assert (H18 := H14 0%nat);  assert (H20 := H19 0%nat); unfold constant_D_eq, open_interval in H18, H20;  simpl in H18; simpl in H20; rewrite <- (H18 (lt_O_Sn _) x). rewrite <- (H20 (lt_O_Sn _) x). reflexivity. assert (H21 := H13 0%nat (lt_O_Sn _)); simpl in H21; elim H21; intro;  [ idtac | elim H7; assumption ]; unfold x in |- *;  split. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; apply H | discrR ] ]. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite <- (Rplus_comm r1); rewrite double; apply Rplus_lt_compat_l; apply H | discrR ] ]. rewrite <- H6; assert (H21 := H13 0%nat (lt_O_Sn _)); simpl in H21; elim H21;  intro; [ idtac | elim H7; assumption ]; unfold x in |- *;  split. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; apply H | discrR ] ]. apply Rlt_le_trans with r1;  [ apply Rmult_lt_reg_l with 2;     [ prove_sup0     | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2));        rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym;        [ rewrite Rmult_1_l; rewrite <- (Rplus_comm r1); rewrite double; apply Rplus_lt_compat_l; apply H | discrR ] ]  | assumption ]. eapply StepFun_P13. apply H4. apply H2. unfold adapted_couple_opt in |- *; split. apply H. rewrite H5 in H3; apply H3. assert (H8 : r1 <= s2). eapply StepFun_P13. apply H4. apply H2. unfold adapted_couple_opt in |- *; split. apply H. rewrite H5 in H3; apply H3. elim H7; intro. simpl in |- *; elim H8; intro. replace (r4 * (s2 - s1)) with (r3 * (r1 - r) + r3 * (s2 - r1));  [ idtac | rewrite H9; rewrite H6; ring ]. rewrite Rplus_assoc; apply Rplus_eq_compat_l;  change    (Int_SF lf1 (cons r1 r2) = Int_SF (cons r3 lf2) (cons r1 (cons s2 s3)))   in |- *; apply H0 with r1 b. unfold adapted_couple in H2; decompose [and] H2; clear H2;  replace b with (Rmax a b). rewrite <- H12; apply RList_P7;  [ assumption | simpl in |- *; right; left; reflexivity ]. eapply StepFun_P7. apply H1. apply H2. unfold adapted_couple_opt in |- *; split. apply StepFun_P7 with a a r3. apply H1. unfold adapted_couple in H2, H; decompose [and] H2; decompose [and] H;  clear H H2; assert (H20 : r = a). simpl in H13; rewrite H13; apply Hyp_min. unfold adapted_couple in |- *; repeat split. unfold ordered_Rlist in |- *; intros; simpl in H; induction i as [| i Hreci]. simpl in |- *; rewrite <- H20; apply (H11 0%nat). simpl in |- *; apply lt_O_Sn. induction i as [| i Hreci0]. simpl in |- *; assumption. change (pos_Rl (cons s2 s3) i <= pos_Rl (cons s2 s3) (S i)) in |- *;  apply (H15 (S i)); simpl in |- *; apply lt_S_n; assumption. simpl in |- *; symmetry in |- *; apply Hyp_min. rewrite <- H17; reflexivity. simpl in H19; simpl in |- *; rewrite H19; reflexivity. intros; simpl in H; unfold constant_D_eq, open_interval in |- *; intros;  induction i as [| i Hreci]. simpl in |- *; apply (H16 0%nat). simpl in |- *; apply lt_O_Sn. simpl in H2; rewrite <- H20 in H2; unfold open_interval in |- *;  simpl in |- *; apply H2. clear Hreci; induction i as [| i Hreci]. simpl in |- *; simpl in H2; rewrite H9; apply (H21 0%nat). simpl in |- *; apply lt_O_Sn. unfold open_interval in |- *; simpl in |- *; elim H2; intros; split. apply Rle_lt_trans with r1; try assumption; rewrite <- H6; apply (H11 0%nat);  simpl in |- *; apply lt_O_Sn. assumption. clear Hreci; simpl in |- *; apply (H21 (S i)). simpl in |- *; apply lt_S_n; assumption. unfold open_interval in |- *; apply H2. elim H3; clear H3; intros; split. rewrite H9;  change    (forall i:nat,       (i < pred (Rlength (cons r4 lf2)))%nat ->       pos_Rl (cons r4 lf2) i <> pos_Rl (cons r4 lf2) (S i) \/       f (pos_Rl (cons s1 (cons s2 s3)) (S i)) <> pos_Rl (cons r4 lf2) i)   in |- *; rewrite <- H5; apply H3. rewrite H5 in H11; intros; simpl in H12; induction i as [| i Hreci]. simpl in |- *; red in |- *; intro; rewrite H13 in H10;  elim (Rlt_irrefl _ H10). clear Hreci; apply (H11 (S i)); simpl in |- *; apply H12. rewrite H9; rewrite H10; rewrite H6; apply Rplus_eq_compat_l; rewrite <- H10;  apply H0 with r1 b. unfold adapted_couple in H2; decompose [and] H2; clear H2;  replace b with (Rmax a b). rewrite <- H12; apply RList_P7;  [ assumption | simpl in |- *; right; left; reflexivity ]. eapply StepFun_P7. apply H1. apply H2. unfold adapted_couple_opt in |- *; split. apply StepFun_P7 with a a r3. apply H1. unfold adapted_couple in H2, H; decompose [and] H2; decompose [and] H;  clear H H2; assert (H20 : r = a). simpl in H13; rewrite H13; apply Hyp_min. unfold adapted_couple in |- *; repeat split. unfold ordered_Rlist in |- *; intros; simpl in H; induction i as [| i Hreci]. simpl in |- *; rewrite <- H20; apply (H11 0%nat); simpl in |- *;  apply lt_O_Sn. rewrite H10; apply (H15 (S i)); simpl in |- *; assumption. simpl in |- *; symmetry in |- *; apply Hyp_min. rewrite <- H17; rewrite H10; reflexivity. simpl in H19; simpl in |- *; apply H19. intros; simpl in H; unfold constant_D_eq, open_interval in |- *; intros;  induction i as [| i Hreci]. simpl in |- *; apply (H16 0%nat). simpl in |- *; apply lt_O_Sn. simpl in H2; rewrite <- H20 in H2; unfold open_interval in |- *;  simpl in |- *; apply H2. clear Hreci; simpl in |- *; apply (H21 (S i)). simpl in |- *; assumption. rewrite <- H10; unfold open_interval in |- *; apply H2. elim H3; clear H3; intros; split. rewrite H5 in H3; intros; apply (H3 (S i)). simpl in |- *; replace (Rlength lf2) with (S (pred (Rlength lf2))). apply lt_n_S; apply H12. symmetry in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *;  intro; rewrite <- H13 in H12; elim (lt_n_O _ H12). intros; simpl in H12; rewrite H10; rewrite H5 in H11; apply (H11 (S i));  simpl in |- *; apply lt_n_S; apply H12. simpl in |- *; rewrite H9; unfold Rminus in |- *; rewrite Rplus_opp_r;  rewrite Rmult_0_r; rewrite Rplus_0_l;  change    (Int_SF lf1 (cons r1 r2) = Int_SF (cons r4 lf2) (cons s1 (cons s2 s3)))   in |- *; eapply H0. apply H1. 2: rewrite H5 in H3; unfold adapted_couple_opt in |- *; split; assumption. assert (H10 : r = a). unfold adapted_couple in H2; decompose [and] H2; clear H2; simpl in H12;  rewrite H12; apply Hyp_min. rewrite <- H9; rewrite H10; apply StepFun_P7 with a r r3;  [ apply H1 | pattern a at 2 in |- *; rewrite <- H10; pattern r at 2 in |- *; rewrite H9; apply H2 ]. Qed. Lemma StepFun_P15 :  forall (f:R -> R) (l1 l2 lf1 lf2:Rlist) (a b:R),    adapted_couple f a b l1 lf1 ->    adapted_couple_opt f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2. intros; case (Rle_dec a b); intro;  [ apply (StepFun_P14 r H H0)  | assert (H1 : b <= a);     [ auto with real     | eapply StepFun_P14;        [ apply H1 | apply StepFun_P2; apply H | apply StepFun_P12; apply H0 ] ] ]. Qed. Lemma StepFun_P16 :  forall (f:R -> R) (l lf:Rlist) (a b:R),    adapted_couple f a b l lf ->     exists l' : Rlist,      (exists lf' : Rlist, adapted_couple_opt f a b l' lf'). intros; case (Rle_dec a b); intro;  [ apply (StepFun_P10 r H)  | assert (H1 : b <= a);     [ auto with real     | assert (H2 := StepFun_P10 H1 (StepFun_P2 H)); elim H2;        intros l' [lf' H3]; exists l'; exists lf'; apply StepFun_P12;        assumption ] ]. Qed. Lemma StepFun_P17 :  forall (f:R -> R) (l1 l2 lf1 lf2:Rlist) (a b:R),    adapted_couple f a b l1 lf1 ->    adapted_couple f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2. intros; elim (StepFun_P16 H); intros l' [lf' H1]; rewrite (StepFun_P15 H H1);  rewrite (StepFun_P15 H0 H1); reflexivity. Qed. Lemma StepFun_P18 :  forall a b c:R, RiemannInt_SF (mkStepFun (StepFun_P4 a b c)) = c * (b - a). intros; unfold RiemannInt_SF in |- *; case (Rle_dec a b); intro. replace  (Int_SF (subdivision_val (mkStepFun (StepFun_P4 a b c)))     (subdivision (mkStepFun (StepFun_P4 a b c)))) with  (Int_SF (cons c nil) (cons a (cons b nil)));  [ simpl in |- *; ring  | apply StepFun_P17 with (fct_cte c) a b;     [ apply StepFun_P3; assumption | apply (StepFun_P1 (mkStepFun (StepFun_P4 a b c))) ] ]. replace  (Int_SF (subdivision_val (mkStepFun (StepFun_P4 a b c)))     (subdivision (mkStepFun (StepFun_P4 a b c)))) with  (Int_SF (cons c nil) (cons b (cons a nil)));  [ simpl in |- *; ring  | apply StepFun_P17 with (fct_cte c) a b;     [ apply StepFun_P2; apply StepFun_P3; auto with real | apply (StepFun_P1 (mkStepFun (StepFun_P4 a b c))) ] ]. Qed. Lemma StepFun_P19 :  forall (l1:Rlist) (f g:R -> R) (l:R),    Int_SF (FF l1 (fun x:R => f x + l * g x)) l1 =    Int_SF (FF l1 f) l1 + l * Int_SF (FF l1 g) l1. intros; induction l1 as [| r l1 Hrecl1];  [ simpl in |- *; ring  | induction l1 as [| r0 l1 Hrecl0]; simpl in |- *;     [ ring | simpl in Hrecl1; rewrite Hrecl1; ring ] ]. Qed. Lemma StepFun_P20 :  forall (l:Rlist) (f:R -> R),    (0 < Rlength l)%nat -> Rlength l = S (Rlength (FF l f)). intros l f H; induction l;  [ elim (lt_irrefl _ H) | simpl in |- *; rewrite RList_P18; rewrite RList_P14; reflexivity ]. Qed. Lemma StepFun_P21 :  forall (a b:R) (f:R -> R) (l:Rlist),    is_subdivision f a b l -> adapted_couple f a b l (FF l f). intros; unfold adapted_couple in |- *; unfold is_subdivision in X;  unfold adapted_couple in X; elim X; clear X; intros;  decompose [and] p; clear p; repeat split; try assumption. apply StepFun_P20; rewrite H2; apply lt_O_Sn. intros; assert (H5 := H4 _ H3); unfold constant_D_eq, open_interval in H5;  unfold constant_D_eq, open_interval in |- *; intros;  induction l as [| r l Hrecl]. discriminate. unfold FF in |- *; rewrite RList_P12. simpl in |- *;  change (f x0 = f (pos_Rl (mid_Rlist (cons r l) r) (S i))) in |- *;  rewrite RList_P13; try assumption; rewrite (H5 x0 H6);  rewrite H5. reflexivity. split. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; elim H6; intros; apply Rlt_trans with x0; assumption | discrR ] ]. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite double; rewrite (Rplus_comm (pos_Rl (cons r l) i)); apply Rplus_lt_compat_l; elim H6; intros; apply Rlt_trans with x0; assumption | discrR ] ]. rewrite RList_P14; simpl in H3; apply H3. Qed. Lemma StepFun_P22 :  forall (a b:R) (f g:R -> R) (lf lg:Rlist),    a <= b ->    is_subdivision f a b lf ->    is_subdivision g a b lg -> is_subdivision f a b (cons_ORlist lf lg). unfold is_subdivision in |- *; intros a b f g lf lg Hyp X X0; elim X; elim X0;  clear X X0; intros lg0 p lf0 p0; assert (Hyp_min : Rmin a b = a). unfold Rmin in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. assert (Hyp_max : Rmax a b = b). unfold Rmax in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. apply existT with (FF (cons_ORlist lf lg) f); unfold adapted_couple in p, p0;  decompose [and] p; decompose [and] p0; clear p p0;  rewrite Hyp_min in H6; rewrite Hyp_min in H1; rewrite Hyp_max in H0;  rewrite Hyp_max in H5; unfold adapted_couple in |- *;  repeat split. apply RList_P2; assumption. rewrite Hyp_min; symmetry in |- *; apply Rle_antisym. induction lf as [| r lf Hreclf]. simpl in |- *; right; symmetry in |- *; assumption. assert  (H10 :   In (pos_Rl (cons_ORlist (cons r lf) lg) 0) (cons_ORlist (cons r lf) lg)). elim  (RList_P3 (cons_ORlist (cons r lf) lg)     (pos_Rl (cons_ORlist (cons r lf) lg) 0)); intros _ H10;  apply H10; exists 0%nat; split;  [ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_O_Sn ]. elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) 0));  intros H12 _; assert (H13 := H12 H10); elim H13; intro. elim (RList_P3 (cons r lf) (pos_Rl (cons_ORlist (cons r lf) lg) 0));  intros H11 _; assert (H14 := H11 H8); elim H14; intros;  elim H15; clear H15; intros; rewrite H15; rewrite <- H6;  elim (RList_P6 (cons r lf)); intros; apply H17;  [ assumption | apply le_O_n | assumption ]. elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) 0)); intros H11 _;  assert (H14 := H11 H8); elim H14; intros; elim H15;  clear H15; intros; rewrite H15; rewrite <- H1; elim (RList_P6 lg);  intros; apply H17; [ assumption | apply le_O_n | assumption ]. induction lf as [| r lf Hreclf]. simpl in |- *; right; assumption. assert (H8 : In a (cons_ORlist (cons r lf) lg)). elim (RList_P9 (cons r lf) lg a); intros; apply H10; left;  elim (RList_P3 (cons r lf) a); intros; apply H12;  exists 0%nat; split;  [ symmetry in |- *; assumption | simpl in |- *; apply lt_O_Sn ]. apply RList_P5; [ apply RList_P2; assumption | assumption ]. rewrite Hyp_max; apply Rle_antisym. induction lf as [| r lf Hreclf]. simpl in |- *; right; assumption. assert  (H8 :   In     (pos_Rl (cons_ORlist (cons r lf) lg)        (pred (Rlength (cons_ORlist (cons r lf) lg))))     (cons_ORlist (cons r lf) lg)). elim  (RList_P3 (cons_ORlist (cons r lf) lg)     (pos_Rl (cons_ORlist (cons r lf) lg)        (pred (Rlength (cons_ORlist (cons r lf) lg)))));  intros _ H10; apply H10;  exists (pred (Rlength (cons_ORlist (cons r lf) lg)));  split; [ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_n_Sn ]. elim  (RList_P9 (cons r lf) lg     (pos_Rl (cons_ORlist (cons r lf) lg)        (pred (Rlength (cons_ORlist (cons r lf) lg)))));  intros H10 _. assert (H11 := H10 H8); elim H11; intro. elim  (RList_P3 (cons r lf)     (pos_Rl (cons_ORlist (cons r lf) lg)        (pred (Rlength (cons_ORlist (cons r lf) lg)))));  intros H13 _; assert (H14 := H13 H12); elim H14; intros;  elim H15; clear H15; intros; rewrite H15; rewrite <- H5;  elim (RList_P6 (cons r lf)); intros; apply H17;  [ assumption | simpl in |- *; simpl in H14; apply lt_n_Sm_le; assumption | simpl in |- *; apply lt_n_Sn ]. elim  (RList_P3 lg     (pos_Rl (cons_ORlist (cons r lf) lg)        (pred (Rlength (cons_ORlist (cons r lf) lg)))));  intros H13 _; assert (H14 := H13 H12); elim H14; intros;  elim H15; clear H15; intros. rewrite H15; assert (H17 : Rlength lg = S (pred (Rlength lg))). apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;  rewrite <- H17 in H16; elim (lt_n_O _ H16). rewrite <- H0; elim (RList_P6 lg); intros; apply H18;  [ assumption | rewrite H17 in H16; apply lt_n_Sm_le; assumption | apply lt_pred_n_n; rewrite H17; apply lt_O_Sn ]. induction lf as [| r lf Hreclf]. simpl in |- *; right; symmetry in |- *; assumption. assert (H8 : In b (cons_ORlist (cons r lf) lg)). elim (RList_P9 (cons r lf) lg b); intros; apply H10; left;  elim (RList_P3 (cons r lf) b); intros; apply H12;  exists (pred (Rlength (cons r lf))); split;  [ symmetry in |- *; assumption | simpl in |- *; apply lt_n_Sn ]. apply RList_P7; [ apply RList_P2; assumption | assumption ]. apply StepFun_P20; rewrite RList_P11; rewrite H2; rewrite H7; simpl in |- *;  apply lt_O_Sn. intros; unfold constant_D_eq, open_interval in |- *; intros;  cut   (exists l : R,      constant_D_eq f        (open_interval (pos_Rl (cons_ORlist lf lg) i)           (pos_Rl (cons_ORlist lf lg) (S i))) l). intros; elim H11; clear H11; intros; assert (H12 := H11);  assert   (Hyp_cons :     exists r : R, (exists r0 : Rlist, cons_ORlist lf lg = cons r r0)). apply RList_P19; red in |- *; intro; rewrite H13 in H8; elim (lt_n_O _ H8). elim Hyp_cons; clear Hyp_cons; intros r [r0 Hyp_cons]; rewrite Hyp_cons;  unfold FF in |- *; rewrite RList_P12. change (f x = f (pos_Rl (mid_Rlist (cons r r0) r) (S i))) in |- *;  rewrite <- Hyp_cons; rewrite RList_P13. assert (H13 := RList_P2 _ _ H _ H8); elim H13; intro. unfold constant_D_eq, open_interval in H11, H12; rewrite (H11 x H10);  assert   (H15 :    pos_Rl (cons_ORlist lf lg) i <    (pos_Rl (cons_ORlist lf lg) i + pos_Rl (cons_ORlist lf lg) (S i)) / 2 <    pos_Rl (cons_ORlist lf lg) (S i)). split. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite double; rewrite (Rplus_comm (pos_Rl (cons_ORlist lf lg) i)); apply Rplus_lt_compat_l; assumption | discrR ] ]. rewrite (H11 _ H15); reflexivity. elim H10; intros; rewrite H14 in H15;  elim (Rlt_irrefl _ (Rlt_trans _ _ _ H16 H15)). apply H8. rewrite RList_P14; rewrite Hyp_cons in H8; simpl in H8; apply H8. assert (H11 : a < b). apply Rle_lt_trans with (pos_Rl (cons_ORlist lf lg) i). rewrite <- H6; rewrite <- (RList_P15 lf lg). elim (RList_P6 (cons_ORlist lf lg)); intros; apply H11. apply RList_P2; assumption. apply le_O_n. apply lt_trans with (pred (Rlength (cons_ORlist lf lg)));  [ assumption | apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H8; elim (lt_n_O _ H8) ]. assumption. assumption. rewrite H1; assumption. apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)). elim H10; intros; apply Rlt_trans with x; assumption. rewrite <- H5; rewrite <- (RList_P16 lf lg); try assumption. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H11. apply RList_P2; assumption. apply lt_n_Sm_le; apply lt_n_S; assumption. apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H8;  elim (lt_n_O _ H8). rewrite H0; assumption. set  (I :=   fun j:nat =>     pos_Rl lf j <= pos_Rl (cons_ORlist lf lg) i /\ (j < Rlength lf)%nat);  assert (H12 : Nbound I). unfold Nbound in |- *; exists (Rlength lf); intros; unfold I in H12; elim H12;  intros; apply lt_le_weak; assumption. assert (H13 : exists n : nat, I n). exists 0%nat; unfold I in |- *; split. apply Rle_trans with (pos_Rl (cons_ORlist lf lg) 0). right; symmetry in |- *. apply RList_P15; try assumption; rewrite H1; assumption. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H13. apply RList_P2; assumption. apply le_O_n. apply lt_trans with (pred (Rlength (cons_ORlist lf lg))). assumption. apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H15 in H8;  elim (lt_n_O _ H8). apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H5;  rewrite <- H6 in H11; rewrite <- H5 in H11; elim (Rlt_irrefl _ H11). assert (H14 := Nzorn H13 H12); elim H14; clear H14; intros x0 H14;  exists (pos_Rl lf0 x0); unfold constant_D_eq, open_interval in |- *;  intros; assert (H16 := H9 x0); assert (H17 : (x0 < pred (Rlength lf))%nat). elim H14; clear H14; intros; unfold I in H14; elim H14; clear H14; intros;  apply lt_S_n; replace (S (pred (Rlength lf))) with (Rlength lf). inversion H18. 2: apply lt_n_S; assumption. cut (x0 = pred (Rlength lf)). intro; rewrite H19 in H14; rewrite H5 in H14;  cut (pos_Rl (cons_ORlist lf lg) i < b). intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H21)). apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)). elim H10; intros; apply Rlt_trans with x; assumption. rewrite <- H5;  apply Rle_trans with   (pos_Rl (cons_ORlist lf lg) (pred (Rlength (cons_ORlist lf lg)))). elim (RList_P6 (cons_ORlist lf lg)); intros; apply H21. apply RList_P2; assumption. apply lt_n_Sm_le; apply lt_n_S; assumption. apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H23 in H8;  elim (lt_n_O _ H8). right; apply RList_P16; try assumption; rewrite H0; assumption. rewrite <- H20; reflexivity. apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;  rewrite <- H19 in H18; elim (lt_n_O _ H18). assert (H18 := H16 H17); unfold constant_D_eq, open_interval in H18;  rewrite (H18 x1). reflexivity. elim H15; clear H15; intros; elim H14; clear H14; intros; unfold I in H14;  elim H14; clear H14; intros; split. apply Rle_lt_trans with (pos_Rl (cons_ORlist lf lg) i); assumption. apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)); try assumption. assert (H22 : (S x0 < Rlength lf)%nat). replace (Rlength lf) with (S (pred (Rlength lf)));  [ apply lt_n_S; assumption | symmetry in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro; rewrite <- H22 in H21; elim (lt_n_O _ H21) ]. elim (Rle_dec (pos_Rl lf (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro. assert (H23 : (S x0 <= x0)%nat). apply H20; unfold I in |- *; split; assumption. elim (le_Sn_n _ H23). assert (H23 : pos_Rl (cons_ORlist lf lg) i < pos_Rl lf (S x0)). auto with real. clear b0; apply RList_P17; try assumption. apply RList_P2; assumption. elim (RList_P9 lf lg (pos_Rl lf (S x0))); intros; apply H25; left;  elim (RList_P3 lf (pos_Rl lf (S x0))); intros; apply H27;  exists (S x0); split; [ reflexivity | apply H22 ]. Qed. Lemma StepFun_P23 :  forall (a b:R) (f g:R -> R) (lf lg:Rlist),    is_subdivision f a b lf ->    is_subdivision g a b lg -> is_subdivision f a b (cons_ORlist lf lg). intros; case (Rle_dec a b); intro;  [ apply StepFun_P22 with g; assumption  | apply StepFun_P5; apply StepFun_P22 with g;     [ auto with real | apply StepFun_P5; assumption | apply StepFun_P5; assumption ] ]. Qed. Lemma StepFun_P24 :  forall (a b:R) (f g:R -> R) (lf lg:Rlist),    a <= b ->    is_subdivision f a b lf ->    is_subdivision g a b lg -> is_subdivision g a b (cons_ORlist lf lg). unfold is_subdivision in |- *; intros a b f g lf lg Hyp X X0; elim X; elim X0;  clear X X0; intros lg0 p lf0 p0; assert (Hyp_min : Rmin a b = a). unfold Rmin in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. assert (Hyp_max : Rmax a b = b). unfold Rmax in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. apply existT with (FF (cons_ORlist lf lg) g); unfold adapted_couple in p, p0;  decompose [and] p; decompose [and] p0; clear p p0;  rewrite Hyp_min in H1; rewrite Hyp_min in H6; rewrite Hyp_max in H0;  rewrite Hyp_max in H5; unfold adapted_couple in |- *;  repeat split. apply RList_P2; assumption. rewrite Hyp_min; symmetry in |- *; apply Rle_antisym. induction lf as [| r lf Hreclf]. simpl in |- *; right; symmetry in |- *; assumption. assert  (H10 :   In (pos_Rl (cons_ORlist (cons r lf) lg) 0) (cons_ORlist (cons r lf) lg)). elim  (RList_P3 (cons_ORlist (cons r lf) lg)     (pos_Rl (cons_ORlist (cons r lf) lg) 0)); intros _ H10;  apply H10; exists 0%nat; split;  [ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_O_Sn ]. elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) 0));  intros H12 _; assert (H13 := H12 H10); elim H13; intro. elim (RList_P3 (cons r lf) (pos_Rl (cons_ORlist (cons r lf) lg) 0));  intros H11 _; assert (H14 := H11 H8); elim H14; intros;  elim H15; clear H15; intros; rewrite H15; rewrite <- H6;  elim (RList_P6 (cons r lf)); intros; apply H17;  [ assumption | apply le_O_n | assumption ]. elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) 0)); intros H11 _;  assert (H14 := H11 H8); elim H14; intros; elim H15;  clear H15; intros; rewrite H15; rewrite <- H1; elim (RList_P6 lg);  intros; apply H17; [ assumption | apply le_O_n | assumption ]. induction lf as [| r lf Hreclf]. simpl in |- *; right; assumption. assert (H8 : In a (cons_ORlist (cons r lf) lg)). elim (RList_P9 (cons r lf) lg a); intros; apply H10; left;  elim (RList_P3 (cons r lf) a); intros; apply H12;  exists 0%nat; split;  [ symmetry in |- *; assumption | simpl in |- *; apply lt_O_Sn ]. apply RList_P5; [ apply RList_P2; assumption | assumption ]. rewrite Hyp_max; apply Rle_antisym. induction lf as [| r lf Hreclf]. simpl in |- *; right; assumption. assert  (H8 :   In     (pos_Rl (cons_ORlist (cons r lf) lg)        (pred (Rlength (cons_ORlist (cons r lf) lg))))     (cons_ORlist (cons r lf) lg)). elim  (RList_P3 (cons_ORlist (cons r lf) lg)     (pos_Rl (cons_ORlist (cons r lf) lg)        (pred (Rlength (cons_ORlist (cons r lf) lg)))));  intros _ H10; apply H10;  exists (pred (Rlength (cons_ORlist (cons r lf) lg)));  split; [ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_n_Sn ]. elim  (RList_P9 (cons r lf) lg     (pos_Rl (cons_ORlist (cons r lf) lg)        (pred (Rlength (cons_ORlist (cons r lf) lg)))));  intros H10 _; assert (H11 := H10 H8); elim H11; intro. elim  (RList_P3 (cons r lf)     (pos_Rl (cons_ORlist (cons r lf) lg)        (pred (Rlength (cons_ORlist (cons r lf) lg)))));  intros H13 _; assert (H14 := H13 H12); elim H14; intros;  elim H15; clear H15; intros; rewrite H15; rewrite <- H5;  elim (RList_P6 (cons r lf)); intros; apply H17;  [ assumption | simpl in |- *; simpl in H14; apply lt_n_Sm_le; assumption | simpl in |- *; apply lt_n_Sn ]. elim  (RList_P3 lg     (pos_Rl (cons_ORlist (cons r lf) lg)        (pred (Rlength (cons_ORlist (cons r lf) lg)))));  intros H13 _; assert (H14 := H13 H12); elim H14; intros;  elim H15; clear H15; intros; rewrite H15;  assert (H17 : Rlength lg = S (pred (Rlength lg))). apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;  rewrite <- H17 in H16; elim (lt_n_O _ H16). rewrite <- H0; elim (RList_P6 lg); intros; apply H18;  [ assumption | rewrite H17 in H16; apply lt_n_Sm_le; assumption | apply lt_pred_n_n; rewrite H17; apply lt_O_Sn ]. induction lf as [| r lf Hreclf]. simpl in |- *; right; symmetry in |- *; assumption. assert (H8 : In b (cons_ORlist (cons r lf) lg)). elim (RList_P9 (cons r lf) lg b); intros; apply H10; left;  elim (RList_P3 (cons r lf) b); intros; apply H12;  exists (pred (Rlength (cons r lf))); split;  [ symmetry in |- *; assumption | simpl in |- *; apply lt_n_Sn ]. apply RList_P7; [ apply RList_P2; assumption | assumption ]. apply StepFun_P20; rewrite RList_P11; rewrite H7; rewrite H2; simpl in |- *;  apply lt_O_Sn. unfold constant_D_eq, open_interval in |- *; intros;  cut   (exists l : R,      constant_D_eq g        (open_interval (pos_Rl (cons_ORlist lf lg) i)           (pos_Rl (cons_ORlist lf lg) (S i))) l). intros; elim H11; clear H11; intros; assert (H12 := H11);  assert   (Hyp_cons :     exists r : R, (exists r0 : Rlist, cons_ORlist lf lg = cons r r0)). apply RList_P19; red in |- *; intro; rewrite H13 in H8; elim (lt_n_O _ H8). elim Hyp_cons; clear Hyp_cons; intros r [r0 Hyp_cons]; rewrite Hyp_cons;  unfold FF in |- *; rewrite RList_P12. change (g x = g (pos_Rl (mid_Rlist (cons r r0) r) (S i))) in |- *;  rewrite <- Hyp_cons; rewrite RList_P13. assert (H13 := RList_P2 _ _ H _ H8); elim H13; intro. unfold constant_D_eq, open_interval in H11, H12; rewrite (H11 x H10);  assert   (H15 :    pos_Rl (cons_ORlist lf lg) i <    (pos_Rl (cons_ORlist lf lg) i + pos_Rl (cons_ORlist lf lg) (S i)) / 2 <    pos_Rl (cons_ORlist lf lg) (S i)). split. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite double; rewrite (Rplus_comm (pos_Rl (cons_ORlist lf lg) i)); apply Rplus_lt_compat_l; assumption | discrR ] ]. rewrite (H11 _ H15); reflexivity. elim H10; intros; rewrite H14 in H15;  elim (Rlt_irrefl _ (Rlt_trans _ _ _ H16 H15)). apply H8. rewrite RList_P14; rewrite Hyp_cons in H8; simpl in H8; apply H8. assert (H11 : a < b). apply Rle_lt_trans with (pos_Rl (cons_ORlist lf lg) i). rewrite <- H6; rewrite <- (RList_P15 lf lg); try assumption. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H11. apply RList_P2; assumption. apply le_O_n. apply lt_trans with (pred (Rlength (cons_ORlist lf lg)));  [ assumption | apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H8; elim (lt_n_O _ H8) ]. rewrite H1; assumption. apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)). elim H10; intros; apply Rlt_trans with x; assumption. rewrite <- H5; rewrite <- (RList_P16 lf lg); try assumption. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H11. apply RList_P2; assumption. apply lt_n_Sm_le; apply lt_n_S; assumption. apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H8;  elim (lt_n_O _ H8). rewrite H0; assumption. set  (I :=   fun j:nat =>     pos_Rl lg j <= pos_Rl (cons_ORlist lf lg) i /\ (j < Rlength lg)%nat);  assert (H12 : Nbound I). unfold Nbound in |- *; exists (Rlength lg); intros; unfold I in H12; elim H12;  intros; apply lt_le_weak; assumption. assert (H13 : exists n : nat, I n). exists 0%nat; unfold I in |- *; split. apply Rle_trans with (pos_Rl (cons_ORlist lf lg) 0). right; symmetry in |- *; rewrite H1; rewrite <- H6; apply RList_P15;  try assumption; rewrite H1; assumption. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H13;  [ apply RList_P2; assumption  | apply le_O_n  | apply lt_trans with (pred (Rlength (cons_ORlist lf lg)));     [ assumption | apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H15 in H8; elim (lt_n_O _ H8) ] ]. apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H0;  rewrite <- H1 in H11; rewrite <- H0 in H11; elim (Rlt_irrefl _ H11). assert (H14 := Nzorn H13 H12); elim H14; clear H14; intros x0 H14;  exists (pos_Rl lg0 x0); unfold constant_D_eq, open_interval in |- *;  intros; assert (H16 := H4 x0); assert (H17 : (x0 < pred (Rlength lg))%nat). elim H14; clear H14; intros; unfold I in H14; elim H14; clear H14; intros;  apply lt_S_n; replace (S (pred (Rlength lg))) with (Rlength lg). inversion H18. 2: apply lt_n_S; assumption. cut (x0 = pred (Rlength lg)). intro; rewrite H19 in H14; rewrite H0 in H14;  cut (pos_Rl (cons_ORlist lf lg) i < b). intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H21)). apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)). elim H10; intros; apply Rlt_trans with x; assumption. rewrite <- H0;  apply Rle_trans with   (pos_Rl (cons_ORlist lf lg) (pred (Rlength (cons_ORlist lf lg)))). elim (RList_P6 (cons_ORlist lf lg)); intros; apply H21. apply RList_P2; assumption. apply lt_n_Sm_le; apply lt_n_S; assumption. apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H23 in H8;  elim (lt_n_O _ H8). right; rewrite H0; rewrite <- H5; apply RList_P16; try assumption. rewrite H0; assumption. rewrite <- H20; reflexivity. apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;  rewrite <- H19 in H18; elim (lt_n_O _ H18). assert (H18 := H16 H17); unfold constant_D_eq, open_interval in H18;  rewrite (H18 x1). reflexivity. elim H15; clear H15; intros; elim H14; clear H14; intros; unfold I in H14;  elim H14; clear H14; intros; split. apply Rle_lt_trans with (pos_Rl (cons_ORlist lf lg) i); assumption. apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)); try assumption. assert (H22 : (S x0 < Rlength lg)%nat). replace (Rlength lg) with (S (pred (Rlength lg))). apply lt_n_S; assumption. symmetry in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *;  intro; rewrite <- H22 in H21; elim (lt_n_O _ H21). elim (Rle_dec (pos_Rl lg (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro. assert (H23 : (S x0 <= x0)%nat);  [ apply H20; unfold I in |- *; split; assumption | elim (le_Sn_n _ H23) ]. assert (H23 : pos_Rl (cons_ORlist lf lg) i < pos_Rl lg (S x0)). auto with real. clear b0; apply RList_P17; try assumption;  [ apply RList_P2; assumption  | elim (RList_P9 lf lg (pos_Rl lg (S x0))); intros; apply H25; right;     elim (RList_P3 lg (pos_Rl lg (S x0))); intros;     apply H27; exists (S x0); split; [ reflexivity | apply H22 ] ]. Qed. Lemma StepFun_P25 :  forall (a b:R) (f g:R -> R) (lf lg:Rlist),    is_subdivision f a b lf ->    is_subdivision g a b lg -> is_subdivision g a b (cons_ORlist lf lg). intros a b f g lf lg H H0; case (Rle_dec a b); intro;  [ apply StepFun_P24 with f; assumption  | apply StepFun_P5; apply StepFun_P24 with f;     [ auto with real | apply StepFun_P5; assumption | apply StepFun_P5; assumption ] ]. Qed. Lemma StepFun_P26 :  forall (a b l:R) (f g:R -> R) (l1:Rlist),    is_subdivision f a b l1 ->    is_subdivision g a b l1 ->    is_subdivision (fun x:R => f x + l * g x) a b l1. Proof. intros a b l f g l1 (x0,(H0,(H1,(H2,(H3,H4)))))                     (x,(_,(_,(_,(_,H9))))).  exists (FF l1 (fun x:R => f x + l * g x)); repeat split; try assumption. apply StepFun_P20; rewrite H3; auto with arith. intros i H8 x1 H10; unfold open_interval in H10, H9, H4;  rewrite (H9 _ H8 _ H10); rewrite (H4 _ H8 _ H10);  assert (H11 : l1 <> nil). red in |- *; intro H11; rewrite H11 in H8; elim (lt_n_O _ H8). destruct (RList_P19 _ H11) as (r,(r0,H12));  rewrite H12; unfold FF in |- *;  change    (pos_Rl x0 i + l * pos_Rl x i =     pos_Rl       (app_Rlist (mid_Rlist (cons r r0) r) (fun x2:R => f x2 + l * g x2))       (S i)) in |- *; rewrite RList_P12. rewrite RList_P13. rewrite <- H12; rewrite (H9 _ H8); try rewrite (H4 _ H8);  reflexivity ||    (elim H10; clear H10; intros; split;      [ apply Rmult_lt_reg_l with 2;         [ prove_sup0         | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2));            rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym;            [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; apply Rlt_trans with x1; assumption | discrR ] ]      | apply Rmult_lt_reg_l with 2;         [ prove_sup0         | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2));            rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym;            [ rewrite Rmult_1_l; rewrite double; rewrite (Rplus_comm (pos_Rl l1 i)); apply Rplus_lt_compat_l; apply Rlt_trans with x1; assumption | discrR ] ] ]). rewrite <- H12; assumption. rewrite RList_P14; simpl in |- *; rewrite H12 in H8; simpl in H8;  apply lt_n_S; apply H8. Qed. Lemma StepFun_P27 :  forall (a b l:R) (f g:R -> R) (lf lg:Rlist),    is_subdivision f a b lf ->    is_subdivision g a b lg ->    is_subdivision (fun x:R => f x + l * g x) a b (cons_ORlist lf lg). intros a b l f g lf lg H H0; apply StepFun_P26;  [ apply StepFun_P23 with g; assumption | apply StepFun_P25 with f; assumption ]. Qed. Lemma StepFun_P28 :  forall (a b l:R) (f g:StepFun a b), IsStepFun (fun x:R => f x + l * g x) a b. intros a b l f g; unfold IsStepFun in |- *; assert (H := pre f);  assert (H0 := pre g); unfold IsStepFun in H, H0; elim H;  elim H0; intros; apply existT with (cons_ORlist x0 x);  apply StepFun_P27; assumption. Qed. Lemma StepFun_P29 :  forall (a b:R) (f:StepFun a b), is_subdivision f a b (subdivision f). intros a b f; unfold is_subdivision in |- *;  apply existT with (subdivision_val f); apply StepFun_P1. Qed. Lemma StepFun_P30 :  forall (a b l:R) (f g:StepFun a b),    RiemannInt_SF (mkStepFun (StepFun_P28 l f g)) =    RiemannInt_SF f + l * RiemannInt_SF g. intros a b l f g; unfold RiemannInt_SF in |- *; case (Rle_dec a b);  (intro;    replace     (Int_SF (subdivision_val (mkStepFun (StepFun_P28 l f g)))        (subdivision (mkStepFun (StepFun_P28 l f g)))) with     (Int_SF        (FF (cons_ORlist (subdivision f) (subdivision g))           (fun x:R => f x + l * g x))        (cons_ORlist (subdivision f) (subdivision g)));    [ rewrite StepFun_P19;       replace        (Int_SF (FF (cons_ORlist (subdivision f) (subdivision g)) f)           (cons_ORlist (subdivision f) (subdivision g))) with        (Int_SF (subdivision_val f) (subdivision f));       [ replace          (Int_SF (FF (cons_ORlist (subdivision f) (subdivision g)) g)             (cons_ORlist (subdivision f) (subdivision g))) with          (Int_SF (subdivision_val g) (subdivision g));          [ ring          | apply StepFun_P17 with (fe g) a b;             [ apply StepFun_P1 | apply StepFun_P21; apply StepFun_P25 with (fe f); apply StepFun_P29 ] ]       | apply StepFun_P17 with (fe f) a b;          [ apply StepFun_P1 | apply StepFun_P21; apply StepFun_P23 with (fe g); apply StepFun_P29 ] ]    | apply StepFun_P17 with (fun x:R => f x + l * g x) a b;       [ apply StepFun_P21; apply StepFun_P27; apply StepFun_P29 | apply (StepFun_P1 (mkStepFun (StepFun_P28 l f g))) ] ]). Qed. Lemma StepFun_P31 :  forall (a b:R) (f:R -> R) (l lf:Rlist),    adapted_couple f a b l lf ->    adapted_couple (fun x:R => Rabs (f x)) a b l (app_Rlist lf Rabs). unfold adapted_couple in |- *; intros; decompose [and] H; clear H;  repeat split; try assumption. symmetry in |- *; rewrite H3; rewrite RList_P18; reflexivity. intros; unfold constant_D_eq, open_interval in |- *;  unfold constant_D_eq, open_interval in H5; intros;  rewrite (H5 _ H _ H4); rewrite RList_P12;  [ reflexivity | rewrite H3 in H; simpl in H; apply H ]. Qed. Lemma StepFun_P32 :  forall (a b:R) (f:StepFun a b), IsStepFun (fun x:R => Rabs (f x)) a b. intros a b f; unfold IsStepFun in |- *; apply existT with (subdivision f);  unfold is_subdivision in |- *;  apply existT with (app_Rlist (subdivision_val f) Rabs);  apply StepFun_P31; apply StepFun_P1. Qed. Lemma StepFun_P33 :  forall l2 l1:Rlist,    ordered_Rlist l1 -> Rabs (Int_SF l2 l1) <= Int_SF (app_Rlist l2 Rabs) l1. simple induction l2; intros. simpl in |- *; rewrite Rabs_R0; right; reflexivity. simpl in |- *; 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 in |- *; apply lt_O_Sn ]. Qed. Lemma StepFun_P34 :  forall (a b:R) (f:StepFun a b),    a <= b ->    Rabs (RiemannInt_SF f) <= RiemannInt_SF (mkStepFun (StepFun_P32 f)). intros; unfold RiemannInt_SF in |- *; case (Rle_dec a b); intro. replace  (Int_SF (subdivision_val (mkStepFun (StepFun_P32 f)))     (subdivision (mkStepFun (StepFun_P32 f)))) with  (Int_SF (app_Rlist (subdivision_val f) Rabs) (subdivision f)). apply StepFun_P33; assert (H0 := StepFun_P29 f); unfold is_subdivision in H0;  elim H0; intros; unfold adapted_couple in p; decompose [and] p;  assumption. apply StepFun_P17 with (fun x:R => Rabs (f x)) a b;  [ apply StepFun_P31; apply StepFun_P1 | apply (StepFun_P1 (mkStepFun (StepFun_P32 f))) ]. elim n; assumption. Qed. Lemma StepFun_P35 :  forall (l:Rlist) (a b:R) (f g:R -> R),    ordered_Rlist l ->    pos_Rl l 0 = a ->    pos_Rl l (pred (Rlength l)) = b ->    (forall x:R, a < x < b -> f x <= g x) ->    Int_SF (FF l f) l <= Int_SF (FF l g) l. simple induction l; intros. right; reflexivity. simpl in |- *; induction r0 as [| r0 r1 Hrecr0]. right; reflexivity. simpl in |- *; apply Rplus_le_compat. 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 in |- *;  apply lt_O_Sn. apply H3; split. apply Rmult_lt_reg_l with 2. prove_sup0. unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;  rewrite <- Rinv_r_sym. assert (H5 : r = a). apply H1. rewrite H5; rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l. assert (H6 := H0 0%nat (lt_O_Sn _)). simpl in H6. elim H6; intro. rewrite H5 in H7; apply H7. elim H4; assumption. discrR. apply Rmult_lt_reg_l with 2. prove_sup0. unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;  rewrite <- Rinv_r_sym. rewrite Rmult_1_l; rewrite double; assert (H5 : r0 <= b). replace b with  (pos_Rl (cons r (cons r0 r1)) (pred (Rlength (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 in |- *; apply le_n_S. apply le_O_n. simpl in |- *; apply lt_n_Sn. 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 (lt_O_Sn _)). simpl in H6. elim H6; intro. apply H7. elim H4; assumption. assumption. discrR. 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 in |- *; apply (H0 0%nat); simpl in |- *; apply lt_O_Sn. Qed. Lemma StepFun_P36 :  forall (a b:R) (f g:StepFun a b) (l:Rlist),    a <= b ->    is_subdivision f a b l ->    is_subdivision g a b l ->    (forall x:R, a < x < b -> f x <= g x) ->    RiemannInt_SF f <= RiemannInt_SF g. intros; unfold RiemannInt_SF in |- *; case (Rle_dec a b); intro. replace (Int_SF (subdivision_val f) (subdivision f)) with (Int_SF (FF l f) l). replace (Int_SF (subdivision_val g) (subdivision g)) with (Int_SF (FF l g) l). unfold is_subdivision in X; elim X; clear X; intros;  unfold adapted_couple in p; decompose [and] p; clear p;  assert (H5 : Rmin a b = a);  [ unfold Rmin in |- *; case (Rle_dec a b); intro;     [ reflexivity | elim n; assumption ]  | assert (H7 : Rmax a b = b);     [ unfold Rmax in |- *; case (Rle_dec a b); intro;        [ reflexivity | elim n; assumption ]     | rewrite H5 in H3; rewrite H7 in H2; eapply StepFun_P35 with a b;        assumption ] ]. apply StepFun_P17 with (fe g) a b;  [ apply StepFun_P21; assumption | apply StepFun_P1 ]. apply StepFun_P17 with (fe f) a b;  [ apply StepFun_P21; assumption | apply StepFun_P1 ]. elim n; assumption. Qed. Lemma StepFun_P37 :  forall (a b:R) (f g:StepFun a b),    a <= b ->    (forall x:R, a < x < b -> f x <= g x) ->    RiemannInt_SF f <= RiemannInt_SF g. intros; eapply StepFun_P36; try assumption. eapply StepFun_P25; apply StepFun_P29. eapply StepFun_P23; apply StepFun_P29. Qed. Lemma StepFun_P38 :  forall (l:Rlist) (a b:R) (f:R -> R),    ordered_Rlist l ->    pos_Rl l 0 = a ->    pos_Rl l (pred (Rlength l)) = b ->    sigT      (fun g:StepFun a b =>         g b = f b /\         (forall i:nat,            (i < pred (Rlength l))%nat ->            constant_D_eq g (co_interval (pos_Rl l i) (pos_Rl l (S i)))              (f (pos_Rl l i)))). intros l a b f; generalize a; clear a; induction l. intros a H H0 H1; simpl in H0; simpl in H1;  exists (mkStepFun (StepFun_P4 a b (f b))); split. reflexivity. intros; elim (lt_n_O _ H2). intros; destruct l as [| r1 l]. simpl in H1; simpl in H0; exists (mkStepFun (StepFun_P4 a b (f b))); split. reflexivity. intros i H2; elim (lt_n_O _ H2). intros; assert (H2 : ordered_Rlist (cons r1 l)). apply RList_P4 with r; assumption. assert (H3 : pos_Rl (cons r1 l) 0 = r1). reflexivity. assert (H4 : pos_Rl (cons r1 l) (pred (Rlength (cons r1 l))) = b). rewrite <- H1; reflexivity. elim (IHl r1 H2 H3 H4); intros g [H5 H6]. set  (g' :=   fun x:R => match Rle_dec r1 x with              | left _ => g x              | right _ => f a              end). assert (H7 : r1 <= b). rewrite <- H4; apply RList_P7; [ assumption | left; reflexivity ]. assert (H8 : IsStepFun g' a b). unfold IsStepFun in |- *; assert (H8 := pre g); unfold IsStepFun in H8;  elim H8; intros lg H9; unfold is_subdivision in H9;  elim H9; clear H9; intros lg2 H9; split with (cons a lg);  unfold is_subdivision in |- *; split with (cons (f a) lg2);  unfold adapted_couple in H9; decompose [and] H9; clear H9;  unfold adapted_couple in |- *; repeat split. unfold ordered_Rlist in |- *; intros; simpl in H9;  induction i as [| i Hreci]. simpl in |- *; rewrite H12; replace (Rmin r1 b) with r1. simpl in H0; rewrite <- H0; apply (H 0%nat); simpl in |- *; apply lt_O_Sn. unfold Rmin in |- *; case (Rle_dec r1 b); intro;  [ reflexivity | elim n; assumption ]. apply (H10 i); apply lt_S_n. replace (S (pred (Rlength lg))) with (Rlength lg). apply H9. apply S_pred with 0%nat; apply neq_O_lt; intro; rewrite <- H14 in H9;  elim (lt_n_O _ H9). simpl in |- *; assert (H14 : a <= b). rewrite <- H1; simpl in H0; rewrite <- H0; apply RList_P7;  [ assumption | left; reflexivity ]. unfold Rmin in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. assert (H14 : a <= b). rewrite <- H1; simpl in H0; rewrite <- H0; apply RList_P7;  [ assumption | left; reflexivity ]. replace (Rmax a b) with (Rmax r1 b). rewrite <- H11; induction lg as [| r0 lg Hreclg]. simpl in H13; discriminate. reflexivity. unfold Rmax in |- *; case (Rle_dec a b); case (Rle_dec r1 b); intros;  reflexivity || elim n; assumption. simpl in |- *; rewrite H13; reflexivity. intros; simpl in H9; induction i as [| i Hreci]. unfold constant_D_eq, open_interval in |- *; simpl in |- *; intros;  assert (H16 : Rmin r1 b = r1). unfold Rmin in |- *; case (Rle_dec r1 b); intro;  [ reflexivity | elim n; assumption ]. rewrite H16 in H12; rewrite H12 in H14; elim H14; clear H14; intros _ H14;  unfold g' in |- *; case (Rle_dec r1 x); intro r3. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r3 H14)). reflexivity. change   (constant_D_eq g' (open_interval (pos_Rl lg i) (pos_Rl lg (S i)))      (pos_Rl lg2 i)) in |- *; clear Hreci; assert (H16 := H15 i);  assert (H17 : (i < pred (Rlength lg))%nat). apply lt_S_n. replace (S (pred (Rlength lg))) with (Rlength lg). assumption. apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;  rewrite <- H14 in H9; elim (lt_n_O _ H9). assert (H18 := H16 H17); unfold constant_D_eq, open_interval in H18;  unfold constant_D_eq, open_interval in |- *; intros;  assert (H19 := H18 _ H14); rewrite <- H19; unfold g' in |- *;  case (Rle_dec r1 x); intro. reflexivity. elim n; replace r1 with (Rmin r1 b). rewrite <- H12; elim H14; clear H14; intros H14 _; left;  apply Rle_lt_trans with (pos_Rl lg i); try assumption. apply RList_P5. assumption. elim (RList_P3 lg (pos_Rl lg i)); intros; apply H21; exists i; split. reflexivity. apply lt_trans with (pred (Rlength lg)); try assumption. apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H22 in H17;  elim (lt_n_O _ H17). unfold Rmin in |- *; case (Rle_dec r1 b); intro;  [ reflexivity | elim n0; assumption ]. exists (mkStepFun H8); split. simpl in |- *; unfold g' in |- *; case (Rle_dec r1 b); intro. assumption. elim n; assumption. intros; simpl in H9; induction i as [| i Hreci]. unfold constant_D_eq, co_interval in |- *; simpl in |- *; intros; simpl in H0;  rewrite H0; elim H10; clear H10; intros; unfold g' in |- *;  case (Rle_dec r1 x); intro r3. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r3 H11)). reflexivity. clear Hreci;  change    (constant_D_eq (mkStepFun H8)       (co_interval (pos_Rl (cons r1 l) i) (pos_Rl (cons r1 l) (S i)))       (f (pos_Rl (cons r1 l) i))) in |- *; assert (H10 := H6 i);  assert (H11 : (i < pred (Rlength (cons r1 l)))%nat). simpl in |- *; apply lt_S_n; assumption. assert (H12 := H10 H11); unfold constant_D_eq, co_interval in H12;  unfold constant_D_eq, co_interval in |- *; intros;  rewrite <- (H12 _ H13); simpl in |- *; unfold g' in |- *;  case (Rle_dec r1 x); intro. reflexivity. elim n; elim H13; clear H13; intros;  apply Rle_trans with (pos_Rl (cons r1 l) i); try assumption;  change (pos_Rl (cons r1 l) 0 <= pos_Rl (cons r1 l) i) in |- *;  elim (RList_P6 (cons r1 l)); intros; apply H15;  [ assumption  | apply le_O_n  | simpl in |- *; apply lt_trans with (Rlength l);     [ apply lt_S_n; assumption | apply lt_n_Sn ] ]. Qed. Lemma StepFun_P39 :  forall (a b:R) (f:StepFun a b),    RiemannInt_SF f = - RiemannInt_SF (mkStepFun (StepFun_P6 (pre f))). intros; unfold RiemannInt_SF in |- *; case (Rle_dec a b); case (Rle_dec b a);  intros. assert (H : adapted_couple f a b (subdivision f) (subdivision_val f));  [ apply StepFun_P1  | assert     (H0 :      adapted_couple (mkStepFun (StepFun_P6 (pre f))) b a        (subdivision (mkStepFun (StepFun_P6 (pre f))))        (subdivision_val (mkStepFun (StepFun_P6 (pre f)))));     [ apply StepFun_P1     | assert (H1 : a = b);        [ apply Rle_antisym; assumption        | rewrite (StepFun_P8 H H1); assert (H2 : b = a);           [ symmetry in |- *; apply H1 | rewrite (StepFun_P8 H0 H2); ring ] ] ] ]. rewrite Ropp_involutive; eapply StepFun_P17;  [ apply StepFun_P1  | apply StepFun_P2; set (H := StepFun_P6 (pre f)); unfold IsStepFun in H;     elim H; intros; unfold is_subdivision in |- *;     elim p; intros; apply p0 ]. apply Ropp_eq_compat; eapply StepFun_P17;  [ apply StepFun_P1  | apply StepFun_P2; set (H := StepFun_P6 (pre f)); unfold IsStepFun in H;     elim H; intros; unfold is_subdivision in |- *;     elim p; intros; apply p0 ]. assert (H : a < b);  [ auto with real  | assert (H0 : b < a);     [ auto with real | elim (Rlt_irrefl _ (Rlt_trans _ _ _ H H0)) ] ]. Qed. Lemma StepFun_P40 :  forall (f:R -> R) (a b c:R) (l1 l2 lf1 lf2:Rlist),    a < b ->    b < c ->    adapted_couple f a b l1 lf1 ->    adapted_couple f b c l2 lf2 ->    adapted_couple f a c (cons_Rlist l1 l2) (FF (cons_Rlist l1 l2) f). intros f a b c l1 l2 lf1 lf2 H H0 H1 H2; unfold adapted_couple in H1, H2;  unfold adapted_couple in |- *; decompose [and] H1;  decompose [and] H2; clear H1 H2; repeat split. apply RList_P25; try assumption. rewrite H10; rewrite H4; unfold Rmin, Rmax in |- *; case (Rle_dec a b);  case (Rle_dec b c); intros;  (right; reflexivity) || (elim n; left; assumption). rewrite RList_P22. rewrite H5; unfold Rmin, Rmax in |- *; case (Rle_dec a b); case (Rle_dec a c);  intros;  [ reflexivity | elim n; apply Rle_trans with b; left; assumption | elim n; left; assumption | elim n0; left; assumption ]. red in |- *; intro; rewrite H1 in H6; discriminate. rewrite RList_P24. rewrite H9; unfold Rmin, Rmax in |- *; case (Rle_dec b c); case (Rle_dec a c);  intros;  [ reflexivity | elim n; apply Rle_trans with b; left; assumption | elim n; left; assumption | elim n0; left; assumption ]. red in |- *; intro; rewrite H1 in H11; discriminate. apply StepFun_P20. rewrite RList_P23; apply neq_O_lt; red in |- *; intro. assert (H2 : (Rlength l1 + Rlength l2)%nat = 0%nat). symmetry in |- *; apply H1. elim (plus_is_O _ _ H2); intros; rewrite H12 in H6; discriminate. unfold constant_D_eq, open_interval in |- *; intros;  elim (le_or_lt (S (S i)) (Rlength l1)); intro. assert (H14 : pos_Rl (cons_Rlist l1 l2) i = pos_Rl l1 i). apply RList_P26; apply lt_S_n; apply le_lt_n_Sm; apply le_S_n;  apply le_trans with (Rlength l1); [ assumption | apply le_n_Sn ]. assert (H15 : pos_Rl (cons_Rlist l1 l2) (S i) = pos_Rl l1 (S i)). apply RList_P26; apply lt_S_n; apply le_lt_n_Sm; assumption. rewrite H14 in H2; rewrite H15 in H2; assert (H16 : (2 <= Rlength l1)%nat). apply le_trans with (S (S i));  [ repeat apply le_n_S; apply le_O_n | assumption ]. elim (RList_P20 _ H16); intros r1 [r2 [r3 H17]]; rewrite H17;  change    (f x = pos_Rl (app_Rlist (mid_Rlist (cons_Rlist (cons r2 r3) l2) r1) f) i)   in |- *; rewrite RList_P12. induction i as [| i Hreci]. simpl in |- *; assert (H18 := H8 0%nat);  unfold constant_D_eq, open_interval in H18;  assert (H19 : (0 < pred (Rlength l1))%nat). rewrite H17; simpl in |- *; apply lt_O_Sn. assert (H20 := H18 H19); repeat rewrite H20. reflexivity. assert (H21 : r1 <= r2). rewrite H17 in H3; apply (H3 0%nat). simpl in |- *; apply lt_O_Sn. elim H21; intro. split. rewrite H17; simpl in |- *; apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. rewrite H17; simpl in |- *; apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite (Rplus_comm r1); rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. elim H2; intros; rewrite H17 in H23; rewrite H17 in H24; simpl in H24;  simpl in H23; rewrite H22 in H23;  elim (Rlt_irrefl _ (Rlt_trans _ _ _ H23 H24)). assumption. clear Hreci; rewrite RList_P13. rewrite H17 in H14; rewrite H17 in H15;  change    (pos_Rl (cons_Rlist (cons r2 r3) l2) i =     pos_Rl (cons r1 (cons r2 r3)) (S i)) in H14; rewrite H14;  change    (pos_Rl (cons_Rlist (cons r2 r3) l2) (S i) =     pos_Rl (cons r1 (cons r2 r3)) (S (S i))) in H15;  rewrite H15; assert (H18 := H8 (S i));  unfold constant_D_eq, open_interval in H18;  assert (H19 : (S i < pred (Rlength l1))%nat). apply lt_pred; apply lt_S_n; apply le_lt_n_Sm; assumption. assert (H20 := H18 H19); repeat rewrite H20. reflexivity. rewrite <- H17; assert (H21 : pos_Rl l1 (S i) <= pos_Rl l1 (S (S i))). apply (H3 (S i)); apply lt_pred; apply lt_S_n; apply le_lt_n_Sm; assumption. elim H21; intro. split. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite (Rplus_comm (pos_Rl l1 (S i))); rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. elim H2; intros; rewrite H22 in H23;  elim (Rlt_irrefl _ (Rlt_trans _ _ _ H23 H24)). assumption. simpl in |- *; rewrite H17 in H1; simpl in H1; apply lt_S_n; assumption. rewrite RList_P14; rewrite H17 in H1; simpl in H1; apply H1. inversion H12. assert (H16 : pos_Rl (cons_Rlist l1 l2) (S i) = b). rewrite RList_P29. rewrite H15; rewrite <- minus_n_n; rewrite H10; unfold Rmin in |- *;  case (Rle_dec b c); intro; [ reflexivity | elim n; left; assumption ]. rewrite H15; apply le_n. induction l1 as [| r l1 Hrecl1]. simpl in H15; discriminate. clear Hrecl1; simpl in H1; simpl in |- *; apply lt_n_S; assumption. assert (H17 : pos_Rl (cons_Rlist l1 l2) i = b). rewrite RList_P26. replace i with (pred (Rlength l1));  [ rewrite H4; unfold Rmax in |- *; case (Rle_dec a b); intro;     [ reflexivity | elim n; left; assumption ]  | rewrite H15; reflexivity ]. rewrite H15; apply lt_n_Sn. rewrite H16 in H2; rewrite H17 in H2; elim H2; intros;  elim (Rlt_irrefl _ (Rlt_trans _ _ _ H14 H18)). assert (H16 : pos_Rl (cons_Rlist l1 l2) i = pos_Rl l2 (i - Rlength l1)). apply RList_P29. apply le_S_n; assumption. apply lt_le_trans with (pred (Rlength (cons_Rlist l1 l2)));  [ assumption | apply le_pred_n ]. assert  (H17 : pos_Rl (cons_Rlist l1 l2) (S i) = pos_Rl l2 (S (i - Rlength l1))). replace (S (i - Rlength l1)) with (S i - Rlength l1)%nat. apply RList_P29. apply le_S_n; apply le_trans with (S i); [ assumption | apply le_n_Sn ]. induction l1 as [| r l1 Hrecl1]. simpl in H6; discriminate. clear Hrecl1; simpl in H1; simpl in |- *; apply lt_n_S; assumption. symmetry in |- *; apply minus_Sn_m; apply le_S_n; assumption. assert (H18 : (2 <= Rlength l1)%nat). clear f c l2 lf2 H0 H3 H8 H7 H10 H9 H11 H13 i H1 x H2 H12 m H14 H15 H16 H17;  induction l1 as [| r l1 Hrecl1]. discriminate. clear Hrecl1; induction l1 as [| r0 l1 Hrecl1]. simpl in H5; simpl in H4; assert (H0 : Rmin a b < Rmax a b). unfold Rmin, Rmax in |- *; case (Rle_dec a b); intro;  [ assumption | elim n; left; assumption ]. rewrite <- H5 in H0; rewrite <- H4 in H0; elim (Rlt_irrefl _ H0). clear Hrecl1; simpl in |- *; repeat apply le_n_S; apply le_O_n. elim (RList_P20 _ H18); intros r1 [r2 [r3 H19]]; rewrite H19;  change    (f x = pos_Rl (app_Rlist (mid_Rlist (cons_Rlist (cons r2 r3) l2) r1) f) i)   in |- *; rewrite RList_P12. induction i as [| i Hreci]. assert (H20 := le_S_n _ _ H15); assert (H21 := le_trans _ _ _ H18 H20);  elim (le_Sn_O _ H21). clear Hreci; rewrite RList_P13. rewrite H19 in H16; rewrite H19 in H17;  change    (pos_Rl (cons_Rlist (cons r2 r3) l2) i =     pos_Rl l2 (S i - Rlength (cons r1 (cons r2 r3))))   in H16; rewrite H16;  change    (pos_Rl (cons_Rlist (cons r2 r3) l2) (S i) =     pos_Rl l2 (S (S i - Rlength (cons r1 (cons r2 r3)))))   in H17; rewrite H17; assert (H20 := H13 (S i - Rlength l1)%nat);  unfold constant_D_eq, open_interval in H20;  assert (H21 : (S i - Rlength l1 < pred (Rlength l2))%nat). apply lt_pred; rewrite minus_Sn_m. apply plus_lt_reg_l with (Rlength l1); rewrite <- le_plus_minus. rewrite H19 in H1; simpl in H1; rewrite H19; simpl in |- *;  rewrite RList_P23 in H1; apply lt_n_S; assumption. apply le_trans with (S i); [ apply le_S_n; assumption | apply le_n_Sn ]. apply le_S_n; assumption. assert (H22 := H20 H21); repeat rewrite H22. reflexivity. rewrite <- H19;  assert   (H23 : pos_Rl l2 (S i - Rlength l1) <= pos_Rl l2 (S (S i - Rlength l1))). apply H7; apply lt_pred. rewrite minus_Sn_m. apply plus_lt_reg_l with (Rlength l1); rewrite <- le_plus_minus. rewrite H19 in H1; simpl in H1; rewrite H19; simpl in |- *;  rewrite RList_P23 in H1; apply lt_n_S; assumption. apply le_trans with (S i); [ apply le_S_n; assumption | apply le_n_Sn ]. apply le_S_n; assumption. elim H23; intro. split. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. apply Rmult_lt_reg_l with 2;  [ prove_sup0  | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;     rewrite <- Rinv_r_sym;     [ rewrite Rmult_1_l; rewrite (Rplus_comm (pos_Rl l2 (S i - Rlength l1))); rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. rewrite <- H19 in H16; rewrite <- H19 in H17; elim H2; intros;  rewrite H19 in H25; rewrite H19 in H26; simpl in H25;  simpl in H16; rewrite H16 in H25; simpl in H26; simpl in H17;  rewrite H17 in H26; simpl in H24; rewrite H24 in H25;  elim (Rlt_irrefl _ (Rlt_trans _ _ _ H25 H26)). assert (H23 : pos_Rl (cons_Rlist l1 l2) (S i) = pos_Rl l2 (S i - Rlength l1)). rewrite H19; simpl in |- *; simpl in H16; apply H16. assert  (H24 :   pos_Rl (cons_Rlist l1 l2) (S (S i)) = pos_Rl l2 (S (S i - Rlength l1))). rewrite H19; simpl in |- *; simpl in H17; apply H17. rewrite <- H23; rewrite <- H24; assumption. simpl in |- *; rewrite H19 in H1; simpl in H1; apply lt_S_n; assumption. rewrite RList_P14; rewrite H19 in H1; simpl in H1; simpl in |- *; apply H1. Qed. Lemma StepFun_P41 :  forall (f:R -> R) (a b c:R),    a <= b -> b <= c -> IsStepFun f a b -> IsStepFun f b c -> IsStepFun f a c. Proof. intros f a b c H H0 (l1,(lf1,H1)) (l2,(lf2,H2));  destruct (total_order_T a b) as [[Hltab|Hab]|Hgtab].  destruct (total_order_T b c) as [[Hltbc|Hbc]|Hgtbc]. exists (cons_Rlist l1 l2); exists (FF (cons_Rlist l1 l2) f);  apply StepFun_P40 with b lf1 lf2; assumption. exists l1; exists lf1; rewrite Hbc in H1; assumption. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hgtbc)). exists l2; exists lf2; rewrite <- Hab in H2; assumption. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgtab)). Qed. Lemma StepFun_P42 :  forall (l1 l2:Rlist) (f:R -> R),    pos_Rl l1 (pred (Rlength l1)) = pos_Rl l2 0 ->    Int_SF (FF (cons_Rlist l1 l2) f) (cons_Rlist l1 l2) =    Int_SF (FF l1 f) l1 + Int_SF (FF l2 f) l2. intros l1 l2 f; induction l1 as [| r l1 IHl1]; intros H;  [ simpl in |- *; ring  | destruct l1 as [| r0 r1];     [ simpl in H; simpl in |- *; destruct l2 as [| r0 r1];        [ simpl in |- *; ring | simpl in |- *; simpl in H; rewrite H; ring ]     | simpl in |- *; rewrite Rplus_assoc; apply Rplus_eq_compat_l; apply IHl1;        rewrite <- H; reflexivity ] ]. Qed. 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). intros f; intros;  assert   (H1 :    sigT (fun l:Rlist => sigT (fun l0:Rlist => adapted_couple f a b l l0))). apply pr1. assert  (H2 :   sigT (fun l:Rlist => sigT (fun l0:Rlist => adapted_couple f b c l l0))). apply pr2. assert  (H3 :   sigT (fun l:Rlist => sigT (fun l0:Rlist => adapted_couple f a c l l0))). apply pr3. elim H1; clear H1; intros l1 [lf1 H1]; elim H2; clear H2; intros l2 [lf2 H2];  elim H3; clear H3; intros 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. replace (RiemannInt_SF (mkStepFun pr2)) with  match Rle_dec b c with  | left _ => Int_SF lf2 l2  | right _ => - Int_SF lf2 l2  end. replace (RiemannInt_SF (mkStepFun pr3)) with  match Rle_dec a c with  | left _ => Int_SF lf3 l3  | right _ => - Int_SF lf3 l3  end. case (Rle_dec a b); case (Rle_dec b c); case (Rle_dec a c); intros. elim r1; intro. elim r0; intro. replace (Int_SF lf3 l3) with  (Int_SF (FF (cons_Rlist l1 l2) f) (cons_Rlist l1 l2)). 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 in |- *; 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 in |- *;  case (Rle_dec a b); case (Rle_dec b c); intros; reflexivity || elim n;  assumption. eapply StepFun_P17;  [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf2; apply H2; assumption | assumption ]. eapply StepFun_P17;  [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf1; apply H1 | assumption ]. eapply StepFun_P17; [ apply (StepFun_P40 H H0 H1 H2) | apply H3 ]. replace (Int_SF lf2 l2) with 0. rewrite Rplus_0_r; eapply StepFun_P17;  [ apply H1 | rewrite <- H0 in H3; apply H3 ]. symmetry in |- *; 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 in |- *; eapply StepFun_P8; [ apply H1 | assumption ]. elim n; 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 r; intro. rewrite Rplus_comm;  replace (Int_SF lf1 l1) with   (Int_SF (FF (cons_Rlist l3 l2) f) (cons_Rlist 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 in |- *;  case (Rle_dec a c); case (Rle_dec b c); intros;  [ elim n; assumption | reflexivity | elim n0; assumption | elim n1; assumption ]. eapply StepFun_P17;  [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf2; apply H2 | assumption ]. eapply StepFun_P17;  [ apply StepFun_P21; unfold is_subdivision in |- *; 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 in |- *; eapply StepFun_P8; [ apply H3 | assumption ]. replace (Int_SF lf2 l2) with (Int_SF lf3 l3 + Int_SF lf1 l1). ring. elim r; intro. replace (Int_SF lf2 l2) with  (Int_SF (FF (cons_Rlist l3 l1) f) (cons_Rlist 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 in |- *; 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 in |- *;  case (Rle_dec a c); case (Rle_dec a b); intros;  [ elim n; assumption | elim n1; assumption | reflexivity | elim n1; assumption ]. eapply StepFun_P17;  [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf1; apply H1 | assumption ]. eapply StepFun_P17;  [ apply StepFun_P21; unfold is_subdivision in |- *; 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 in |- *; 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 r; intro. replace (Int_SF lf2 l2) with  (Int_SF (FF (cons_Rlist l1 l3) f) (cons_Rlist 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 in |- *; 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 in |- *;  case (Rle_dec a c); case (Rle_dec a b); intros;  [ elim n; assumption | reflexivity | elim n0; assumption | elim n1; assumption ]. eapply StepFun_P17;  [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf1; apply H1 | assumption ]. eapply StepFun_P17;  [ apply StepFun_P21; unfold is_subdivision in |- *; 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 in |- *; 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 r; intro. replace (Int_SF lf1 l1) with  (Int_SF (FF (cons_Rlist l2 l3) f) (cons_Rlist 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 in |- *; 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 in |- *;  case (Rle_dec a c); case (Rle_dec b c); intros;  [ elim n; assumption | elim n1; assumption | reflexivity | elim n1; assumption ]. eapply StepFun_P17;  [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf2; apply H2 | assumption ]. eapply StepFun_P17;  [ apply StepFun_P21; unfold is_subdivision in |- *; 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 in |- *; eapply StepFun_P8; [ apply H2 | assumption ]. elim n; 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 (cons_Rlist l2 l1) f) (cons_Rlist 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 in |- *; 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 in |- *;  case (Rle_dec a b); case (Rle_dec b c); intros;  [ elim n1; assumption | elim n1; assumption | elim n0; assumption | reflexivity ]. eapply StepFun_P17;  [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf2; apply H2 | assumption ]. eapply StepFun_P17;  [ apply StepFun_P21; unfold is_subdivision in |- *; 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. unfold RiemannInt_SF in |- *; case (Rle_dec a c); intro. eapply StepFun_P17. apply H3. change   (adapted_couple (mkStepFun pr3) a c (subdivision (mkStepFun pr3))      (subdivision_val (mkStepFun pr3))) in |- *; apply StepFun_P1. apply Ropp_eq_compat; eapply StepFun_P17. apply H3. change   (adapted_couple (mkStepFun pr3) a c (subdivision (mkStepFun pr3))      (subdivision_val (mkStepFun pr3))) in |- *; apply StepFun_P1. unfold RiemannInt_SF in |- *; case (Rle_dec b c); intro. eapply StepFun_P17. apply H2. change   (adapted_couple (mkStepFun pr2) b c (subdivision (mkStepFun pr2))      (subdivision_val (mkStepFun pr2))) in |- *; apply StepFun_P1. apply Ropp_eq_compat; eapply StepFun_P17. apply H2. change   (adapted_couple (mkStepFun pr2) b c (subdivision (mkStepFun pr2))      (subdivision_val (mkStepFun pr2))) in |- *; apply StepFun_P1. unfold RiemannInt_SF in |- *; case (Rle_dec a b); intro. eapply StepFun_P17. apply H1. change   (adapted_couple (mkStepFun pr1) a b (subdivision (mkStepFun pr1))      (subdivision_val (mkStepFun pr1))) in |- *; apply StepFun_P1. apply Ropp_eq_compat; eapply StepFun_P17. apply H1. change   (adapted_couple (mkStepFun pr1) a b (subdivision (mkStepFun pr1))      (subdivision_val (mkStepFun pr1))) in |- *; apply StepFun_P1. Qed. Lemma StepFun_P44 :  forall (f:R -> R) (a b c:R),    IsStepFun f a b -> a <= c <= b -> IsStepFun f a c. intros f; intros; assert (H0 : a <= b). elim H; intros; apply Rle_trans with c; assumption. elim H; clear H; intros; unfold IsStepFun in X; unfold is_subdivision in X;  elim X; clear X; intros l1 [lf1 H2];  cut   (forall (l1 lf1:Rlist) (a b c:R) (f:R -> R),      adapted_couple f a b l1 lf1 ->      a <= c <= b ->      sigT (fun l:Rlist => sigT (fun l0:Rlist => adapted_couple f a c l l0))). intro X; unfold IsStepFun in |- *; unfold is_subdivision in |- *; eapply X. apply H2. split; assumption. clear f a b c H0 H H1 H2 l1 lf1; simple induction l1. intros; unfold adapted_couple in H; decompose [and] H; clear H; simpl in H4;  discriminate. simple induction r0. intros X lf1 a b c f H H0; assert (H1 : a = b). unfold adapted_couple in H; decompose [and] H; clear H; simpl in H3;  simpl in H2; assert (H7 : a <= b). elim H0; intros; apply Rle_trans with c; assumption. replace a with (Rmin a b). pattern b at 2 in |- *; replace b with (Rmax a b). rewrite <- H2; rewrite H3; reflexivity. unfold Rmax in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. unfold Rmin in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. split with (cons r nil); split with lf1; assert (H2 : c = b). rewrite H1 in H0; elim H0; intros; apply Rle_antisym; assumption. rewrite H2; assumption. intros r1 r2 _ X0 lf1 a b c f H H0; induction lf1 as [| r3 lf1 Hreclf1]. unfold adapted_couple in H; decompose [and] H; clear H; simpl in H4;  discriminate. clear Hreclf1; assert (H1 : {c <= r1} + {r1 < c}). case (Rle_dec c r1); intro; [ left; assumption | right; auto with real ]. elim H1; intro. split with (cons r (cons c nil)); split with (cons r3 nil);  unfold adapted_couple in H; decompose [and] H; clear H;  assert (H6 : r = a). simpl in H4; rewrite H4; unfold Rmin in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; elim H0; intros; apply Rle_trans with c; assumption ]. elim H0; clear H0; intros; unfold adapted_couple in |- *; repeat split. rewrite H6; unfold ordered_Rlist in |- *; intros; simpl in H8; inversion H8;  [ simpl in |- *; assumption | elim (le_Sn_O _ H10) ]. simpl in |- *; unfold Rmin in |- *; case (Rle_dec a c); intro;  [ assumption | elim n; assumption ]. simpl in |- *; unfold Rmax in |- *; case (Rle_dec a c); intro;  [ reflexivity | elim n; assumption ]. unfold constant_D_eq, open_interval in |- *; intros; simpl in H8;  inversion H8. simpl in |- *; assert (H10 := H7 0%nat);  assert (H12 : (0 < pred (Rlength (cons r (cons r1 r2))))%nat). simpl in |- *; apply lt_O_Sn. apply (H10 H12); unfold open_interval in |- *; simpl in |- *;  rewrite H11 in H9; simpl in H9; elim H9; clear H9;  intros; split; try assumption. apply Rlt_le_trans with c; assumption. elim (le_Sn_O _ H11). cut (adapted_couple f r1 b (cons r1 r2) lf1). cut (r1 <= c <= b). intros. elim (X0 _ _ _ _ _ H3 H2); intros l1' [lf1' H4]; split with (cons r l1');  split with (cons r3 lf1'); unfold adapted_couple in H, H4;  decompose [and] H; decompose [and] H4; clear H H4 X0;  assert (H14 : a <= b). elim H0; intros; apply Rle_trans with c; assumption. assert (H16 : r = a). simpl in H7; rewrite H7; unfold Rmin in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. induction l1' as [| r4 l1' Hrecl1']. simpl in H13; discriminate. clear Hrecl1'; unfold adapted_couple in |- *; repeat split. unfold ordered_Rlist in |- *; intros; simpl in H; induction i as [| i Hreci]. simpl in |- *; replace r4 with r1. apply (H5 0%nat). simpl in |- *; apply lt_O_Sn. simpl in H12; rewrite H12; unfold Rmin in |- *; case (Rle_dec r1 c); intro;  [ reflexivity | elim n; left; assumption ]. apply (H9 i); simpl in |- *; apply lt_S_n; assumption. simpl in |- *; unfold Rmin in |- *; case (Rle_dec a c); intro;  [ assumption | elim n; elim H0; intros; assumption ]. replace (Rmax a c) with (Rmax r1 c). rewrite <- H11; reflexivity. unfold Rmax in |- *; case (Rle_dec r1 c); case (Rle_dec a c); intros;  [ reflexivity | elim n; elim H0; intros; assumption | elim n; left; assumption | elim n0; left; assumption ]. simpl in |- *; simpl in H13; rewrite H13; reflexivity. intros; simpl in H; unfold constant_D_eq, open_interval in |- *; intros;  induction i as [| i Hreci]. simpl in |- *; assert (H17 := H10 0%nat);  assert (H18 : (0 < pred (Rlength (cons r (cons r1 r2))))%nat). simpl in |- *; apply lt_O_Sn. apply (H17 H18); unfold open_interval in |- *; simpl in |- *; simpl in H4;  elim H4; clear H4; intros; split; try assumption;  replace r1 with r4. assumption. simpl in H12; rewrite H12; unfold Rmin in |- *; case (Rle_dec r1 c); intro;  [ reflexivity | elim n; left; assumption ]. clear Hreci; simpl in |- *; apply H15. simpl in |- *; apply lt_S_n; assumption. unfold open_interval in |- *; apply H4. split. left; assumption. elim H0; intros; assumption. eapply StepFun_P7;  [ elim H0; intros; apply Rle_trans with c; [ apply H2 | apply H3 ]  | apply H ]. Qed. Lemma StepFun_P45 :  forall (f:R -> R) (a b c:R),    IsStepFun f a b -> a <= c <= b -> IsStepFun f c b. intros f; intros; assert (H0 : a <= b). elim H; intros; apply Rle_trans with c; assumption. elim H; clear H; intros; unfold IsStepFun in X; unfold is_subdivision in X;  elim X; clear X; intros l1 [lf1 H2];  cut   (forall (l1 lf1:Rlist) (a b c:R) (f:R -> R),      adapted_couple f a b l1 lf1 ->      a <= c <= b ->      sigT (fun l:Rlist => sigT (fun l0:Rlist => adapted_couple f c b l l0))). intro X; unfold IsStepFun in |- *; unfold is_subdivision in |- *; eapply X;  [ apply H2 | split; assumption ]. clear f a b c H0 H H1 H2 l1 lf1; simple induction l1. intros; unfold adapted_couple in H; decompose [and] H; clear H; simpl in H4;  discriminate. simple induction r0. intros X lf1 a b c f H H0; assert (H1 : a = b). unfold adapted_couple in H; decompose [and] H; clear H; simpl in H3;  simpl in H2; assert (H7 : a <= b). elim H0; intros; apply Rle_trans with c; assumption. replace a with (Rmin a b). pattern b at 2 in |- *; replace b with (Rmax a b). rewrite <- H2; rewrite H3; reflexivity. unfold Rmax in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. unfold Rmin in |- *; case (Rle_dec a b); intro;  [ reflexivity | elim n; assumption ]. split with (cons r nil); split with lf1; assert (H2 : c = b). rewrite H1 in H0; elim H0; intros; apply Rle_antisym; assumption. rewrite <- H2 in H1; rewrite <- H1; assumption. intros r1 r2 _ X0 lf1 a b c f H H0; induction lf1 as [| r3 lf1 Hreclf1]. unfold adapted_couple in H; decompose [and] H; clear H; simpl in H4;  discriminate. clear Hreclf1; assert (H1 : {c <= r1} + {r1 < c}). case (Rle_dec c r1); intro; [ left; assumption | right; auto with real ]. elim H1; intro. split with (cons c (cons r1 r2)); split with (cons r3 lf1);  unfold adapted_couple in H; decompose [and] H; clear H;  unfold adapted_couple in |- *; repeat split. unfold ordered_Rlist in |- *; intros; simpl in H; induction i as [| i Hreci]. simpl in |- *; assumption. clear Hreci; apply (H2 (S i)); simpl in |- *; assumption. simpl in |- *; unfold Rmin in |- *; case (Rle_dec c b); intro;  [ reflexivity | elim n; elim H0; intros; assumption ]. replace (Rmax c b) with (Rmax a b). rewrite <- H3; reflexivity. unfold Rmax in |- *; case (Rle_dec a b); case (Rle_dec c b); intros;  [ reflexivity | elim n; elim H0; intros; assumption | elim n; elim H0; intros; apply Rle_trans with c; assumption | elim n0; elim H0; intros; apply Rle_trans with c; assumption ]. simpl in |- *; simpl in H5; apply H5. intros; simpl in H; induction i as [| i Hreci]. unfold constant_D_eq, open_interval in |- *; intros; simpl in |- *;  apply (H7 0%nat). simpl in |- *; apply lt_O_Sn. unfold open_interval in |- *; simpl in |- *; simpl in H6; elim H6; clear H6;  intros; split; try assumption; apply Rle_lt_trans with c;  try assumption; replace r with a. elim H0; intros; assumption. simpl in H4; rewrite H4; unfold Rmin in |- *; case (Rle_dec a b); intros;  [ reflexivity | elim n; elim H0; intros; apply Rle_trans with c; assumption ]. clear Hreci; apply (H7 (S i)); simpl in |- *; assumption. cut (adapted_couple f r1 b (cons r1 r2) lf1). cut (r1 <= c <= b). intros; elim (X0 _ _ _ _ _ H3 H2); intros l1' [lf1' H4]; split with l1';  split with lf1'; assumption. split; [ left; assumption | elim H0; intros; assumption ]. eapply StepFun_P7;  [ elim H0; intros; apply Rle_trans with c; [ apply H2 | apply H3 ]  | apply H ]. Qed. Lemma StepFun_P46 :  forall (f:R -> R) (a b c:R),    IsStepFun f a b -> IsStepFun f b c -> IsStepFun f a c. intros f; intros; case (Rle_dec a b); case (Rle_dec b c); intros. apply StepFun_P41 with b; assumption. case (Rle_dec a c); intro. apply StepFun_P44 with b; try assumption. split; [ assumption | auto with real ]. apply StepFun_P6; apply StepFun_P44 with b. apply StepFun_P6; assumption. split; auto with real. case (Rle_dec a c); intro. apply StepFun_P45 with b; try assumption. split; auto with real. apply StepFun_P6; apply StepFun_P45 with b. apply StepFun_P6; assumption. split; [ assumption | auto with real ]. apply StepFun_P6; apply StepFun_P41 with b;  auto with real || apply StepFun_P6; assumption. Qed. ```