Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: sortPPPP.launch Sprache: Coq

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis_reg.
Require Import Classical_Prop.
Local Open 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}.
Proof.
  intros; apply Z_of_nat_complete_inf; assumption.
Qed.

Lemma Nzorn :
  forall I:nat -> Prop,
    (exists n : nat, I n) ->
    Nbound I -> { n:nat | I n /\ (forall i:nat, I i -> (i <= n)%nat) }.
Proof.
  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;
    exists (INR N); unfold is_upper_bound; 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; exists x; split;
    [ assumption | reflexivity ].
  destruct (completeness E H1 H2) as (x,(H4,H5)); unfold is_upper_bound in H4, H5;
      assert (H6 : 0 <= x).
  destruct H2 as (x0,H6). remember H6 as H7. destruct H7 as (x1,(H8,H9)).
    apply Rle_trans with x0;
      [ rewrite <- H9; change (INR 0 <= INR x1); 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 x0 H9. assert (H10 := H4 _ H9); unfold E in H9; elim H9; intros x1 (H12,<-).
    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 ].
  destruct (IZN _ H14) as (x2,H15).
    rewrite H15, <- INR_IZR_INZ; apply le_INR; apply lt_le_S.
      apply INR_lt; 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 x0 H8; assert (H13 : E x).
  elim (classic (E x)); intro; try assumption.
  cut (forall y:R, E y -> y <= x - 1).
  intro H13; assert (H14 := H5 _ H13); cut (x - 1 < x).
  intro H15; 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 y H13; assert (H14 := H4 _ H13); elim H14; intro H15; unfold E in H13; elim H13;
    intros x1 H16; elim H16; intros H17 H18; 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 H19; rewrite H19; apply le_INR; apply lt_le_S; apply INR_lt; rewrite H18;
    rewrite <- H19; assumption.
  rewrite H10; rewrite H8; rewrite <- INR_IZR_INZ;
    rewrite <- (minus_INR _ 1).
  apply f_equal;
    case x0; [ reflexivity | intro; apply sym_eq, minus_n_O ].
  induction x0 as [|x0 Hrecx0].
    rewrite H8 in H3. rewrite <- INR_IZR_INZ in H3; simpl in H3.
      elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H3)).
    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 H8 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; split.
  assumption.
  intros; apply INR_le; rewrite H15; rewrite <- H15; elim H12; intros;
    rewrite H20; apply H4; unfold E; 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 :=
  { l0:Rlist & adapted_couple f a b l l0 }.

Definition IsStepFun (f:R -> R) (a b:R) : Type :=
  { 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) : 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).
Proof.
  intros a b f; unfold subdivision_val; case (projT2 (pre f)) as (x,H);
    apply H.
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.
Proof.
  unfold adapted_couple; intros; decompose [and] H; clear H;
    repeat split; try assumption.
  rewrite H2; unfold Rmin; 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; 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).
Proof.
  intros; unfold adapted_couple; repeat split.
  unfold ordered_Rlist; intros; simpl in H0; inversion H0;
    [ simpl; assumption | elim (le_Sn_O _ H2) ].
  simpl; unfold Rmin; decide (Rle_dec a b) with H; reflexivity.
  simpl; unfold Rmax; decide (Rle_dec a b) with H; reflexivity.
  unfold constant_D_eq, open_interval; 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.
Proof.
  intros; unfold IsStepFun; destruct (Rle_dec a b) as [Hle|Hnle].
  apply existT with (cons a (cons b nil)); unfold is_subdivision;
    apply existT with (cons c nil); apply (StepFun_P3 c Hle).
  apply existT with (cons b (cons a nil)); unfold is_subdivision;
    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.
Proof.
  destruct 1 as (x,(H0,(H1,(H2,(H3,H4))))); exists x;
    repeat split; try assumption.
  rewrite H1; apply Rmin_comm.
  rewrite H2; apply Rmax_comm.
Qed.

Lemma StepFun_P6 :
  forall (f:R -> R) (a b:R), IsStepFun f a b -> IsStepFun f b a.
Proof.
  unfold IsStepFun; 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.
