path: root/theories/Reals/RiemannInt_SF.v

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)
 
(*i $Id: RiemannInt_SF.v,v 1.16.2.1 2004/07/16 19:31:13 herbelin Exp $ i*)

Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis.
Require Import Classical_Prop.
Open Local Scope R_scope.

Set Implicit Arguments.

(**************************************************)
(* Each bounded subset of N has a maximal element *)
(**************************************************)

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.

(*******************************************)
(*             Step functions              *)
(*******************************************)

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).

(* Class of step functions *)
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.

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.

(* Integral of step functions *)
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.

(********************************)
(* Properties of step functions *)
(********************************)

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.
unfold is_subdivision in |- *; intros; elim X; intros; exists x;
 unfold adapted_couple in p; decompose [and] p; clear p;
 unfold adapted_couple in |- *; repeat split; try assumption.
rewrite H1; 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 H0; 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_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.
intros a b l f g l1; unfold is_subdivision in |- *; intros; elim X; elim X0;
 intros; clear X X0; unfold adapted_couple in p, p0; 
 decompose [and] p; decompose [and] p0; clear p p0;
 apply existT with (FF l1 (fun x:R => f x + l * g x));
 unfold adapted_couple in |- *; repeat split; try assumption.
apply StepFun_P20; apply neq_O_lt; red in |- *; intro; rewrite <- H8 in H7;
 discriminate.
intros; unfold constant_D_eq, open_interval in |- *;
 unfold constant_D_eq, open_interval in H9, H4; intros;
 rewrite (H9 _ H8 _ H10); rewrite (H4 _ H8 _ H10); 
 assert (H11 : l1 <> nil).
red in |- *; intro; rewrite H11 in H8; elim (lt_n_O _ H8).
assert (H12 := RList_P19 _ H11); elim H12; clear H12; intros 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.

(* The set of step functions on [a,b] is a vectorial space *)
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.
unfold IsStepFun in |- *; unfold is_subdivision in |- *; intros; elim X;
 clear X; intros l1 [lf1 H1]; elim X0; clear X0; intros l2 [lf2 H2];
 case (total_order_T a b); intro.
elim s; intro.
case (total_order_T b c); intro.
elim s0; intro.
split with (cons_Rlist l1 l2); split with (FF (cons_Rlist l1 l2) f);
 apply StepFun_P40 with b lf1 lf2; assumption.
split with l1; split with lf1; rewrite b0 in H1; assumption.
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 r)).
split with l2; split with lf2; rewrite <- b0 in H2; assumption.
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)).
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))).
intros; 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; 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; clear X; 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))).
intros; 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; 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; clear X; 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.