Proof.
  unfold adapted_couple; intros; decompose [and] H0; clear H0;
    assert (H5 : Rmax a b = b).
  unfold Rmax; decide (Rle_dec a b) with H; reflexivity.
  assert (H7 : r2 <= b).
  rewrite H5 in H2; rewrite <- H2; apply RList_P7;
    [ assumption | simpl; right; left; reflexivity ].
  repeat split.
  apply RList_P4 with r1; assumption.
  rewrite H5 in H2; unfold Rmin; decide (Rle_dec r2 b) with H7; reflexivity.
  unfold Rmax; decide (Rle_dec r2 b) with H7.
    rewrite H5 in H2; rewrite <- H2; reflexivity.
  simpl in H4; simpl; 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; intros;
    unfold constant_D_eq, open_interval in H6;
      assert (H9 : (S i < pred (Rlength (cons r1 (cons r2 l))))%nat).
  simpl; 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.
Proof.
  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; 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;
      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; 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; right; left; reflexivity ]
      | unfold Rmin, Rmax; 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.
Proof.
  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; case (Rle_dec a b);
              intros; elim H0; rewrite <- H5; rewrite <- H7;
                reflexivity
            | simpl; 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').
Proof.
  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;
    unfold adapted_couple; unfold ordered_Rlist;
      repeat split; try (intros; simpl in H3; elim (lt_n_O _ H3)).
  simpl; rewrite <- H2; unfold Rmin; case (Rle_dec a a); intro;
    reflexivity.
  simpl; rewrite <- H2; unfold Rmax; 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; decide (Rle_dec a b) with H0; reflexivity.
  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; unfold adapted_couple;
      repeat split.
  unfold ordered_Rlist; intros; simpl in H8; inversion H8;
    [ simpl; assumption | elim (le_Sn_O _ H10) ].
  simpl; unfold Rmin; decide (Rle_dec a b) with H0; reflexivity.
  simpl; unfold Rmax; decide (Rle_dec a b) with H0; reflexivity.
  intros; simpl in H8; inversion H8.
  unfold constant_D_eq, open_interval; intros; simpl;
    simpl in H9; rewrite H3 in H1; unfold adapted_couple in H1;
      decompose [and] H1; apply (H16 0%nat).
  simpl; apply lt_O_Sn.
  unfold open_interval; simpl; rewrite H7; simpl in H13;
    rewrite H13; unfold Rmin; decide (Rle_dec a b) with H0; assumption.
  elim (le_Sn_O _ H10).
  intros; simpl in H8; elim (lt_n_O _ H8).
  intros; simpl in H8; inversion H8;
    [ simpl; assumption | elim (le_Sn_O _ H10) ].
  assert (Hyp_min : Rmin t2 b = t2).
  unfold Rmin; decide (Rle_dec t2 b) with H5; reflexivity.
  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; unfold adapted_couple;
          repeat split.
  unfold ordered_Rlist; intros; simpl in H1;
    induction  i as [| i Hreci].
  simpl; apply Rle_trans with s1.
  replace s1 with t2.
  apply (H12 0%nat).
  simpl; apply lt_O_Sn.
  simpl in H19; rewrite H19; symmetry ; apply Hyp_min.
  apply (H16 0%nat); simpl; apply lt_O_Sn.
  change (pos_Rl (cons s2 s3) i <= pos_Rl (cons s2 s3) (S i));
    apply (H16 (S i)); simpl; assumption.
  simpl; simpl in H14; rewrite H14; reflexivity.
  simpl; simpl in H18; rewrite H18; unfold Rmax;
    decide (Rle_dec a b) with H0; decide (Rle_dec t2 b) with H5; reflexivity.
  simpl; simpl in H20; apply H20.
  intros; simpl in H1; unfold constant_D_eq, open_interval; intros;
    induction  i as [| i Hreci].
  simpl; simpl in H6; destruct (total_order_T x t2) as [[Hlt|Heq]|Hgt].
  apply (H17 0%nat);
    [ simpl; apply lt_O_Sn
      | unfold open_interval; simpl; elim H6; intros; split;
        assumption ].
  rewrite Heq; assumption.
  rewrite H10; apply (H22 0%nat);
    [ simpl; apply lt_O_Sn
      | unfold open_interval; simpl; replace s1 with t2;
        [ elim H6; intros; split; assumption
          | simpl in H19; rewrite H19; rewrite Hyp_min; reflexivity ] ].
  simpl; simpl in H6; apply (H22 (S i));
    [ simpl; assumption
      | unfold open_interval; simpl; 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)
     ; rewrite <- H9; elim H8; intros; apply H6;
        simpl; apply H1.
  intros; induction  i as [| i Hreci].
  simpl; red; intro; elim Hyp_eq; apply Rle_antisym.
  apply (H12 0%nat); simpl; apply lt_O_Sn.
  rewrite <- Hyp_min; rewrite H6; simpl in H19; rewrite <- H19;
    apply (H16 0%nat); simpl; apply lt_O_Sn.
  elim H8; intros; rewrite H9 in H21; apply (H21 (S i)); simpl;
    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; unfold adapted_couple;
          repeat split.
  rewrite H9; unfold ordered_Rlist; intros; simpl in H1;
    induction  i as [| i Hreci].
  simpl; replace s1 with t2.
  apply (H16 0%nat); simpl; 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))
   ; apply (H12 i); simpl; apply lt_S_n;
      assumption.
  simpl; simpl in H19; apply H19.
  rewrite H9; simpl; simpl in H13; rewrite H13; unfold Rmax;
    decide (Rle_dec t2 b) with H5; decide (Rle_dec a b) with H0; reflexivity.
  rewrite H9; simpl; simpl in H15; rewrite H15; reflexivity.
  intros; simpl in H1; unfold constant_D_eq, open_interval; intros;
    induction  i as [| i Hreci].
  simpl; rewrite H9 in H6; simpl in H6; apply (H22 0%nat).
  simpl; apply lt_O_Sn.
  unfold open_interval; simpl.
  replace t2 with s1.
  assumption.
  simpl in H14; rewrite H14; rewrite Hyp_min; reflexivity.
  change (f x = pos_Rl (cons r2 lf') i); clear Hreci; apply (H17 i).
  simpl; rewrite H9 in H1; simpl in H1; apply lt_S_n; apply H1.
  rewrite H9 in H6; unfold open_interval; apply H6.
  intros; simpl in H1; induction  i as [| i Hreci].
  simpl; rewrite H9; right; simpl; replace s1 with t2.
  assumption.
  simpl in H14; rewrite H14; rewrite Hyp_min; reflexivity.
  elim H8; intros; apply (H6 i).
  simpl; apply lt_S_n; apply H1.
  intros; rewrite H9; induction  i as [| i Hreci].
  simpl; red; intro; elim Hyp_eq; apply Rle_antisym.
  apply (H16 0%nat); simpl; 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; 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; unfold adapted_couple;
          repeat split.
  rewrite H9; unfold ordered_Rlist; intros; simpl in H1;
    induction  i as [| i Hreci].
  simpl; replace s1 with t2.
  apply (H15 0%nat); simpl; 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))
   ; apply (H11 i); simpl; apply lt_S_n;
      assumption.
  simpl; simpl in H18; apply H18.
  rewrite H9; simpl; simpl in H12; rewrite H12; unfold Rmax;
    decide (Rle_dec t2 b) with H5; decide (Rle_dec a b) with H0; reflexivity.
  rewrite H9; simpl; simpl in H14; rewrite H14; reflexivity.
  intros; simpl in H1; unfold constant_D_eq, open_interval; intros;
    induction  i as [| i Hreci].
  simpl; rewrite H9 in H6; simpl in H6; apply (H21 0%nat).
  simpl; apply lt_O_Sn.
  unfold open_interval; simpl; replace t2 with s1.
  assumption.
  simpl in H13; rewrite H13; rewrite Hyp_min; reflexivity.
  change (f x = pos_Rl (cons r2 lf') i); clear Hreci; apply (H16 i).
  simpl; rewrite H9 in H1; simpl in H1; apply lt_S_n; apply H1.
  rewrite H9 in H6; unfold open_interval; apply H6.
  intros; simpl in H1; induction  i as [| i Hreci].
  simpl; left; assumption.
  elim H8; intros; apply (H6 i).
  simpl; apply lt_S_n; apply H1.
  intros; rewrite H9; induction  i as [| i Hreci].
  simpl; red; intro; elim Hyp_eq; apply Rle_antisym.
  apply (H15 0%nat); simpl; 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; 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; right; left; reflexivity ]
        | unfold Rmax; decide (Rle_dec a b) with H0; reflexivity ].
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.
Proof.
  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; destruct (Rle_dec r1 s2) as [Hle|Hnle]; 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; 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; split.
  apply Rmult_lt_reg_l with 2;
    [ prove_sup0
      | unfold Rdiv; 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; 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; split.
  apply Rmult_lt_reg_l with 2;
    [ prove_sup0
      | unfold Rdiv; 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; 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; apply lt_O_Sn
      | unfold open_interval; simpl; 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; simpl; unfold x; split.
  apply Rmult_lt_reg_l with 2;
    [ prove_sup0
      | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
        rewrite <- Rinv_r_sym;
          [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l;
            unfold Rmin; case (Rle_dec r1 r0); intro;
              assumption
            | discrR ] ].
  apply Rmult_lt_reg_l with 2;
    [ prove_sup0
      | unfold Rdiv; 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; simpl; unfold x; split.
  apply Rlt_trans with s2;
    [ assumption
      | apply Rmult_lt_reg_l with 2;
        [ prove_sup0
          | unfold Rdiv; rewrite <- (Rmult_comm (/ 2));
            rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym;
              [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l;
                unfold Rmin; case (Rle_dec r1 r0);
                  intro; assumption
                | discrR ] ] ].
  apply Rmult_lt_reg_l with 2;
    [ prove_sup0
      | unfold Rdiv; 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; 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.
Proof.
  unfold adapted_couple_opt; unfold adapted_couple; intros;
    decompose [and] H; clear H; repeat split; try assumption.
  rewrite H0; unfold Rmin; 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; 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.
Proof.
  intros; destruct (total_order_T a b) as [[Hlt|Heq]|Hgt].
  eapply StepFun_P11; [ apply Hlt | apply H0 | apply H1 ].
  elim H; assumption.
  eapply StepFun_P11;
    [ apply Hgt | 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.
Proof.
  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; decide (Rle_dec a b) with H1; reflexivity.
  assert (Hyp_max : Rmax a b = b).
  unfold Rmax; decide (Rle_dec a b) with H1; reflexivity.
  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;
      split.
  apply Rmult_lt_reg_l with 2;
    [ prove_sup0
      | unfold Rdiv; 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; 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;
      split.
  apply Rmult_lt_reg_l with 2;
    [ prove_sup0
      | unfold Rdiv; 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; 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; split.
  apply H.
  rewrite H5 in H3; apply H3.
  assert (H8 : r1 <= s2).
  eapply StepFun_P13.
  apply H4.
  apply H2.
  unfold adapted_couple_opt; split.
  apply H.
  rewrite H5 in H3; apply H3.
  elim H7; intro.
  simpl; 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)))
     ; 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; right; left; reflexivity ].
  eapply StepFun_P7.
  apply H1.
  apply H2.
  unfold adapted_couple_opt; 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; repeat split.
  unfold ordered_Rlist; intros; simpl in H; induction  i as [| i Hreci].
  simpl; rewrite <- H20; apply (H11 0%nat).
  simpl; apply lt_O_Sn.
  induction  i as [| i Hreci0].
  simpl; assumption.
  change (pos_Rl (cons s2 s3) i <= pos_Rl (cons s2 s3) (S i));
    apply (H15 (S i)); simpl; apply lt_S_n; assumption.
  simpl; symmetry ; apply Hyp_min.
  rewrite <- H17; reflexivity.
  simpl in H19; simpl; rewrite H19; reflexivity.
  intros; simpl in H; unfold constant_D_eq, open_interval; intros;
    induction  i as [| i Hreci].
  simpl; apply (H16 0%nat).
  simpl; apply lt_O_Sn.
  simpl in H2; rewrite <- H20 in H2; unfold open_interval;
    simpl; apply H2.
  clear Hreci; induction  i as [| i Hreci].
  simpl; simpl in H2; rewrite H9; apply (H21 0%nat).
  simpl; apply lt_O_Sn.
  unfold open_interval; simpl; elim H2; intros; split.
  apply Rle_lt_trans with r1; try assumption; rewrite <- H6; apply (H11 0%nat);
    simpl; apply lt_O_Sn.
  assumption.
  clear Hreci; simpl; apply (H21 (S i)).
  simpl; apply lt_S_n; assumption.
  unfold open_interval; 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)
     ; rewrite <- H5; apply H3.
  rewrite H5 in H11; intros; simpl in H12; induction  i as [| i Hreci].
  simpl; red; intro; rewrite H13 in H10;
    elim (Rlt_irrefl _ H10).
  clear Hreci; apply (H11 (S i)); simpl; 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; right; left; reflexivity ].
  eapply StepFun_P7.
  apply H1.
  apply H2.
  unfold adapted_couple_opt; 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; repeat split.
  unfold ordered_Rlist; intros; simpl in H; induction  i as [| i Hreci].
  simpl; rewrite <- H20; apply (H11 0%nat); simpl;
    apply lt_O_Sn.
  rewrite H10; apply (H15 (S i)); simpl; assumption.
  simpl; symmetry ; apply Hyp_min.
  rewrite <- H17; rewrite H10; reflexivity.
  simpl in H19; simpl; apply H19.
  intros; simpl in H; unfold constant_D_eq, open_interval; intros;
    induction  i as [| i Hreci].
  simpl; apply (H16 0%nat).
  simpl; apply lt_O_Sn.
  simpl in H2; rewrite <- H20 in H2; unfold open_interval;
    simpl; apply H2.
  clear Hreci; simpl; apply (H21 (S i)).
  simpl; assumption.
  rewrite <- H10; unfold open_interval; apply H2.
  elim H3; clear H3; intros; split.
  rewrite H5 in H3; intros; apply (H3 (S i)).
  simpl; replace (Rlength lf2) with (S (pred (Rlength lf2))).
  apply lt_n_S; apply H12.
  symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red;
    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; apply lt_n_S; apply H12.
  simpl; rewrite H9; unfold Rminus; 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)))
       ; eapply H0.
  apply H1.
  2: rewrite H5 in H3; unfold adapted_couple_opt; 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; rewrite <- H10; pattern r at 2; 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.
Proof.
  intros; destruct (Rle_dec a b) as [Hle|Hnle];
    [ apply (StepFun_P14 Hle 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').
Proof.
  intros; destruct (Rle_dec a b) as [Hle|Hnle];
    [ apply (StepFun_P10 Hle 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.
Proof.
  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).
Proof.
  intros; unfold RiemannInt_SF; 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; 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; 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.
Proof.
  intros; induction  l1 as [| r l1 Hrecl1];
    [ simpl; ring
      | induction  l1 as [| r0 l1 Hrecl0]; simpl;
        [ 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)).
Proof.
  intros l f H; induction l;
    [ elim (lt_irrefl _ H)
      | simpl; 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).
Proof.
  intros * (x & H & H1 & H0 & H2 & H4).
  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; intros;
      induction  l as [| r l Hrecl].
  discriminate.
  unfold FF; rewrite RList_P12.
  simpl;
    change (f x0 = f (pos_Rl (mid_Rlist (cons r l) r) (S i)));
      rewrite RList_P13; try assumption; rewrite (H5 x0 H6);
        rewrite H5.
  reflexivity.
  split.
  apply Rmult_lt_reg_l with 2;
    [ prove_sup0
      | unfold Rdiv; 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; 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).
Proof.
  unfold is_subdivision; 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; decide (Rle_dec a b) with Hyp; reflexivity.
  assert (Hyp_max : Rmax a b = b).
  unfold Rmax; decide (Rle_dec a b) with Hyp; reflexivity.
  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;
          repeat split.
  apply RList_P2; assumption.
  rewrite Hyp_min; symmetry ; apply Rle_antisym.
  induction  lf as [| r lf Hreclf].
  simpl; right; symmetry ; 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; 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; 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 ; assumption | simpl; 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; 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; 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; simpl in H14; apply lt_n_Sm_le; assumption
            | simpl; 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; 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; right; symmetry ; 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 ; assumption | simpl; apply lt_n_Sn ].
  apply RList_P7; [ apply RList_P2; assumption | assumption ].
  apply StepFun_P20; rewrite RList_P11; rewrite H2; rewrite H7; simpl;
    apply lt_O_Sn.
  intros; unfold constant_D_eq, open_interval; 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; 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; rewrite RList_P12.
  change (f x = f (pos_Rl (mid_Rlist (cons r r0) r) (S i)));
    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; 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; 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; 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; 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; 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; split.
  apply Rle_trans with (pos_Rl (cons_ORlist lf lg) 0).
  right; symmetry .
  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; intro; rewrite <- H15 in H8;
    elim (lt_n_O _ H8).
  apply neq_O_lt; red; 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;
      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; 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; 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 ; apply S_pred with 0%nat; apply neq_O_lt; red;
      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 a0.
  assert (H23 : (S x0 <= x0)%nat).
  apply H20; unfold I; 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 a0; 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).
Proof.
  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).
Proof.
  unfold is_subdivision; 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; decide (Rle_dec a b) with Hyp; reflexivity.
  assert (Hyp_max : Rmax a b = b).
  unfold Rmax; decide (Rle_dec a b) with Hyp; reflexivity.
  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;
          repeat split.
  apply RList_P2; assumption.
  rewrite Hyp_min; symmetry ; apply Rle_antisym.
  induction  lf as [| r lf Hreclf].
  simpl; right; symmetry ; 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; 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; 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 ; assumption | simpl; 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; 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; 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; simpl in H14; apply lt_n_Sm_le; assumption
            | simpl; 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; 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; right; symmetry ; 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 ; assumption | simpl; apply lt_n_Sn ].
  apply RList_P7; [ apply RList_P2; assumption | assumption ].
  apply StepFun_P20; rewrite RList_P11; rewrite H7; rewrite H2; simpl;
    apply lt_O_Sn.
  unfold constant_D_eq, open_interval; 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; 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; rewrite RList_P12.
  change (g x = g (pos_Rl (mid_Rlist (cons r r0) r) (S i)));
    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; 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; 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; 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; 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; 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; split.
  apply Rle_trans with (pos_Rl (cons_ORlist lf lg) 0).
  right; symmetry ; 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; intro;
            rewrite <- H15 in H8; elim (lt_n_O _ H8) ] ].
  apply neq_O_lt; red; 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;
      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; 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; 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 ; apply S_pred with 0%nat; apply neq_O_lt; red;
    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 a0.
  assert (H23 : (S x0 <= x0)%nat);
    [ apply H20; unfold I; 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 a0; 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).
Proof.
  intros a b f g lf lg H H0; case (Rle_dec a b); intro;
    [ apply StepFun_P24 with f; assumption
      | apply StepFun_P5; apply StepFun_P24 with f;
        [ auto with real
          | apply StepFun_P5; assumption
          | apply StepFun_P5; assumption ] ].
Qed.

Lemma StepFun_P26 :
  forall (a b l:R) (f g:R -> R) (l1:Rlist),
    is_subdivision f a b l1 ->
    is_subdivision g a b l1 ->
    is_subdivision (fun x:R => f x + l * g x) a b l1.
Proof.
  intros a b l f g l1 (x0,(H0,(H1,(H2,(H3,H4)))))
    (x,(_,(_,(_,(_,H9))))).
  exists (FF l1 (fun x:R => f x + l * g x)); repeat split; try assumption.
  apply StepFun_P20; rewrite H3; auto with arith.
  intros i H8 x1 H10; unfold open_interval in H10, H9, H4;
    rewrite (H9 _ H8 _ H10); rewrite (H4 _ H8 _ H10);
      assert (H11 : l1 <> nil).
  red; intro H11; rewrite H11 in H8; elim (lt_n_O _ H8).
  destruct (RList_P19 _ H11) as (r,(r0,H12));
    rewrite H12; unfold FF;
      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)); 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; 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; 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; 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).
Proof.
  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.
Proof.
  intros a b l f g; unfold IsStepFun; 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).
Proof.
  intros a b f; unfold is_subdivision;
    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.
Proof.
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.81 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.