RList.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   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.
Local Open Scope R_scope.

Inductive Rlist : Type :=
| nil : Rlist
| cons : R -> Rlist -> Rlist.

Fixpoint In (x:R) (l:Rlist) : Prop :=
  match l with
    | nil => False
    | cons a l' => x = a \/ In x l'
  end.

Fixpoint Rlength (l:Rlist) : nat :=
  match l with
    | nil => 0%nat
    | cons a l' => S (Rlength l')
  end.

Fixpoint MaxRlist (l:Rlist) : R :=
  match l with
    | nil => 0
    | cons a l1 =>
      match l1 with
        | nil => a
        | cons a' l2 => Rmax a (MaxRlist l1)
      end
  end.

Fixpoint MinRlist (l:Rlist) : R :=
  match l with
    | nil => 1
    | cons a l1 =>
      match l1 with
        | nil => a
        | cons a' l2 => Rmin a (MinRlist l1)
      end
  end.

Lemma MaxRlist_P1 : forall (l:Rlist) (x:R), In x l -> x <= MaxRlist l.forall (l : Rlist) (x : R), In x l -> x <= MaxRlist l
Proof.forall (l : Rlist) (x : R), In x l -> x <= MaxRlist l
  intros; induction  l as [| r l Hrecl].x:R
H:In x nil
x <= MaxRlist nil
r:R
l:Rlist
x:R
H:In x (cons r l)
Hrecl:In x l -> x <= MaxRlist l
x <= MaxRlist (cons r l)
  simpl in H; elim H.r:R
l:Rlist
x:R
H:In x (cons r l)
Hrecl:In x l -> x <= MaxRlist l
x <= MaxRlist (cons r l)
  induction  l as [| r0 l Hrecl0].r, x:R
H:In x (cons r nil)
Hrecl:In x nil -> x <= MaxRlist nil
x <= MaxRlist (cons r nil)
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
x <= MaxRlist (cons r (cons r0 l))
  simpl in H; elim H; intro.r, x:R
H:x = r \/ False
Hrecl:In x nil -> x <= MaxRlist nil
H0:x = r
x <= MaxRlist (cons r nil)
r, x:R
H:x = r \/ False
Hrecl:In x nil -> x <= MaxRlist nil
H0:False
x <= MaxRlist (cons r nil)
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
x <= MaxRlist (cons r (cons r0 l))
  simpl; right; assumption.r, x:R
H:x = r \/ False
Hrecl:In x nil -> x <= MaxRlist nil
H0:False
x <= MaxRlist (cons r nil)
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
x <= MaxRlist (cons r (cons r0 l))
  elim H0.r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
x <= MaxRlist (cons r (cons r0 l))
  replace (MaxRlist (cons r (cons r0 l))) with (Rmax r (MaxRlist (cons r0 l))).r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
x <= Rmax r (MaxRlist (cons r0 l))
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
Rmax r (MaxRlist (cons r0 l)) =
MaxRlist (cons r (cons r0 l))
  simpl in H; decompose [or] H.r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
H0:x = r
x <= Rmax r (MaxRlist (cons r0 l))
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
H1:x = r0
x <= Rmax r (MaxRlist (cons r0 l))
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
H1:In x l
x <= Rmax r (MaxRlist (cons r0 l))
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
Rmax r (MaxRlist (cons r0 l)) =
MaxRlist (cons r (cons r0 l))
  rewrite H0; apply RmaxLess1.r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
H1:x = r0
x <= Rmax r (MaxRlist (cons r0 l))
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
H1:In x l
x <= Rmax r (MaxRlist (cons r0 l))
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
Rmax r (MaxRlist (cons r0 l)) =
MaxRlist (cons r (cons r0 l))
  unfold Rmax; case (Rle_dec r (MaxRlist (cons r0 l))); intro.r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
H1:x = r0
r1:r <= MaxRlist (cons r0 l)
x <= MaxRlist (cons r0 l)
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
H1:x = r0
n:~ r <= MaxRlist (cons r0 l)
x <= r
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
H1:In x l
x <= Rmax r (MaxRlist (cons r0 l))
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
Rmax r (MaxRlist (cons r0 l)) =
MaxRlist (cons r (cons r0 l))
  apply Hrecl; simpl; tauto.r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
H1:x = r0
n:~ r <= MaxRlist (cons r0 l)
x <= r
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
H1:In x l
x <= Rmax r (MaxRlist (cons r0 l))
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
Rmax r (MaxRlist (cons r0 l)) =
MaxRlist (cons r (cons r0 l))
  apply Rle_trans with (MaxRlist (cons r0 l));
    [ apply Hrecl; simpl; tauto | left; auto with real ].r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
H1:In x l
x <= Rmax r (MaxRlist (cons r0 l))
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
Rmax r (MaxRlist (cons r0 l)) =
MaxRlist (cons r (cons r0 l))
  unfold Rmax; case (Rle_dec r (MaxRlist (cons r0 l))); intro.r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
H1:In x l
r1:r <= MaxRlist (cons r0 l)
x <= MaxRlist (cons r0 l)
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
H1:In x l
n:~ r <= MaxRlist (cons r0 l)
x <= r
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
Rmax r (MaxRlist (cons r0 l)) =
MaxRlist (cons r (cons r0 l))
  apply Hrecl; simpl; tauto.r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
H1:In x l
n:~ r <= MaxRlist (cons r0 l)
x <= r
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
Rmax r (MaxRlist (cons r0 l)) =
MaxRlist (cons r (cons r0 l))
  apply Rle_trans with (MaxRlist (cons r0 l));
    [ apply Hrecl; simpl; tauto | left; auto with real ].r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> x <= MaxRlist (cons r0 l)
Hrecl0:In x (cons r l) ->
(In x l -> x <= MaxRlist l) ->
x <= MaxRlist (cons r l)
Rmax r (MaxRlist (cons r0 l)) =
MaxRlist (cons r (cons r0 l))
  reflexivity.
Qed.

Fixpoint AbsList (l:Rlist) (x:R) : Rlist :=
  match l with
    | nil => nil
    | cons a l' => cons (Rabs (a - x) / 2) (AbsList l' x)
  end.

Lemma MinRlist_P1 : forall (l:Rlist) (x:R), In x l -> MinRlist l <= x.forall (l : Rlist) (x : R), In x l -> MinRlist l <= x
Proof.forall (l : Rlist) (x : R), In x l -> MinRlist l <= x
  intros; induction  l as [| r l Hrecl].x:R
H:In x nil
MinRlist nil <= x
r:R
l:Rlist
x:R
H:In x (cons r l)
Hrecl:In x l -> MinRlist l <= x
MinRlist (cons r l) <= x
  simpl in H; elim H.r:R
l:Rlist
x:R
H:In x (cons r l)
Hrecl:In x l -> MinRlist l <= x
MinRlist (cons r l) <= x
  induction  l as [| r0 l Hrecl0].r, x:R
H:In x (cons r nil)
Hrecl:In x nil -> MinRlist nil <= x
MinRlist (cons r nil) <= x
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
MinRlist (cons r (cons r0 l)) <= x
  simpl in H; elim H; intro.r, x:R
H:x = r \/ False
Hrecl:In x nil -> MinRlist nil <= x
H0:x = r
MinRlist (cons r nil) <= x
r, x:R
H:x = r \/ False
Hrecl:In x nil -> MinRlist nil <= x
H0:False
MinRlist (cons r nil) <= x
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
MinRlist (cons r (cons r0 l)) <= x
  simpl; right; symmetry ; assumption.r, x:R
H:x = r \/ False
Hrecl:In x nil -> MinRlist nil <= x
H0:False
MinRlist (cons r nil) <= x
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
MinRlist (cons r (cons r0 l)) <= x
  elim H0.r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
MinRlist (cons r (cons r0 l)) <= x
  replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))).r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
Rmin r (MinRlist (cons r0 l)) <= x
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
Rmin r (MinRlist (cons r0 l)) =
MinRlist (cons r (cons r0 l))
  simpl in H; decompose [or] H.r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H0:x = r
Rmin r (MinRlist (cons r0 l)) <= x
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:x = r0
Rmin r (MinRlist (cons r0 l)) <= x
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:In x l
Rmin r (MinRlist (cons r0 l)) <= x
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
Rmin r (MinRlist (cons r0 l)) =
MinRlist (cons r (cons r0 l))
  rewrite H0; apply Rmin_l.r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:x = r0
Rmin r (MinRlist (cons r0 l)) <= x
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:In x l
Rmin r (MinRlist (cons r0 l)) <= x
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
Rmin r (MinRlist (cons r0 l)) =
MinRlist (cons r (cons r0 l))
  unfold Rmin; case (Rle_dec r (MinRlist (cons r0 l))); intro.r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:x = r0
r1:r <= MinRlist (cons r0 l)
r <= x
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:x = r0
n:~ r <= MinRlist (cons r0 l)
MinRlist (cons r0 l) <= x
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:In x l
Rmin r (MinRlist (cons r0 l)) <= x
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
Rmin r (MinRlist (cons r0 l)) =
MinRlist (cons r (cons r0 l))
  apply Rle_trans with (MinRlist (cons r0 l)).r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:x = r0
r1:r <= MinRlist (cons r0 l)
r <= MinRlist (cons r0 l)
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:x = r0
r1:r <= MinRlist (cons r0 l)
MinRlist (cons r0 l) <= x
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:x = r0
n:~ r <= MinRlist (cons r0 l)
MinRlist (cons r0 l) <= x
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:In x l
Rmin r (MinRlist (cons r0 l)) <= x
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
Rmin r (MinRlist (cons r0 l)) =
MinRlist (cons r (cons r0 l))
  assumption.r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:x = r0
r1:r <= MinRlist (cons r0 l)
MinRlist (cons r0 l) <= x
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:x = r0
n:~ r <= MinRlist (cons r0 l)
MinRlist (cons r0 l) <= x
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:In x l
Rmin r (MinRlist (cons r0 l)) <= x
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
Rmin r (MinRlist (cons r0 l)) =
MinRlist (cons r (cons r0 l))
  apply Hrecl; simpl; tauto.r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:x = r0
n:~ r <= MinRlist (cons r0 l)
MinRlist (cons r0 l) <= x
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:In x l
Rmin r (MinRlist (cons r0 l)) <= x
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
Rmin r (MinRlist (cons r0 l)) =
MinRlist (cons r (cons r0 l))
  apply Hrecl; simpl; tauto.r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:In x l
Rmin r (MinRlist (cons r0 l)) <= x
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
Rmin r (MinRlist (cons r0 l)) =
MinRlist (cons r (cons r0 l))
  apply Rle_trans with (MinRlist (cons r0 l)).r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:In x l
Rmin r (MinRlist (cons r0 l)) <= MinRlist (cons r0 l)
r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:In x l
MinRlist (cons r0 l) <= x
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
Rmin r (MinRlist (cons r0 l)) =
MinRlist (cons r (cons r0 l))
  apply Rmin_r.r, r0:R
l:Rlist
x:R
H:x = r \/ x = r0 \/ In x l
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
H1:In x l
MinRlist (cons r0 l) <= x
r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
Rmin r (MinRlist (cons r0 l)) =
MinRlist (cons r (cons r0 l))
  apply Hrecl; simpl; tauto.r, r0:R
l:Rlist
x:R
H:In x (cons r (cons r0 l))
Hrecl:In x (cons r0 l) -> MinRlist (cons r0 l) <= x
Hrecl0:In x (cons r l) ->
(In x l -> MinRlist l <= x) ->
MinRlist (cons r l) <= x
Rmin r (MinRlist (cons r0 l)) =
MinRlist (cons r (cons r0 l))
  reflexivity.
Qed.

Lemma AbsList_P1 :
  forall (l:Rlist) (x y:R), In y l -> In (Rabs (y - x) / 2) (AbsList l x).forall (l : Rlist) (x y : R),
In y l -> In (Rabs (y - x) / 2) (AbsList l x)
Proof.forall (l : Rlist) (x y : R),
In y l -> In (Rabs (y - x) / 2) (AbsList l x)
  intros; induction  l as [| r l Hrecl].x, y:R
H:In y nil
In (Rabs (y - x) / 2) (AbsList nil x)
r:R
l:Rlist
x, y:R
H:In y (cons r l)
Hrecl:In y l -> In (Rabs (y - x) / 2) (AbsList l x)
In (Rabs (y - x) / 2) (AbsList (cons r l) x)
  elim H.r:R
l:Rlist
x, y:R
H:In y (cons r l)
Hrecl:In y l -> In (Rabs (y - x) / 2) (AbsList l x)
In (Rabs (y - x) / 2) (AbsList (cons r l) x)
  simpl; simpl in H; elim H; intro.r:R
l:Rlist
x, y:R
H:y = r \/ In y l
Hrecl:In y l -> In (Rabs (y - x) / 2) (AbsList l x)
H0:y = r
Rabs (y - x) / 2 = Rabs (r - x) / 2 \/
In (Rabs (y - x) / 2) (AbsList l x)
r:R
l:Rlist
x, y:R
H:y = r \/ In y l
Hrecl:In y l -> In (Rabs (y - x) / 2) (AbsList l x)
H0:In y l
Rabs (y - x) / 2 = Rabs (r - x) / 2 \/
In (Rabs (y - x) / 2) (AbsList l x)
  left; rewrite H0; reflexivity.r:R
l:Rlist
x, y:R
H:y = r \/ In y l
Hrecl:In y l -> In (Rabs (y - x) / 2) (AbsList l x)
H0:In y l
Rabs (y - x) / 2 = Rabs (r - x) / 2 \/
In (Rabs (y - x) / 2) (AbsList l x)
  right; apply Hrecl; assumption.
Qed.

Lemma MinRlist_P2 :
  forall l:Rlist, (forall y:R, In y l -> 0 < y) -> 0 < MinRlist l.forall l : Rlist,
(forall y : R, In y l -> 0 < y) -> 0 < MinRlist l
Proof.forall l : Rlist,
(forall y : R, In y l -> 0 < y) -> 0 < MinRlist l
  intros; induction  l as [| r l Hrecl].H:forall y : R, In y nil -> 0 < y
0 < MinRlist nil
r:R
l:Rlist
H:forall y : R, In y (cons r l) -> 0 < y
Hrecl:(forall y : R, In y l -> 0 < y) ->
0 < MinRlist l
0 < MinRlist (cons r l)
  apply Rlt_0_1.r:R
l:Rlist
H:forall y : R, In y (cons r l) -> 0 < y
Hrecl:(forall y : R, In y l -> 0 < y) ->
0 < MinRlist l
0 < MinRlist (cons r l)
  induction  l as [| r0 l Hrecl0].r:R
H:forall y : R, In y (cons r nil) -> 0 < y
Hrecl:(forall y : R, In y nil -> 0 < y) ->
0 < MinRlist nil
0 < MinRlist (cons r nil)
r, r0:R
l:Rlist
H:forall y : R, In y (cons r (cons r0 l)) -> 0 < y
Hrecl:(forall y : R, In y (cons r0 l) -> 0 < y) ->
0 < MinRlist (cons r0 l)
Hrecl0:(forall y : R, In y (cons r l) -> 0 < y) ->
((forall y : R, In y l -> 0 < y) ->
 0 < MinRlist l) -> 0 < MinRlist (cons r l)
0 < MinRlist (cons r (cons r0 l))
  simpl; apply H; simpl; tauto.r, r0:R
l:Rlist
H:forall y : R, In y (cons r (cons r0 l)) -> 0 < y
Hrecl:(forall y : R, In y (cons r0 l) -> 0 < y) ->
0 < MinRlist (cons r0 l)
Hrecl0:(forall y : R, In y (cons r l) -> 0 < y) ->
((forall y : R, In y l -> 0 < y) ->
 0 < MinRlist l) -> 0 < MinRlist (cons r l)
0 < MinRlist (cons r (cons r0 l))
  replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))).r, r0:R
l:Rlist
H:forall y : R, In y (cons r (cons r0 l)) -> 0 < y
Hrecl:(forall y : R, In y (cons r0 l) -> 0 < y) ->
0 < MinRlist (cons r0 l)
Hrecl0:(forall y : R, In y (cons r l) -> 0 < y) ->
((forall y : R, In y l -> 0 < y) ->
 0 < MinRlist l) -> 0 < MinRlist (cons r l)
0 < Rmin r (MinRlist (cons r0 l))
r, r0:R
l:Rlist
H:forall y : R, In y (cons r (cons r0 l)) -> 0 < y
Hrecl:(forall y : R, In y (cons r0 l) -> 0 < y) ->
0 < MinRlist (cons r0 l)
Hrecl0:(forall y : R, In y (cons r l) -> 0 < y) ->
((forall y : R, In y l -> 0 < y) ->
 0 < MinRlist l) -> 0 < MinRlist (cons r l)
Rmin r (MinRlist (cons r0 l)) =
MinRlist (cons r (cons r0 l))
  unfold Rmin; case (Rle_dec r (MinRlist (cons r0 l))); intro.r, r0:R
l:Rlist
H:forall y : R, In y (cons r (cons r0 l)) -> 0 < y
Hrecl:(forall y : R, In y (cons r0 l) -> 0 < y) ->
0 < MinRlist (cons r0 l)
Hrecl0:(forall y : R, In y (cons r l) -> 0 < y) ->
((forall y : R, In y l -> 0 < y) ->
 0 < MinRlist l) -> 0 < MinRlist (cons r l)
r1:r <= MinRlist (cons r0 l)
0 < r
r, r0:R
l:Rlist
H:forall y : R, In y (cons r (cons r0 l)) -> 0 < y
Hrecl:(forall y : R, In y (cons r0 l) -> 0 < y) ->
0 < MinRlist (cons r0 l)
Hrecl0:(forall y : R, In y (cons r l) -> 0 < y) ->
((forall y : R, In y l -> 0 < y) ->
 0 < MinRlist l) -> 0 < MinRlist (cons r l)
n:~ r <= MinRlist (cons r0 l)
0 < MinRlist (cons r0 l)
r, r0:R
l:Rlist
H:forall y : R, In y (cons r (cons r0 l)) -> 0 < y
Hrecl:(forall y : R, In y (cons r0 l) -> 0 < y) ->
0 < MinRlist (cons r0 l)
Hrecl0:(forall y : R, In y (cons r l) -> 0 < y) ->
((forall y : R, In y l -> 0 < y) ->
 0 < MinRlist l) -> 0 < MinRlist (cons r l)
Rmin r (MinRlist (cons r0 l)) =
MinRlist (cons r (cons r0 l))
  apply H; simpl; tauto.r, r0:R
l:Rlist
H:forall y : R, In y (cons r (cons r0 l)) -> 0 < y
Hrecl:(forall y : R, In y (cons r0 l) -> 0 < y) ->
0 < MinRlist (cons r0 l)
Hrecl0:(forall y : R, In y (cons r l) -> 0 < y) ->
((forall y : R, In y l -> 0 < y) ->
 0 < MinRlist l) -> 0 < MinRlist (cons r l)
n:~ r <= MinRlist (cons r0 l)
0 < MinRlist (cons r0 l)
r, r0:R
l:Rlist
H:forall y : R, In y (cons r (cons r0 l)) -> 0 < y
Hrecl:(forall y : R, In y (cons r0 l) -> 0 < y) ->
0 < MinRlist (cons r0 l)
Hrecl0:(forall y : R, In y (cons r l) -> 0 < y) ->
((forall y : R, In y l -> 0 < y) ->
 0 < MinRlist l) -> 0 < MinRlist (cons r l)
Rmin r (MinRlist (cons r0 l)) =
MinRlist (cons r (cons r0 l))
  apply Hrecl; intros; apply H; simpl; simpl in H0; tauto.r, r0:R
l:Rlist
H:forall y : R, In y (cons r (cons r0 l)) -> 0 < y
Hrecl:(forall y : R, In y (cons r0 l) -> 0 < y) ->
0 < MinRlist (cons r0 l)
Hrecl0:(forall y : R, In y (cons r l) -> 0 < y) ->
((forall y : R, In y l -> 0 < y) ->
 0 < MinRlist l) -> 0 < MinRlist (cons r l)
Rmin r (MinRlist (cons r0 l)) =
MinRlist (cons r (cons r0 l))
  reflexivity.
Qed.

Lemma AbsList_P2 :
  forall (l:Rlist) (x y:R),
    In y (AbsList l x) ->  exists z : R, In z l /\ y = Rabs (z - x) / 2.forall (l : Rlist) (x y : R),
In y (AbsList l x) ->
exists z : R, In z l /\ y = Rabs (z - x) / 2
Proof.forall (l : Rlist) (x y : R),
In y (AbsList l x) ->
exists z : R, In z l /\ y = Rabs (z - x) / 2
  intros; induction  l as [| r l Hrecl].x, y:R
H:In y (AbsList nil x)
exists z : R, In z nil /\ y = Rabs (z - x) / 2
r:R
l:Rlist
x, y:R
H:In y (AbsList (cons r l) x)
Hrecl:In y (AbsList l x) ->
exists z : R, In z l /\ y = Rabs (z - x) / 2
exists z : R, In z (cons r l) /\ y = Rabs (z - x) / 2
  elim H.r:R
l:Rlist
x, y:R
H:In y (AbsList (cons r l) x)
Hrecl:In y (AbsList l x) ->
exists z : R, In z l /\ y = Rabs (z - x) / 2
exists z : R, In z (cons r l) /\ y = Rabs (z - x) / 2
  elim H; intro.r:R
l:Rlist
x, y:R
H:In y (AbsList (cons r l) x)
Hrecl:In y (AbsList l x) ->
exists z : R, In z l /\ y = Rabs (z - x) / 2
H0:y = Rabs (r - x) / 2
exists z : R, In z (cons r l) /\ y = Rabs (z - x) / 2
r:R
l:Rlist
x, y:R
H:In y (AbsList (cons r l) x)
Hrecl:In y (AbsList l x) ->
exists z : R, In z l /\ y = Rabs (z - x) / 2
H0:In y (AbsList l x)
exists z : R, In z (cons r l) /\ y = Rabs (z - x) / 2
  exists r; split.r:R
l:Rlist
x, y:R
H:In y (AbsList (cons r l) x)
Hrecl:In y (AbsList l x) ->
exists z : R, In z l /\ y = Rabs (z - x) / 2
H0:y = Rabs (r - x) / 2
In r (cons r l)
r:R
l:Rlist
x, y:R
H:In y (AbsList (cons r l) x)
Hrecl:In y (AbsList l x) ->
exists z : R, In z l /\ y = Rabs (z - x) / 2
H0:y = Rabs (r - x) / 2
y = Rabs (r - x) / 2
r:R
l:Rlist
x, y:R
H:In y (AbsList (cons r l) x)
Hrecl:In y (AbsList l x) ->
exists z : R, In z l /\ y = Rabs (z - x) / 2
H0:In y (AbsList l x)
exists z : R, In z (cons r l) /\ y = Rabs (z - x) / 2
  simpl; tauto.r:R
l:Rlist
x, y:R
H:In y (AbsList (cons r l) x)
Hrecl:In y (AbsList l x) ->
exists z : R, In z l /\ y = Rabs (z - x) / 2
H0:y = Rabs (r - x) / 2
y = Rabs (r - x) / 2
r:R
l:Rlist
x, y:R
H:In y (AbsList (cons r l) x)
Hrecl:In y (AbsList l x) ->
exists z : R, In z l /\ y = Rabs (z - x) / 2
H0:In y (AbsList l x)
exists z : R, In z (cons r l) /\ y = Rabs (z - x) / 2
  assumption.r:R
l:Rlist
x, y:R
H:In y (AbsList (cons r l) x)
Hrecl:In y (AbsList l x) ->
exists z : R, In z l /\ y = Rabs (z - x) / 2
H0:In y (AbsList l x)
exists z : R, In z (cons r l) /\ y = Rabs (z - x) / 2
  assert (H1 := Hrecl H0); elim H1; intros; elim H2; clear H2; intros;
    exists x0; simpl; simpl in H2; tauto.
Qed.

Lemma MaxRlist_P2 :
  forall l:Rlist, (exists y : R, In y l) -> In (MaxRlist l) l.forall l : Rlist,
(exists y : R, In y l) -> In (MaxRlist l) l
Proof.forall l : Rlist,
(exists y : R, In y l) -> In (MaxRlist l) l
  intros; induction  l as [| r l Hrecl].H:exists y : R, In y nil
In (MaxRlist nil) nil
r:R
l:Rlist
H:exists y : R, In y (cons r l)
Hrecl:(exists y : R, In y l) -> In (MaxRlist l) l
In (MaxRlist (cons r l)) (cons r l)
  simpl in H; elim H; trivial.r:R
l:Rlist
H:exists y : R, In y (cons r l)
Hrecl:(exists y : R, In y l) -> In (MaxRlist l) l
In (MaxRlist (cons r l)) (cons r l)
  induction  l as [| r0 l Hrecl0].r:R
H:exists y : R, In y (cons r nil)
Hrecl:(exists y : R, In y nil) ->
In (MaxRlist nil) nil
In (MaxRlist (cons r nil)) (cons r nil)
r, r0:R
l:Rlist
H:exists y : R, In y (cons r (cons r0 l))
Hrecl:(exists y : R, In y (cons r0 l)) ->
In (MaxRlist (cons r0 l)) (cons r0 l)
Hrecl0:(exists y : R, In y (cons r l)) ->
((exists y : R, In y l) -> In (MaxRlist l) l) ->
In (MaxRlist (cons r l)) (cons r l)
In (MaxRlist (cons r (cons r0 l)))
  (cons r (cons r0 l))
  simpl; left; reflexivity.r, r0:R
l:Rlist
H:exists y : R, In y (cons r (cons r0 l))
Hrecl:(exists y : R, In y (cons r0 l)) ->
In (MaxRlist (cons r0 l)) (cons r0 l)
Hrecl0:(exists y : R, In y (cons r l)) ->
((exists y : R, In y l) -> In (MaxRlist l) l) ->
In (MaxRlist (cons r l)) (cons r l)
In (MaxRlist (cons r (cons r0 l)))
  (cons r (cons r0 l))
  change (In (Rmax r (MaxRlist (cons r0 l))) (cons r (cons r0 l)));
    unfold Rmax; case (Rle_dec r (MaxRlist (cons r0 l)));
      intro.r, r0:R
l:Rlist
H:exists y : R, In y (cons r (cons r0 l))
Hrecl:(exists y : R, In y (cons r0 l)) ->
In (MaxRlist (cons r0 l)) (cons r0 l)
Hrecl0:(exists y : R, In y (cons r l)) ->
((exists y : R, In y l) -> In (MaxRlist l) l) ->
In (MaxRlist (cons r l)) (cons r l)
r1:r <= MaxRlist (cons r0 l)
In (MaxRlist (cons r0 l)) (cons r (cons r0 l))
r, r0:R
l:Rlist
H:exists y : R, In y (cons r (cons r0 l))
Hrecl:(exists y : R, In y (cons r0 l)) ->
In (MaxRlist (cons r0 l)) (cons r0 l)
Hrecl0:(exists y : R, In y (cons r l)) ->
((exists y : R, In y l) -> In (MaxRlist l) l) ->
In (MaxRlist (cons r l)) (cons r l)
n:~ r <= MaxRlist (cons r0 l)
In r (cons r (cons r0 l))
  right; apply Hrecl; exists r0; left; reflexivity.r, r0:R
l:Rlist
H:exists y : R, In y (cons r (cons r0 l))
Hrecl:(exists y : R, In y (cons r0 l)) ->
In (MaxRlist (cons r0 l)) (cons r0 l)
Hrecl0:(exists y : R, In y (cons r l)) ->
((exists y : R, In y l) -> In (MaxRlist l) l) ->
In (MaxRlist (cons r l)) (cons r l)
n:~ r <= MaxRlist (cons r0 l)
In r (cons r (cons r0 l))
  left; reflexivity.
Qed.

Fixpoint pos_Rl (l:Rlist) (i:nat) : R :=
  match l with
    | nil => 0
    | cons a l' => match i with
                     | O => a
                     | S i' => pos_Rl l' i'
                   end
  end.

Lemma pos_Rl_P1 :
  forall (l:Rlist) (a:R),
    (0 < Rlength l)%nat ->
    pos_Rl (cons a l) (Rlength l) = pos_Rl l (pred (Rlength l)).forall (l : Rlist) (a : R),
(0 < Rlength l)%nat ->
pos_Rl (cons a l) (Rlength l) =
pos_Rl l (Init.Nat.pred (Rlength l))
Proof.forall (l : Rlist) (a : R),
(0 < Rlength l)%nat ->
pos_Rl (cons a l) (Rlength l) =
pos_Rl l (Init.Nat.pred (Rlength l))
  intros; induction  l as [| r l Hrecl];
    [ elim (lt_n_O _ H)
      | simpl; case (Rlength l); [ reflexivity | intro; reflexivity ] ].
Qed.

Lemma pos_Rl_P2 :
  forall (l:Rlist) (x:R),
    In x l <-> (exists i : nat, (i < Rlength l)%nat /\ x = pos_Rl l i).forall (l : Rlist) (x : R),
In x l <->
(exists i : nat, (i < Rlength l)%nat /\ x = pos_Rl l i)
Proof.forall (l : Rlist) (x : R),
In x l <->
(exists i : nat, (i < Rlength l)%nat /\ x = pos_Rl l i)
  intros; induction  l as [| r l Hrecl].x:R
In x nil <->
(exists i : nat,
   (i < Rlength nil)%nat /\ x = pos_Rl nil i)
r:R
l:Rlist
x:R
Hrecl:In x l <->
(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i)
In x (cons r l) <->
(exists i : nat,
   (i < Rlength (cons r l))%nat /\
   x = pos_Rl (cons r l) i)
  split; intro;
    [ elim H | elim H; intros; elim H0; intros; elim (lt_n_O _ H1) ].r:R
l:Rlist
x:R
Hrecl:In x l <->
(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i)
In x (cons r l) <->
(exists i : nat,
   (i < Rlength (cons r l))%nat /\
   x = pos_Rl (cons r l) i)
  split; intro.r:R
l:Rlist
x:R
Hrecl:In x l <->
(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i)
H:In x (cons r l)
exists i : nat,
  (i < Rlength (cons r l))%nat /\
  x = pos_Rl (cons r l) i
r:R
l:Rlist
x:R
Hrecl:In x l <->
(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i)
H:exists i : nat,
  (i < Rlength (cons r l))%nat /\
  x = pos_Rl (cons r l) i
In x (cons r l)
  elim H; intro.r:R
l:Rlist
x:R
Hrecl:In x l <->
(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i)
H:In x (cons r l)
H0:x = r
exists i : nat,
  (i < Rlength (cons r l))%nat /\
  x = pos_Rl (cons r l) i
r:R
l:Rlist
x:R
Hrecl:In x l <->
(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i)
H:In x (cons r l)
H0:In x l
exists i : nat,
  (i < Rlength (cons r l))%nat /\
  x = pos_Rl (cons r l) i
r:R
l:Rlist
x:R
Hrecl:In x l <->
(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i)
H:exists i : nat,
  (i < Rlength (cons r l))%nat /\
  x = pos_Rl (cons r l) i
In x (cons r l)
  exists 0%nat; split;
    [ simpl; apply lt_O_Sn | simpl; apply H0 ].r:R
l:Rlist
x:R
Hrecl:In x l <->
(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i)
H:In x (cons r l)
H0:In x l
exists i : nat,
  (i < Rlength (cons r l))%nat /\
  x = pos_Rl (cons r l) i
r:R
l:Rlist
x:R
Hrecl:In x l <->
(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i)
H:exists i : nat,
  (i < Rlength (cons r l))%nat /\
  x = pos_Rl (cons r l) i
In x (cons r l)
  elim Hrecl; intros; assert (H3 := H1 H0); elim H3; intros; elim H4; intros;
    exists (S x0); split;
      [ simpl; apply lt_n_S; assumption | simpl; assumption ].r:R
l:Rlist
x:R
Hrecl:In x l <->
(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i)
H:exists i : nat,
  (i < Rlength (cons r l))%nat /\
  x = pos_Rl (cons r l) i
In x (cons r l)
  elim H; intros; elim H0; intros; destruct (zerop x0) as [->|].r:R
l:Rlist
x:R
Hrecl:In x l <->
(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i)
H:exists i : nat,
  (i < Rlength (cons r l))%nat /\
  x = pos_Rl (cons r l) i
H2:x = pos_Rl (cons r l) 0
H1:(0 < Rlength (cons r l))%nat
H0:(0 < Rlength (cons r l))%nat /\
x = pos_Rl (cons r l) 0
In x (cons r l)
r:R
l:Rlist
x:R
Hrecl:In x l <->
(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i)
H:exists i : nat,
  (i < Rlength (cons r l))%nat /\
  x = pos_Rl (cons r l) i
x0:nat
H0:(x0 < Rlength (cons r l))%nat /\
x = pos_Rl (cons r l) x0
H1:(x0 < Rlength (cons r l))%nat
H2:x = pos_Rl (cons r l) x0
l0:(0 < x0)%nat
In x (cons r l)
  simpl in H2; left; assumption.r:R
l:Rlist
x:R
Hrecl:In x l <->
(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i)
H:exists i : nat,
  (i < Rlength (cons r l))%nat /\
  x = pos_Rl (cons r l) i
x0:nat
H0:(x0 < Rlength (cons r l))%nat /\
x = pos_Rl (cons r l) x0
H1:(x0 < Rlength (cons r l))%nat
H2:x = pos_Rl (cons r l) x0
l0:(0 < x0)%nat
In x (cons r l)
  right; elim Hrecl; intros H4 H5; apply H5; assert (H6 : S (pred x0) = x0).r:R
l:Rlist
x:R
Hrecl:In x l <->
(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i)
H:exists i : nat,
  (i < Rlength (cons r l))%nat /\
  x = pos_Rl (cons r l) i
x0:nat
H0:(x0 < Rlength (cons r l))%nat /\
x = pos_Rl (cons r l) x0
H1:(x0 < Rlength (cons r l))%nat
H2:x = pos_Rl (cons r l) x0
l0:(0 < x0)%nat
H4:In x l ->
exists i : nat,
  (i < Rlength l)%nat /\ x = pos_Rl l i
H5:(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i) ->
In x l
S (Init.Nat.pred x0) = x0
r:R
l:Rlist
x:R
Hrecl:In x l <->
(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i)
H:exists i : nat,
  (i < Rlength (cons r l))%nat /\
  x = pos_Rl (cons r l) i
x0:nat
H0:(x0 < Rlength (cons r l))%nat /\
x = pos_Rl (cons r l) x0
H1:(x0 < Rlength (cons r l))%nat
H2:x = pos_Rl (cons r l) x0
l0:(0 < x0)%nat
H4:In x l ->
exists i : nat,
  (i < Rlength l)%nat /\ x = pos_Rl l i
H5:(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i) ->
In x l
H6:S (Init.Nat.pred x0) = x0
exists i : nat, (i < Rlength l)%nat /\ x = pos_Rl l i
  symmetry ; apply S_pred with 0%nat; assumption.r:R
l:Rlist
x:R
Hrecl:In x l <->
(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i)
H:exists i : nat,
  (i < Rlength (cons r l))%nat /\
  x = pos_Rl (cons r l) i
x0:nat
H0:(x0 < Rlength (cons r l))%nat /\
x = pos_Rl (cons r l) x0
H1:(x0 < Rlength (cons r l))%nat
H2:x = pos_Rl (cons r l) x0
l0:(0 < x0)%nat
H4:In x l ->
exists i : nat,
  (i < Rlength l)%nat /\ x = pos_Rl l i
H5:(exists i : nat,
   (i < Rlength l)%nat /\ x = pos_Rl l i) ->
In x l
H6:S (Init.Nat.pred x0) = x0
exists i : nat, (i < Rlength l)%nat /\ x = pos_Rl l i
  exists (pred x0); split;
    [ simpl in H1; apply lt_S_n; rewrite H6; assumption
      | rewrite <- H6 in H2; simpl in H2; assumption ].
Qed.

Lemma Rlist_P1 :
  forall (l:Rlist) (P:R -> R -> Prop),
    (forall x:R, In x l ->  exists y : R, P x y) ->
    exists l' : Rlist,
      Rlength l = Rlength l' /\
      (forall i:nat, (i < Rlength l)%nat -> P (pos_Rl l i) (pos_Rl l' i)).forall (l : Rlist) (P : R -> R -> Prop),
(forall x : R, In x l -> exists y : R, P x y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat -> P (pos_Rl l i) (pos_Rl l' i))
Proof.forall (l : Rlist) (P : R -> R -> Prop),
(forall x : R, In x l -> exists y : R, P x y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat -> P (pos_Rl l i) (pos_Rl l' i))
  intros; induction  l as [| r l Hrecl].P:R -> R -> Prop
H:forall x : R, In x nil -> exists y : R, P x y
exists l' : Rlist,
  Rlength nil = Rlength l' /\
  (forall i : nat,
   (i < Rlength nil)%nat ->
   P (pos_Rl nil i) (pos_Rl l' i))
r:R
l:Rlist
P:R -> R -> Prop
H:forall x : R,
In x (cons r l) -> exists y : R, P x y
Hrecl:(forall x : R, In x l -> exists y : R, P x y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat ->
   P (pos_Rl l i) (pos_Rl l' i))
exists l' : Rlist,
  Rlength (cons r l) = Rlength l' /\
  (forall i : nat,
   (i < Rlength (cons r l))%nat ->
   P (pos_Rl (cons r l) i) (pos_Rl l' i))
  exists nil; intros; split;
    [ reflexivity | intros; simpl in H0; elim (lt_n_O _ H0) ].r:R
l:Rlist
P:R -> R -> Prop
H:forall x : R,
In x (cons r l) -> exists y : R, P x y
Hrecl:(forall x : R, In x l -> exists y : R, P x y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat ->
   P (pos_Rl l i) (pos_Rl l' i))
exists l' : Rlist,
  Rlength (cons r l) = Rlength l' /\
  (forall i : nat,
   (i < Rlength (cons r l))%nat ->
   P (pos_Rl (cons r l) i) (pos_Rl l' i))
  assert (H0 : In r (cons r l)).r:R
l:Rlist
P:R -> R -> Prop
H:forall x : R,
In x (cons r l) -> exists y : R, P x y
Hrecl:(forall x : R, In x l -> exists y : R, P x y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat ->
   P (pos_Rl l i) (pos_Rl l' i))
In r (cons r l)
r:R
l:Rlist
P:R -> R -> Prop
H:forall x : R,
In x (cons r l) -> exists y : R, P x y
Hrecl:(forall x : R, In x l -> exists y : R, P x y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat ->
   P (pos_Rl l i) (pos_Rl l' i))
H0:In r (cons r l)
exists l' : Rlist,
  Rlength (cons r l) = Rlength l' /\
  (forall i : nat,
   (i < Rlength (cons r l))%nat ->
   P (pos_Rl (cons r l) i) (pos_Rl l' i))
  simpl; left; reflexivity.r:R
l:Rlist
P:R -> R -> Prop
H:forall x : R,
In x (cons r l) -> exists y : R, P x y
Hrecl:(forall x : R, In x l -> exists y : R, P x y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat ->
   P (pos_Rl l i) (pos_Rl l' i))
H0:In r (cons r l)
exists l' : Rlist,
  Rlength (cons r l) = Rlength l' /\
  (forall i : nat,
   (i < Rlength (cons r l))%nat ->
   P (pos_Rl (cons r l) i) (pos_Rl l' i))
  assert (H1 := H _ H0);
    assert (H2 : forall x:R, In x l ->  exists y : R, P x y).r:R
l:Rlist
P:R -> R -> Prop
H:forall x : R,
In x (cons r l) -> exists y : R, P x y
Hrecl:(forall x : R, In x l -> exists y : R, P x y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat ->
   P (pos_Rl l i) (pos_Rl l' i))
H0:In r (cons r l)
H1:exists y : R, P r y
forall x : R, In x l -> exists y : R, P x y
r:R
l:Rlist
P:R -> R -> Prop
H:forall x : R,
In x (cons r l) -> exists y : R, P x y
Hrecl:(forall x : R, In x l -> exists y : R, P x y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat ->
   P (pos_Rl l i) (pos_Rl l' i))
H0:In r (cons r l)
H1:exists y : R, P r y
H2:forall x : R, In x l -> exists y : R, P x y
exists l' : Rlist,
  Rlength (cons r l) = Rlength l' /\
  (forall i : nat,
   (i < Rlength (cons r l))%nat ->
   P (pos_Rl (cons r l) i) (pos_Rl l' i))
  intros; apply H; simpl; right; assumption.r:R
l:Rlist
P:R -> R -> Prop
H:forall x : R,
In x (cons r l) -> exists y : R, P x y
Hrecl:(forall x : R, In x l -> exists y : R, P x y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat ->
   P (pos_Rl l i) (pos_Rl l' i))
H0:In r (cons r l)
H1:exists y : R, P r y
H2:forall x : R, In x l -> exists y : R, P x y
exists l' : Rlist,
  Rlength (cons r l) = Rlength l' /\
  (forall i : nat,
   (i < Rlength (cons r l))%nat ->
   P (pos_Rl (cons r l) i) (pos_Rl l' i))
  assert (H3 := Hrecl H2); elim H1; intros; elim H3; intros; exists (cons x x0);
    intros; elim H5; clear H5; intros; split.r:R
l:Rlist
P:R -> R -> Prop
H:forall x1 : R,
In x1 (cons r l) -> exists y : R, P x1 y
Hrecl:(forall x1 : R,
 In x1 l -> exists y : R, P x1 y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat ->
   P (pos_Rl l i) (pos_Rl l' i))
H0:In r (cons r l)
H1:exists y : R, P r y
H2:forall x1 : R, In x1 l -> exists y : R, P x1 y
H3:exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat ->
   P (pos_Rl l i) (pos_Rl l' i))
x:R
H4:P r x
x0:Rlist
H5:Rlength l = Rlength x0
H6:forall i : nat,
(i < Rlength l)%nat ->
P (pos_Rl l i) (pos_Rl x0 i)
Rlength (cons r l) = Rlength (cons x x0)
r:R
l:Rlist
P:R -> R -> Prop
H:forall x1 : R,
In x1 (cons r l) -> exists y : R, P x1 y
Hrecl:(forall x1 : R,
 In x1 l -> exists y : R, P x1 y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat ->
   P (pos_Rl l i) (pos_Rl l' i))
H0:In r (cons r l)
H1:exists y : R, P r y
H2:forall x1 : R, In x1 l -> exists y : R, P x1 y
H3:exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat ->
   P (pos_Rl l i) (pos_Rl l' i))
x:R
H4:P r x
x0:Rlist
H5:Rlength l = Rlength x0
H6:forall i : nat,
(i < Rlength l)%nat ->
P (pos_Rl l i) (pos_Rl x0 i)
forall i : nat,
(i < Rlength (cons r l))%nat ->
P (pos_Rl (cons r l) i) (pos_Rl (cons x x0) i)
  simpl; rewrite H5; reflexivity.r:R
l:Rlist
P:R -> R -> Prop
H:forall x1 : R,
In x1 (cons r l) -> exists y : R, P x1 y
Hrecl:(forall x1 : R,
 In x1 l -> exists y : R, P x1 y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat ->
   P (pos_Rl l i) (pos_Rl l' i))
H0:In r (cons r l)
H1:exists y : R, P r y
H2:forall x1 : R, In x1 l -> exists y : R, P x1 y
H3:exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat ->
   P (pos_Rl l i) (pos_Rl l' i))
x:R
H4:P r x
x0:Rlist
H5:Rlength l = Rlength x0
H6:forall i : nat,
(i < Rlength l)%nat ->
P (pos_Rl l i) (pos_Rl x0 i)
forall i : nat,
(i < Rlength (cons r l))%nat ->
P (pos_Rl (cons r l) i) (pos_Rl (cons x x0) i)
  intros; destruct (zerop i) as [->|].r:R
l:Rlist
P:R -> R -> Prop
H:forall x1 : R,
In x1 (cons r l) -> exists y : R, P x1 y
Hrecl:(forall x1 : R,
 In x1 l -> exists y : R, P x1 y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat ->
   P (pos_Rl l i) (pos_Rl l' i))
H0:In r (cons r l)
H1:exists y : R, P r y
H2:forall x1 : R, In x1 l -> exists y : R, P x1 y
H3:exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i : nat,
   (i < Rlength l)%nat ->
   P (pos_Rl l i) (pos_Rl l' i))
x:R
H4:P r x
x0:Rlist
H5:Rlength l = Rlength x0
H6:forall i : nat,
(i < Rlength l)%nat ->
P (pos_Rl l i) (pos_Rl x0 i)
H7:(0 < Rlength (cons r l))%nat
P (pos_Rl (cons r l) 0) (pos_Rl (cons x x0) 0)
r:R
l:Rlist
P:R -> R -> Prop
H:forall x1 : R,
In x1 (cons r l) -> exists y : R, P x1 y
Hrecl:(forall x1 : R,
 In x1 l -> exists y : R, P x1 y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i0 : nat,
   (i0 < Rlength l)%nat ->
   P (pos_Rl l i0) (pos_Rl l' i0))
H0:In r (cons r l)
H1:exists y : R, P r y
H2:forall x1 : R, In x1 l -> exists y : R, P x1 y
H3:exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i0 : nat,
   (i0 < Rlength l)%nat ->
   P (pos_Rl l i0) (pos_Rl l' i0))
x:R
H4:P r x
x0:Rlist
H5:Rlength l = Rlength x0
H6:forall i0 : nat,
(i0 < Rlength l)%nat ->
P (pos_Rl l i0) (pos_Rl x0 i0)
i:nat
H7:(i < Rlength (cons r l))%nat
l0:(0 < i)%nat
P (pos_Rl (cons r l) i) (pos_Rl (cons x x0) i)
  simpl; assumption.r:R
l:Rlist
P:R -> R -> Prop
H:forall x1 : R,
In x1 (cons r l) -> exists y : R, P x1 y
Hrecl:(forall x1 : R,
 In x1 l -> exists y : R, P x1 y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i0 : nat,
   (i0 < Rlength l)%nat ->
   P (pos_Rl l i0) (pos_Rl l' i0))
H0:In r (cons r l)
H1:exists y : R, P r y
H2:forall x1 : R, In x1 l -> exists y : R, P x1 y
H3:exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i0 : nat,
   (i0 < Rlength l)%nat ->
   P (pos_Rl l i0) (pos_Rl l' i0))
x:R
H4:P r x
x0:Rlist
H5:Rlength l = Rlength x0
H6:forall i0 : nat,
(i0 < Rlength l)%nat ->
P (pos_Rl l i0) (pos_Rl x0 i0)
i:nat
H7:(i < Rlength (cons r l))%nat
l0:(0 < i)%nat
P (pos_Rl (cons r l) i) (pos_Rl (cons x x0) i)
  assert (H9 : i = S (pred i)).r:R
l:Rlist
P:R -> R -> Prop
H:forall x1 : R,
In x1 (cons r l) -> exists y : R, P x1 y
Hrecl:(forall x1 : R,
 In x1 l -> exists y : R, P x1 y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i0 : nat,
   (i0 < Rlength l)%nat ->
   P (pos_Rl l i0) (pos_Rl l' i0))
H0:In r (cons r l)
H1:exists y : R, P r y
H2:forall x1 : R, In x1 l -> exists y : R, P x1 y
H3:exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i0 : nat,
   (i0 < Rlength l)%nat ->
   P (pos_Rl l i0) (pos_Rl l' i0))
x:R
H4:P r x
x0:Rlist
H5:Rlength l = Rlength x0
H6:forall i0 : nat,
(i0 < Rlength l)%nat ->
P (pos_Rl l i0) (pos_Rl x0 i0)
i:nat
H7:(i < Rlength (cons r l))%nat
l0:(0 < i)%nat
i = S (Init.Nat.pred i)
r:R
l:Rlist
P:R -> R -> Prop
H:forall x1 : R,
In x1 (cons r l) -> exists y : R, P x1 y
Hrecl:(forall x1 : R,
 In x1 l -> exists y : R, P x1 y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i0 : nat,
   (i0 < Rlength l)%nat ->
   P (pos_Rl l i0) (pos_Rl l' i0))
H0:In r (cons r l)
H1:exists y : R, P r y
H2:forall x1 : R, In x1 l -> exists y : R, P x1 y
H3:exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i0 : nat,
   (i0 < Rlength l)%nat ->
   P (pos_Rl l i0) (pos_Rl l' i0))
x:R
H4:P r x
x0:Rlist
H5:Rlength l = Rlength x0
H6:forall i0 : nat,
(i0 < Rlength l)%nat ->
P (pos_Rl l i0) (pos_Rl x0 i0)
i:nat
H7:(i < Rlength (cons r l))%nat
l0:(0 < i)%nat
H9:i = S (Init.Nat.pred i)
P (pos_Rl (cons r l) i) (pos_Rl (cons x x0) i)
  apply S_pred with 0%nat; assumption.r:R
l:Rlist
P:R -> R -> Prop
H:forall x1 : R,
In x1 (cons r l) -> exists y : R, P x1 y
Hrecl:(forall x1 : R,
 In x1 l -> exists y : R, P x1 y) ->
exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i0 : nat,
   (i0 < Rlength l)%nat ->
   P (pos_Rl l i0) (pos_Rl l' i0))
H0:In r (cons r l)
H1:exists y : R, P r y
H2:forall x1 : R, In x1 l -> exists y : R, P x1 y
H3:exists l' : Rlist,
  Rlength l = Rlength l' /\
  (forall i0 : nat,
   (i0 < Rlength l)%nat ->
   P (pos_Rl l i0) (pos_Rl l' i0))
x:R
H4:P r x
x0:Rlist
H5:Rlength l = Rlength x0
H6:forall i0 : nat,
(i0 < Rlength l)%nat ->
P (pos_Rl l i0) (pos_Rl x0 i0)
i:nat
H7:(i < Rlength (cons r l))%nat
l0:(0 < i)%nat
H9:i = S (Init.Nat.pred i)
P (pos_Rl (cons r l) i) (pos_Rl (cons x x0) i)
  rewrite H9; simpl; apply H6; simpl in H7; apply lt_S_n; rewrite <- H9;
    assumption.
Qed.

Definition ordered_Rlist (l:Rlist) : Prop :=
  forall i:nat, (i < pred (Rlength l))%nat -> pos_Rl l i <= pos_Rl l (S i).

Fixpoint insert (l:Rlist) (x:R) : Rlist :=
  match l with
    | nil => cons x nil
    | cons a l' =>
      match Rle_dec a x with
        | left _ => cons a (insert l' x)
        | right _ => cons x l
      end
  end.

Fixpoint cons_Rlist (l k:Rlist) : Rlist :=
  match l with
    | nil => k
    | cons a l' => cons a (cons_Rlist l' k)
  end.

Fixpoint cons_ORlist (k l:Rlist) : Rlist :=
  match k with
    | nil => l
    | cons a k' => cons_ORlist k' (insert l a)
  end.

Fixpoint app_Rlist (l:Rlist) (f:R -> R) : Rlist :=
  match l with
    | nil => nil
    | cons a l' => cons (f a) (app_Rlist l' f)
  end.

Fixpoint mid_Rlist (l:Rlist) (x:R) : Rlist :=
  match l with
    | nil => nil
    | cons a l' => cons ((x + a) / 2) (mid_Rlist l' a)
  end.

Definition Rtail (l:Rlist) : Rlist :=
  match l with
    | nil => nil
    | cons a l' => l'
  end.

Definition FF (l:Rlist) (f:R -> R) : Rlist :=
  match l with
    | nil => nil
    | cons a l' => app_Rlist (mid_Rlist l' a) f
  end.

Lemma RList_P0 :
  forall (l:Rlist) (a:R),
    pos_Rl (insert l a) 0 = a \/ pos_Rl (insert l a) 0 = pos_Rl l 0.forall (l : Rlist) (a : R),
pos_Rl (insert l a) 0 = a \/
pos_Rl (insert l a) 0 = pos_Rl l 0
Proof.forall (l : Rlist) (a : R),
pos_Rl (insert l a) 0 = a \/
pos_Rl (insert l a) 0 = pos_Rl l 0
  intros; induction  l as [| r l Hrecl];
    [ left; reflexivity
      | simpl; case (Rle_dec r a); intro;
        [ right; reflexivity | left; reflexivity ] ].
Qed.

Lemma RList_P1 :
  forall (l:Rlist) (a:R), ordered_Rlist l -> ordered_Rlist (insert l a).forall (l : Rlist) (a : R),
ordered_Rlist l -> ordered_Rlist (insert l a)
Proof.forall (l : Rlist) (a : R),
ordered_Rlist l -> ordered_Rlist (insert l a)
  intros; induction  l as [| r l Hrecl].a:R
H:ordered_Rlist nil
ordered_Rlist (insert nil a)
r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
ordered_Rlist (insert (cons r l) a)
  simpl; unfold ordered_Rlist; intros; simpl in H0;
    elim (lt_n_O _ H0).r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
ordered_Rlist (insert (cons r l) a)
  simpl; case (Rle_dec r a); intro.r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
r0:r <= a
ordered_Rlist (cons r (insert l a))
r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
n:~ r <= a
ordered_Rlist (cons a (cons r l))
  assert (H1 : ordered_Rlist l).r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
r0:r <= a
ordered_Rlist l
r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
r0:r <= a
H1:ordered_Rlist l
ordered_Rlist (cons r (insert l a))
r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
n:~ r <= a
ordered_Rlist (cons a (cons r l))
  unfold ordered_Rlist; unfold ordered_Rlist in H; intros;
    assert (H1 : (S i < pred (Rlength (cons r l)))%nat);
      [ simpl; replace (Rlength l) with (S (pred (Rlength l)));
        [ apply lt_n_S; assumption
          | symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red;
            intro; rewrite <- H1 in H0; simpl in H0; elim (lt_n_O _ H0) ]
        | apply (H _ H1) ].r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
r0:r <= a
H1:ordered_Rlist l
ordered_Rlist (cons r (insert l a))
r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
n:~ r <= a
ordered_Rlist (cons a (cons r l))
  assert (H2 := Hrecl H1); unfold ordered_Rlist; intros;
    induction  i as [| i Hreci].r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
r0:r <= a
H1:ordered_Rlist l
H2:ordered_Rlist (insert l a)
H0:(0 <
 Init.Nat.pred (Rlength (cons r (insert l a))))%nat
pos_Rl (cons r (insert l a)) 0 <=
pos_Rl (cons r (insert l a)) 1
r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
r0:r <= a
H1:ordered_Rlist l
H2:ordered_Rlist (insert l a)
i:nat
H0:(S i <
 Init.Nat.pred (Rlength (cons r (insert l a))))%nat
Hreci:(i <
 Init.Nat.pred (Rlength (cons r (insert l a))))%nat ->
pos_Rl (cons r (insert l a)) i <=
pos_Rl (cons r (insert l a)) (S i)
pos_Rl (cons r (insert l a)) (S i) <=
pos_Rl (cons r (insert l a)) (S (S i))
r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
n:~ r <= a
ordered_Rlist (cons a (cons r l))
  simpl; assert (H3 := RList_P0 l a); elim H3; intro.r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
r0:r <= a
H1:ordered_Rlist l
H2:ordered_Rlist (insert l a)
H0:(0 <
 Init.Nat.pred (Rlength (cons r (insert l a))))%nat
H3:pos_Rl (insert l a) 0 = a \/
pos_Rl (insert l a) 0 = pos_Rl l 0
H4:pos_Rl (insert l a) 0 = a
r <= pos_Rl (insert l a) 0
r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
r0:r <= a
H1:ordered_Rlist l
H2:ordered_Rlist (insert l a)
H0:(0 <
 Init.Nat.pred (Rlength (cons r (insert l a))))%nat
H3:pos_Rl (insert l a) 0 = a \/
pos_Rl (insert l a) 0 = pos_Rl l 0
H4:pos_Rl (insert l a) 0 = pos_Rl l 0
r <= pos_Rl (insert l a) 0
r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
r0:r <= a
H1:ordered_Rlist l
H2:ordered_Rlist (insert l a)
i:nat
H0:(S i <
 Init.Nat.pred (Rlength (cons r (insert l a))))%nat
Hreci:(i <
 Init.Nat.pred (Rlength (cons r (insert l a))))%nat ->
pos_Rl (cons r (insert l a)) i <=
pos_Rl (cons r (insert l a)) (S i)
pos_Rl (cons r (insert l a)) (S i) <=
pos_Rl (cons r (insert l a)) (S (S i))
r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
n:~ r <= a
ordered_Rlist (cons a (cons r l))
  rewrite H4; assumption.r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
r0:r <= a
H1:ordered_Rlist l
H2:ordered_Rlist (insert l a)
H0:(0 <
 Init.Nat.pred (Rlength (cons r (insert l a))))%nat
H3:pos_Rl (insert l a) 0 = a \/
pos_Rl (insert l a) 0 = pos_Rl l 0
H4:pos_Rl (insert l a) 0 = pos_Rl l 0
r <= pos_Rl (insert l a) 0
r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
r0:r <= a
H1:ordered_Rlist l
H2:ordered_Rlist (insert l a)
i:nat
H0:(S i <
 Init.Nat.pred (Rlength (cons r (insert l a))))%nat
Hreci:(i <
 Init.Nat.pred (Rlength (cons r (insert l a))))%nat ->
pos_Rl (cons r (insert l a)) i <=
pos_Rl (cons r (insert l a)) (S i)
pos_Rl (cons r (insert l a)) (S i) <=
pos_Rl (cons r (insert l a)) (S (S i))
r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
n:~ r <= a
ordered_Rlist (cons a (cons r l))
  induction  l as [| r1 l Hrecl0];
    [ simpl; assumption
      | rewrite H4; apply (H 0%nat); simpl; apply lt_O_Sn ].r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
r0:r <= a
H1:ordered_Rlist l
H2:ordered_Rlist (insert l a)
i:nat
H0:(S i <
 Init.Nat.pred (Rlength (cons r (insert l a))))%nat
Hreci:(i <
 Init.Nat.pred (Rlength (cons r (insert l a))))%nat ->
pos_Rl (cons r (insert l a)) i <=
pos_Rl (cons r (insert l a)) (S i)
pos_Rl (cons r (insert l a)) (S i) <=
pos_Rl (cons r (insert l a)) (S (S i))
r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
n:~ r <= a
ordered_Rlist (cons a (cons r l))
  simpl; apply H2; simpl in H0; apply lt_S_n;
    replace (S (pred (Rlength (insert l a)))) with (Rlength (insert l a));
    [ assumption
      | apply S_pred with 0%nat; apply neq_O_lt; red; intro;
        rewrite <- H3 in H0; elim (lt_n_O _ H0) ].r:R
l:Rlist
a:R
H:ordered_Rlist (cons r l)
Hrecl:ordered_Rlist l -> ordered_Rlist (insert l a)
n:~ r <= a
ordered_Rlist (cons a (cons r l))
  unfold ordered_Rlist; intros; induction  i as [| i Hreci];
    [ simpl; auto with real
      | change (pos_Rl (cons r l) i <= pos_Rl (cons r l) (S i)); apply H;
        simpl in H0; simpl; apply (lt_S_n _ _ H0) ].
Qed.

Lemma RList_P2 :
  forall l1 l2:Rlist, ordered_Rlist l2 -> ordered_Rlist (cons_ORlist l1 l2).forall l1 l2 : Rlist,
ordered_Rlist l2 -> ordered_Rlist (cons_ORlist l1 l2)
Proof.forall l1 l2 : Rlist,
ordered_Rlist l2 -> ordered_Rlist (cons_ORlist l1 l2)
  simple induction l1;
    [ intros; simpl; apply H
      | intros; simpl; apply H; apply RList_P1; assumption ].
Qed.

Lemma RList_P3 :
  forall (l:Rlist) (x:R),
    In x l <-> (exists i : nat, x = pos_Rl l i /\ (i < Rlength l)%nat).forall (l : Rlist) (x : R),
In x l <->
(exists i : nat, x = pos_Rl l i /\ (i < Rlength l)%nat)
Proof.forall (l : Rlist) (x : R),
In x l <->
(exists i : nat, x = pos_Rl l i /\ (i < Rlength l)%nat)
  intros; split; intro;
    [ induction  l as [| r l Hrecl] | induction  l as [| r l Hrecl] ].x:R
H:In x nil
exists i : nat,
  x = pos_Rl nil i /\ (i < Rlength nil)%nat
r:R
l:Rlist
x:R
H:In x (cons r l)
Hrecl:In x l ->
exists i : nat,
  x = pos_Rl l i /\ (i < Rlength l)%nat
exists i : nat,
  x = pos_Rl (cons r l) i /\
  (i < Rlength (cons r l))%nat
x:R
H:exists i : nat,
  x = pos_Rl nil i /\ (i < Rlength nil)%nat
In x nil
r:R
l:Rlist
x:R
H:exists i : nat,
  x = pos_Rl (cons r l) i /\
  (i < Rlength (cons r l))%nat
Hrecl:(exists i : nat,
   x = pos_Rl l i /\ (i < Rlength l)%nat) ->
In x l
In x (cons r l)
  elim H.r:R
l:Rlist
x:R
H:In x (cons r l)
Hrecl:In x l ->
exists i : nat,
  x = pos_Rl l i /\ (i < Rlength l)%nat
exists i : nat,
  x = pos_Rl (cons r l) i /\
  (i < Rlength (cons r l))%nat
x:R
H:exists i : nat,
  x = pos_Rl nil i /\ (i < Rlength nil)%nat
In x nil
r:R
l:Rlist
x:R
H:exists i : nat,
  x = pos_Rl (cons r l) i /\
  (i < Rlength (cons r l))%nat
Hrecl:(exists i : nat,
   x = pos_Rl l i /\ (i < Rlength l)%nat) ->
In x l
In x (cons r l)
  elim H; intro;
    [ exists 0%nat; split; [ apply H0 | simpl; apply lt_O_Sn ]
      | elim (Hrecl H0); intros; elim H1; clear H1; intros; exists (S x0); split;
        [ apply H1 | simpl; apply lt_n_S; assumption ] ].x:R
H:exists i : nat,
  x = pos_Rl nil i /\ (i < Rlength nil)%nat
In x nil
r:R
l:Rlist
x:R
H:exists i : nat,
  x = pos_Rl (cons r l) i /\
  (i < Rlength (cons r l))%nat
Hrecl:(exists i : nat,
   x = pos_Rl l i /\ (i < Rlength l)%nat) ->
In x l
In x (cons r l)
  elim H; intros; elim H0; intros; elim (lt_n_O _ H2).r:R
l:Rlist
x:R
H:exists i : nat,
  x = pos_Rl (cons r l) i /\
  (i < Rlength (cons r l))%nat
Hrecl:(exists i : nat,
   x = pos_Rl l i /\ (i < Rlength l)%nat) ->
In x l
In x (cons r l)
  simpl; elim H; intros; elim H0; clear H0; intros;
    induction  x0 as [| x0 Hrecx0];
      [ left; apply H0
        | right; apply Hrecl; exists x0; split;
          [ apply H0 | simpl in H1; apply lt_S_n; assumption ] ].
Qed.

Lemma RList_P4 :
  forall (l1:Rlist) (a:R), ordered_Rlist (cons a l1) -> ordered_Rlist l1.forall (l1 : Rlist) (a : R),
ordered_Rlist (cons a l1) -> ordered_Rlist l1
Proof.forall (l1 : Rlist) (a : R),
ordered_Rlist (cons a l1) -> ordered_Rlist l1
  intros; unfold ordered_Rlist; intros; apply (H (S i)); simpl;
    replace (Rlength l1) with (S (pred (Rlength l1)));
    [ apply lt_n_S; assumption
      | symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red;
        intro; rewrite <- H1 in H0; elim (lt_n_O _ H0) ].
Qed.

Lemma RList_P5 :
  forall (l:Rlist) (x:R), ordered_Rlist l -> In x l -> pos_Rl l 0 <= x.forall (l : Rlist) (x : R),
ordered_Rlist l -> In x l -> pos_Rl l 0 <= x
Proof.forall (l : Rlist) (x : R),
ordered_Rlist l -> In x l -> pos_Rl l 0 <= x
  intros; induction  l as [| r l Hrecl];
    [ elim H0
      | simpl; elim H0; intro;
        [ rewrite H1; right; reflexivity
          | apply Rle_trans with (pos_Rl l 0);
            [ apply (H 0%nat); simpl; induction  l as [| r0 l Hrecl0];
              [ elim H1 | simpl; apply lt_O_Sn ]
              | apply Hrecl; [ eapply RList_P4; apply H | assumption ] ] ] ].
Qed.

Lemma RList_P6 :
  forall l:Rlist,
    ordered_Rlist l <->
    (forall i j:nat,
      (i <= j)%nat -> (j < Rlength l)%nat -> pos_Rl l i <= pos_Rl l j).forall l : Rlist,
ordered_Rlist l <->
(forall i j : nat,
 (i <= j)%nat ->
 (j < Rlength l)%nat -> pos_Rl l i <= pos_Rl l j)
Proof.forall l : Rlist,
ordered_Rlist l <->
(forall i j : nat,
 (i <= j)%nat ->
 (j < Rlength l)%nat -> pos_Rl l i <= pos_Rl l j)
  simple induction l; split; intro.l:Rlist
H:ordered_Rlist nil
forall i j : nat,
(i <= j)%nat ->
(j < Rlength nil)%nat -> pos_Rl nil i <= pos_Rl nil j
l:Rlist
H:forall i j : nat,
(i <= j)%nat ->
(j < Rlength nil)%nat ->
pos_Rl nil i <= pos_Rl nil j
ordered_Rlist nil
l:Rlist
r:R
r0:Rlist
H:ordered_Rlist r0 <->
(forall i j : nat,
 (i <= j)%nat ->
 (j < Rlength r0)%nat ->
 pos_Rl r0 i <= pos_Rl r0 j)
H0:ordered_Rlist (cons r r0)
forall i j : nat,
(i <= j)%nat ->
(j < Rlength (cons r r0))%nat ->
pos_Rl (cons r r0) i <= pos_Rl (cons r r0) j
l:Rlist
r:R
r0:Rlist
H:ordered_Rlist r0 <->
(forall i j : nat,
 (i <= j)%nat ->
 (j < Rlength r0)%nat ->
 pos_Rl r0 i <= pos_Rl r0 j)
H0:forall i j : nat,
(i <= j)%nat ->
(j < Rlength (cons r r0))%nat ->
pos_Rl (cons r r0) i <= pos_Rl (cons r r0) j
ordered_Rlist (cons r r0)
  intros; right; reflexivity.l:Rlist
H:forall i j : nat,
(i <= j)%nat ->
(j < Rlength nil)%nat ->
pos_Rl nil i <= pos_Rl nil j
ordered_Rlist nil
l:Rlist
r:R
r0:Rlist
H:ordered_Rlist r0 <->
(forall i j : nat,
 (i <= j)%nat ->
 (j < Rlength r0)%nat ->
 pos_Rl r0 i <= pos_Rl r0 j)
H0:ordered_Rlist (cons r r0)
forall i j : nat,
(i <= j)%nat ->
(j < Rlength (cons r r0))%nat ->
pos_Rl (cons r r0) i <= pos_Rl (cons r r0) j
l:Rlist
r:R
r0:Rlist
H:ordered_Rlist r0 <->
(forall i j : nat,
 (i <= j)%nat ->
 (j < Rlength r0)%nat ->
 pos_Rl r0 i <= pos_Rl r0 j)
H0:forall i j : nat,
(i <= j)%nat ->
(j < Rlength (cons r r0))%nat ->
pos_Rl (cons r r0) i <= pos_Rl (cons r r0) j
ordered_Rlist (cons r r0)
  unfold ordered_Rlist; intros; simpl in H0; elim (lt_n_O _ H0).l:Rlist
r:R
r0:Rlist
H:ordered_Rlist r0 <->
(forall i j : nat,
 (i <= j)%nat ->
 (j < Rlength r0)%nat ->
 pos_Rl r0 i <= pos_Rl r0 j)
H0:ordered_Rlist (cons r r0)
forall i j : nat,
(i <= j)%nat ->
(j < Rlength (cons r r0))%nat ->
pos_Rl (cons r r0) i <= pos_Rl (cons r r0) j
l:Rlist
r:R
r0:Rlist
H:ordered_Rlist r0 <->
(forall i j : nat,
 (i <= j)%nat ->
 (j < Rlength r0)%nat ->
 pos_Rl r0 i <= pos_Rl r0 j)
H0:forall i j : nat,
(i <= j)%nat ->
(j < Rlength (cons r r0))%nat ->
pos_Rl (cons r r0) i <= pos_Rl (cons r r0) j
ordered_Rlist (cons r r0)
  intros; induction  i as [| i Hreci];
    [ induction  j as [| j Hrecj];
      [ right; reflexivity
        | simpl; apply Rle_trans with (pos_Rl r0 0);
          [ apply (H0 0%nat); simpl; simpl in H2; apply neq_O_lt;
            red; intro; rewrite <- H3 in H2;
              assert (H4 := lt_S_n _ _ H2); elim (lt_n_O _ H4)
            | elim H; intros; apply H3;
              [ apply RList_P4 with r; assumption
                | apply le_O_n
                | simpl in H2; apply lt_S_n; assumption ] ] ]
      | induction  j as [| j Hrecj];
        [ elim (le_Sn_O _ H1)
          | simpl; elim H; intros; apply H3;
            [ apply RList_P4 with r; assumption
              | apply le_S_n; assumption
              | simpl in H2; apply lt_S_n; assumption ] ] ].l:Rlist
r:R
r0:Rlist
H:ordered_Rlist r0 <->
(forall i j : nat,
 (i <= j)%nat ->
 (j < Rlength r0)%nat ->
 pos_Rl r0 i <= pos_Rl r0 j)
H0:forall i j : nat,
(i <= j)%nat ->
(j < Rlength (cons r r0))%nat ->
pos_Rl (cons r r0) i <= pos_Rl (cons r r0) j
ordered_Rlist (cons r r0)
  unfold ordered_Rlist; intros; apply H0;
    [ apply le_n_Sn | simpl; simpl in H1; apply lt_n_S; assumption ].
Qed.

Lemma RList_P7 :
  forall (l:Rlist) (x:R),
    ordered_Rlist l -> In x l -> x <= pos_Rl l (pred (Rlength l)).forall (l : Rlist) (x : R),
ordered_Rlist l ->
In x l -> x <= pos_Rl l (Init.Nat.pred (Rlength l))
Proof.forall (l : Rlist) (x : R),
ordered_Rlist l ->
In x l -> x <= pos_Rl l (Init.Nat.pred (Rlength l))
  intros; assert (H1 := RList_P6 l); elim H1; intros H2 _; assert (H3 := H2 H);
    clear H1 H2; assert (H1 := RList_P3 l x); elim H1;
      clear H1; intros; assert (H4 := H1 H0); elim H4; clear H4;
        intros; elim H4; clear H4; intros; rewrite H4;
          assert (H6 : Rlength l = S (pred (Rlength l))).l:Rlist
x:R
H:ordered_Rlist l
H0:In x l
H3:forall i j : nat,
(i <= j)%nat ->
(j < Rlength l)%nat -> pos_Rl l i <= pos_Rl l j
H1:In x l ->
exists i : nat,
  x = pos_Rl l i /\ (i < Rlength l)%nat
H2:(exists i : nat,
   x = pos_Rl l i /\ (i < Rlength l)%nat) ->
In x l
x0:nat
H4:x = pos_Rl l x0
H5:(x0 < Rlength l)%nat
Rlength l = S (Init.Nat.pred (Rlength l))
l:Rlist
x:R
H:ordered_Rlist l
H0:In x l
H3:forall i j : nat,
(i <= j)%nat ->
(j < Rlength l)%nat -> pos_Rl l i <= pos_Rl l j
H1:In x l ->
exists i : nat,
  x = pos_Rl l i /\ (i < Rlength l)%nat
H2:(exists i : nat,
   x = pos_Rl l i /\ (i < Rlength l)%nat) ->
In x l
x0:nat
H4:x = pos_Rl l x0
H5:(x0 < Rlength l)%nat
H6:Rlength l = S (Init.Nat.pred (Rlength l))
pos_Rl l x0 <= pos_Rl l (Init.Nat.pred (Rlength l))
  apply S_pred with 0%nat; apply neq_O_lt; red; intro;
    rewrite <- H6 in H5; elim (lt_n_O _ H5).l:Rlist
x:R
H:ordered_Rlist l
H0:In x l
H3:forall i j : nat,
(i <= j)%nat ->
(j < Rlength l)%nat -> pos_Rl l i <= pos_Rl l j
H1:In x l ->
exists i : nat,
  x = pos_Rl l i /\ (i < Rlength l)%nat
H2:(exists i : nat,
   x = pos_Rl l i /\ (i < Rlength l)%nat) ->
In x l
x0:nat
H4:x = pos_Rl l x0
H5:(x0 < Rlength l)%nat
H6:Rlength l = S (Init.Nat.pred (Rlength l))
pos_Rl l x0 <= pos_Rl l (Init.Nat.pred (Rlength l))
  apply H3;
    [ rewrite H6 in H5; apply lt_n_Sm_le; assumption
      | apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H7 in H5;
        elim (lt_n_O _ H5) ].
Qed.

Lemma RList_P8 :
  forall (l:Rlist) (a x:R), In x (insert l a) <-> x = a \/ In x l.forall (l : Rlist) (a x : R),
In x (insert l a) <-> x = a \/ In x l
Proof.forall (l : Rlist) (a x : R),
In x (insert l a) <-> x = a \/ In x l
  simple induction l.l:Rlist
forall a x : R,
In x (insert nil a) <-> x = a \/ In x nil
l:Rlist
forall (r : R) (r0 : Rlist),
(forall a x : R,
 In x (insert r0 a) <-> x = a \/ In x r0) ->
forall a x : R,
In x (insert (cons r r0) a) <->
x = a \/ In x (cons r r0)
  intros; split; intro; simpl in H; apply H.l:Rlist
forall (r : R) (r0 : Rlist),
(forall a x : R,
 In x (insert r0 a) <-> x = a \/ In x r0) ->
forall a x : R,
In x (insert (cons r r0) a) <->
x = a \/ In x (cons r r0)
  intros; split; intro;
    [ simpl in H0; generalize H0; case (Rle_dec r a); intros;
      [ simpl in H1; elim H1; intro;
        [ right; left; assumption
          | elim (H a x); intros; elim (H3 H2); intro;
            [ left; assumption | right; right; assumption ] ]
        | simpl in H1; decompose [or] H1;
          [ left; assumption
            | right; left; assumption
            | right; right; assumption ] ]
      | simpl; case (Rle_dec r a); intro;
        [ simpl in H0; decompose [or] H0;
          [ right; elim (H a x); intros; apply H3; left
            | left
            | right; elim (H a x); intros; apply H3; right ]
          | simpl in H0; decompose [or] H0; [ left | right; left | right; right ] ];
        assumption ].
Qed.

Lemma RList_P9 :
  forall (l1 l2:Rlist) (x:R), In x (cons_ORlist l1 l2) <-> In x l1 \/ In x l2.forall (l1 l2 : Rlist) (x : R),
In x (cons_ORlist l1 l2) <-> In x l1 \/ In x l2
Proof.forall (l1 l2 : Rlist) (x : R),
In x (cons_ORlist l1 l2) <-> In x l1 \/ In x l2
  simple induction l1.l1:Rlist
forall (l2 : Rlist) (x : R),
In x (cons_ORlist nil l2) <-> In x nil \/ In x l2
l1:Rlist
forall (r : R) (r0 : Rlist),
(forall (l2 : Rlist) (x : R),
 In x (cons_ORlist r0 l2) <-> In x r0 \/ In x l2) ->
forall (l2 : Rlist) (x : R),
In x (cons_ORlist (cons r r0) l2) <->
In x (cons r r0) \/ In x l2
  intros; split; intro;
    [ simpl in H; right; assumption
      | simpl; elim H; intro; [ elim H0 | assumption ] ].l1:Rlist
forall (r : R) (r0 : Rlist),
(forall (l2 : Rlist) (x : R),
 In x (cons_ORlist r0 l2) <-> In x r0 \/ In x l2) ->
forall (l2 : Rlist) (x : R),
In x (cons_ORlist (cons r r0) l2) <->
In x (cons r r0) \/ In x l2
  intros; split.l1:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (x0 : R),
In x0 (cons_ORlist r0 l0) <-> In x0 r0 \/ In x0 l0
l2:Rlist
x:R
In x (cons_ORlist (cons r r0) l2) ->
In x (cons r r0) \/ In x l2
l1:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (x0 : R),
In x0 (cons_ORlist r0 l0) <-> In x0 r0 \/ In x0 l0
l2:Rlist
x:R
In x (cons r r0) \/ In x l2 ->
In x (cons_ORlist (cons r r0) l2)
  simpl; intros; elim (H (insert l2 r) x); intros; assert (H3 := H1 H0);
    elim H3; intro;
      [ left; right; assumption
        | elim (RList_P8 l2 r x); intros H5 _; assert (H6 := H5 H4); elim H6; intro;
          [ left; left; assumption | right; assumption ] ].l1:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (x0 : R),
In x0 (cons_ORlist r0 l0) <-> In x0 r0 \/ In x0 l0
l2:Rlist
x:R
In x (cons r r0) \/ In x l2 ->
In x (cons_ORlist (cons r r0) l2)
  intro; simpl; elim (H (insert l2 r) x); intros _ H1; apply H1;
    elim H0; intro;
      [ elim H2; intro;
        [ right; elim (RList_P8 l2 r x); intros _ H4; apply H4; left; assumption
          | left; assumption ]
        | right; elim (RList_P8 l2 r x); intros _ H3; apply H3; right; assumption ].
Qed.

Lemma RList_P10 :
  forall (l:Rlist) (a:R), Rlength (insert l a) = S (Rlength l).forall (l : Rlist) (a : R),
Rlength (insert l a) = S (Rlength l)
Proof.forall (l : Rlist) (a : R),
Rlength (insert l a) = S (Rlength l)
  intros; induction  l as [| r l Hrecl];
    [ reflexivity
      | simpl; case (Rle_dec r a); intro;
        [ simpl; rewrite Hrecl; reflexivity | reflexivity ] ].
Qed.

Lemma RList_P11 :
  forall l1 l2:Rlist,
    Rlength (cons_ORlist l1 l2) = (Rlength l1 + Rlength l2)%nat.forall l1 l2 : Rlist,
Rlength (cons_ORlist l1 l2) =
(Rlength l1 + Rlength l2)%nat
Proof.forall l1 l2 : Rlist,
Rlength (cons_ORlist l1 l2) =
(Rlength l1 + Rlength l2)%nat
  simple induction l1;
    [ intro; reflexivity
      | intros; simpl; rewrite (H (insert l2 r)); rewrite RList_P10;
        apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR;
          rewrite S_INR; ring ].
Qed.

Lemma RList_P12 :
  forall (l:Rlist) (i:nat) (f:R -> R),
    (i < Rlength l)%nat -> pos_Rl (app_Rlist l f) i = f (pos_Rl l i).forall (l : Rlist) (i : nat) (f : R -> R),
(i < Rlength l)%nat ->
pos_Rl (app_Rlist l f) i = f (pos_Rl l i)
Proof.forall (l : Rlist) (i : nat) (f : R -> R),
(i < Rlength l)%nat ->
pos_Rl (app_Rlist l f) i = f (pos_Rl l i)
  simple induction l;
    [ intros; elim (lt_n_O _ H)
      | intros; induction  i as [| i Hreci];
        [ reflexivity | simpl; apply H; apply lt_S_n; apply H0 ] ].
Qed.

Lemma RList_P13 :
  forall (l:Rlist) (i:nat) (a:R),
    (i < pred (Rlength l))%nat ->
    pos_Rl (mid_Rlist l a) (S i) = (pos_Rl l i + pos_Rl l (S i)) / 2.forall (l : Rlist) (i : nat) (a : R),
(i < Init.Nat.pred (Rlength l))%nat ->
pos_Rl (mid_Rlist l a) (S i) =
(pos_Rl l i + pos_Rl l (S i)) / 2
Proof.forall (l : Rlist) (i : nat) (a : R),
(i < Init.Nat.pred (Rlength l))%nat ->
pos_Rl (mid_Rlist l a) (S i) =
(pos_Rl l i + pos_Rl l (S i)) / 2
  simple induction l.l:Rlist
forall (i : nat) (a : R),
(i < Init.Nat.pred (Rlength nil))%nat ->
pos_Rl (mid_Rlist nil a) (S i) =
(pos_Rl nil i + pos_Rl nil (S i)) / 2
l:Rlist
forall (r : R) (r0 : Rlist),
(forall (i : nat) (a : R),
 (i < Init.Nat.pred (Rlength r0))%nat ->
 pos_Rl (mid_Rlist r0 a) (S i) =
 (pos_Rl r0 i + pos_Rl r0 (S i)) / 2) ->
forall (i : nat) (a : R),
(i < Init.Nat.pred (Rlength (cons r r0)))%nat ->
pos_Rl (mid_Rlist (cons r r0) a) (S i) =
(pos_Rl (cons r r0) i + pos_Rl (cons r r0) (S i)) / 2
  intros; simpl in H; elim (lt_n_O _ H).l:Rlist
forall (r : R) (r0 : Rlist),
(forall (i : nat) (a : R),
 (i < Init.Nat.pred (Rlength r0))%nat ->
 pos_Rl (mid_Rlist r0 a) (S i) =
 (pos_Rl r0 i + pos_Rl r0 (S i)) / 2) ->
forall (i : nat) (a : R),
(i < Init.Nat.pred (Rlength (cons r r0)))%nat ->
pos_Rl (mid_Rlist (cons r r0) a) (S i) =
(pos_Rl (cons r r0) i + pos_Rl (cons r r0) (S i)) / 2
  simple induction r0.l:Rlist
r:R
r0:Rlist
(forall (i : nat) (a : R),
 (i < Init.Nat.pred (Rlength nil))%nat ->
 pos_Rl (mid_Rlist nil a) (S i) =
 (pos_Rl nil i + pos_Rl nil (S i)) / 2) ->
forall (i : nat) (a : R),
(i < Init.Nat.pred (Rlength (cons r nil)))%nat ->
pos_Rl (mid_Rlist (cons r nil) a) (S i) =
(pos_Rl (cons r nil) i + pos_Rl (cons r nil) (S i)) /
2
l:Rlist
r:R
r0:Rlist
forall (r1 : R) (r2 : Rlist),
((forall (i : nat) (a : R),
  (i < Init.Nat.pred (Rlength r2))%nat ->
  pos_Rl (mid_Rlist r2 a) (S i) =
  (pos_Rl r2 i + pos_Rl r2 (S i)) / 2) ->
 forall (i : nat) (a : R),
 (i < Init.Nat.pred (Rlength (cons r r2)))%nat ->
 pos_Rl (mid_Rlist (cons r r2) a) (S i) =
 (pos_Rl (cons r r2) i + pos_Rl (cons r r2) (S i)) / 2) ->
(forall (i : nat) (a : R),
 (i < Init.Nat.pred (Rlength (cons r1 r2)))%nat ->
 pos_Rl (mid_Rlist (cons r1 r2) a) (S i) =
 (pos_Rl (cons r1 r2) i + pos_Rl (cons r1 r2) (S i)) /
 2) ->
forall (i : nat) (a : R),
(i < Init.Nat.pred (Rlength (cons r (cons r1 r2))))%nat ->
pos_Rl (mid_Rlist (cons r (cons r1 r2)) a) (S i) =
(pos_Rl (cons r (cons r1 r2)) i +
 pos_Rl (cons r (cons r1 r2)) (S i)) / 2
  intros; simpl in H0; elim (lt_n_O _ H0).l:Rlist
r:R
r0:Rlist
forall (r1 : R) (r2 : Rlist),
((forall (i : nat) (a : R),
  (i < Init.Nat.pred (Rlength r2))%nat ->
  pos_Rl (mid_Rlist r2 a) (S i) =
  (pos_Rl r2 i + pos_Rl r2 (S i)) / 2) ->
 forall (i : nat) (a : R),
 (i < Init.Nat.pred (Rlength (cons r r2)))%nat ->
 pos_Rl (mid_Rlist (cons r r2) a) (S i) =
 (pos_Rl (cons r r2) i + pos_Rl (cons r r2) (S i)) / 2) ->
(forall (i : nat) (a : R),
 (i < Init.Nat.pred (Rlength (cons r1 r2)))%nat ->
 pos_Rl (mid_Rlist (cons r1 r2) a) (S i) =
 (pos_Rl (cons r1 r2) i + pos_Rl (cons r1 r2) (S i)) /
 2) ->
forall (i : nat) (a : R),
(i < Init.Nat.pred (Rlength (cons r (cons r1 r2))))%nat ->
pos_Rl (mid_Rlist (cons r (cons r1 r2)) a) (S i) =
(pos_Rl (cons r (cons r1 r2)) i +
 pos_Rl (cons r (cons r1 r2)) (S i)) / 2
  intros; simpl in H1; induction  i as [| i Hreci].l:Rlist
r:R
r0:Rlist
r1:R
r2:Rlist
H:(forall (i : nat) (a0 : R),
 (i < Init.Nat.pred (Rlength r2))%nat ->
 pos_Rl (mid_Rlist r2 a0) (S i) =
 (pos_Rl r2 i + pos_Rl r2 (S i)) / 2) ->
forall (i : nat) (a0 : R),
(i < Init.Nat.pred (Rlength (cons r r2)))%nat ->
pos_Rl (mid_Rlist (cons r r2) a0) (S i) =
(pos_Rl (cons r r2) i + pos_Rl (cons r r2) (S i)) /
2
H0:forall (i : nat) (a0 : R),
(i < Init.Nat.pred (Rlength (cons r1 r2)))%nat ->
pos_Rl (mid_Rlist (cons r1 r2) a0) (S i) =
(pos_Rl (cons r1 r2) i +
 pos_Rl (cons r1 r2) (S i)) / 2
a:R
H1:(0 < S (Rlength r2))%nat
pos_Rl (mid_Rlist (cons r (cons r1 r2)) a) 1 =
(pos_Rl (cons r (cons r1 r2)) 0 +
 pos_Rl (cons r (cons r1 r2)) 1) / 2
l:Rlist
r:R
r0:Rlist
r1:R
r2:Rlist
H:(forall (i0 : nat) (a0 : R),
 (i0 < Init.Nat.pred (Rlength r2))%nat ->
 pos_Rl (mid_Rlist r2 a0) (S i0) =
 (pos_Rl r2 i0 + pos_Rl r2 (S i0)) / 2) ->
forall (i0 : nat) (a0 : R),
(i0 < Init.Nat.pred (Rlength (cons r r2)))%nat ->
pos_Rl (mid_Rlist (cons r r2) a0) (S i0) =
(pos_Rl (cons r r2) i0 + pos_Rl (cons r r2) (S i0)) /
2
H0:forall (i0 : nat) (a0 : R),
(i0 < Init.Nat.pred (Rlength (cons r1 r2)))%nat ->
pos_Rl (mid_Rlist (cons r1 r2) a0) (S i0) =
(pos_Rl (cons r1 r2) i0 +
 pos_Rl (cons r1 r2) (S i0)) / 2
i:nat
a:R
H1:(S i < S (Rlength r2))%nat
Hreci:(i < S (Rlength r2))%nat ->
pos_Rl (mid_Rlist (cons r (cons r1 r2)) a)
  (S i) =
(pos_Rl (cons r (cons r1 r2)) i +
 pos_Rl (cons r (cons r1 r2)) (S i)) / 2
pos_Rl (mid_Rlist (cons r (cons r1 r2)) a) (S (S i)) =
(pos_Rl (cons r (cons r1 r2)) (S i) +
 pos_Rl (cons r (cons r1 r2)) (S (S i))) / 2
  reflexivity.l:Rlist
r:R
r0:Rlist
r1:R
r2:Rlist
H:(forall (i0 : nat) (a0 : R),
 (i0 < Init.Nat.pred (Rlength r2))%nat ->
 pos_Rl (mid_Rlist r2 a0) (S i0) =
 (pos_Rl r2 i0 + pos_Rl r2 (S i0)) / 2) ->
forall (i0 : nat) (a0 : R),
(i0 < Init.Nat.pred (Rlength (cons r r2)))%nat ->
pos_Rl (mid_Rlist (cons r r2) a0) (S i0) =
(pos_Rl (cons r r2) i0 + pos_Rl (cons r r2) (S i0)) /
2
H0:forall (i0 : nat) (a0 : R),
(i0 < Init.Nat.pred (Rlength (cons r1 r2)))%nat ->
pos_Rl (mid_Rlist (cons r1 r2) a0) (S i0) =
(pos_Rl (cons r1 r2) i0 +
 pos_Rl (cons r1 r2) (S i0)) / 2
i:nat
a:R
H1:(S i < S (Rlength r2))%nat
Hreci:(i < S (Rlength r2))%nat ->
pos_Rl (mid_Rlist (cons r (cons r1 r2)) a)
  (S i) =
(pos_Rl (cons r (cons r1 r2)) i +
 pos_Rl (cons r (cons r1 r2)) (S i)) / 2
pos_Rl (mid_Rlist (cons r (cons r1 r2)) a) (S (S i)) =
(pos_Rl (cons r (cons r1 r2)) (S i) +
 pos_Rl (cons r (cons r1 r2)) (S (S i))) / 2
  change
    (pos_Rl (mid_Rlist (cons r1 r2) r) (S i) =
      (pos_Rl (cons r1 r2) i + pos_Rl (cons r1 r2) (S i)) / 2)
   ; apply H0; simpl; apply lt_S_n; assumption.
Qed.

Lemma RList_P14 : forall (l:Rlist) (a:R), Rlength (mid_Rlist l a) = Rlength l.forall (l : Rlist) (a : R),
Rlength (mid_Rlist l a) = Rlength l
Proof.forall (l : Rlist) (a : R),
Rlength (mid_Rlist l a) = Rlength l
  simple induction l; intros;
    [ reflexivity | simpl; rewrite (H r); reflexivity ].
Qed.

Lemma RList_P15 :
  forall l1 l2:Rlist,
    ordered_Rlist l1 ->
    ordered_Rlist l2 ->
    pos_Rl l1 0 = pos_Rl l2 0 -> pos_Rl (cons_ORlist l1 l2) 0 = pos_Rl l1 0.forall l1 l2 : Rlist,
ordered_Rlist l1 ->
ordered_Rlist l2 ->
pos_Rl l1 0 = pos_Rl l2 0 ->
pos_Rl (cons_ORlist l1 l2) 0 = pos_Rl l1 0
Proof.forall l1 l2 : Rlist,
ordered_Rlist l1 ->
ordered_Rlist l2 ->
pos_Rl l1 0 = pos_Rl l2 0 ->
pos_Rl (cons_ORlist l1 l2) 0 = pos_Rl l1 0
  intros; apply Rle_antisym.l1, l2:Rlist
H:ordered_Rlist l1
H0:ordered_Rlist l2
H1:pos_Rl l1 0 = pos_Rl l2 0
pos_Rl (cons_ORlist l1 l2) 0 <= pos_Rl l1 0
l1, l2:Rlist
H:ordered_Rlist l1
H0:ordered_Rlist l2
H1:pos_Rl l1 0 = pos_Rl l2 0
pos_Rl l1 0 <= pos_Rl (cons_ORlist l1 l2) 0
  induction  l1 as [| r l1 Hrecl1];
    [ simpl; simpl in H1; right; symmetry ; assumption
      | elim (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) 0)); intros;
        assert
          (H4 :
            In (pos_Rl (cons r l1) 0) (cons r l1) \/ In (pos_Rl (cons r l1) 0) l2);
          [ left; left; reflexivity
            | assert (H5 := H3 H4); apply RList_P5;
              [ apply RList_P2; assumption | assumption ] ] ].l1, l2:Rlist
H:ordered_Rlist l1
H0:ordered_Rlist l2
H1:pos_Rl l1 0 = pos_Rl l2 0
pos_Rl l1 0 <= pos_Rl (cons_ORlist l1 l2) 0
  induction  l1 as [| r l1 Hrecl1];
    [ simpl; simpl in H1; right; assumption
      | assert
        (H2 :
          In (pos_Rl (cons_ORlist (cons r l1) l2) 0) (cons_ORlist (cons r l1) l2));
        [ elim
          (RList_P3 (cons_ORlist (cons r l1) l2)
            (pos_Rl (cons_ORlist (cons r l1) l2) 0));
          intros; apply H3; exists 0%nat; split;
            [ reflexivity | rewrite RList_P11; simpl; apply lt_O_Sn ]
          | elim (RList_P9 (cons r l1) l2 (pos_Rl (cons_ORlist (cons r l1) l2) 0));
            intros; assert (H5 := H3 H2); elim H5; intro;
              [ apply RList_P5; assumption
                | rewrite H1; apply RList_P5; assumption ] ] ].
Qed.

Lemma RList_P16 :
  forall l1 l2:Rlist,
    ordered_Rlist l1 ->
    ordered_Rlist l2 ->
    pos_Rl l1 (pred (Rlength l1)) = pos_Rl l2 (pred (Rlength l2)) ->
    pos_Rl (cons_ORlist l1 l2) (pred (Rlength (cons_ORlist l1 l2))) =
    pos_Rl l1 (pred (Rlength l1)).forall l1 l2 : Rlist,
ordered_Rlist l1 ->
ordered_Rlist l2 ->
pos_Rl l1 (Init.Nat.pred (Rlength l1)) =
pos_Rl l2 (Init.Nat.pred (Rlength l2)) ->
pos_Rl (cons_ORlist l1 l2)
  (Init.Nat.pred (Rlength (cons_ORlist l1 l2))) =
pos_Rl l1 (Init.Nat.pred (Rlength l1))
Proof.forall l1 l2 : Rlist,
ordered_Rlist l1 ->
ordered_Rlist l2 ->
pos_Rl l1 (Init.Nat.pred (Rlength l1)) =
pos_Rl l2 (Init.Nat.pred (Rlength l2)) ->
pos_Rl (cons_ORlist l1 l2)
  (Init.Nat.pred (Rlength (cons_ORlist l1 l2))) =
pos_Rl l1 (Init.Nat.pred (Rlength l1))
  intros; apply Rle_antisym.l1, l2:Rlist
H:ordered_Rlist l1
H0:ordered_Rlist l2
H1:pos_Rl l1 (Init.Nat.pred (Rlength l1)) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
pos_Rl (cons_ORlist l1 l2)
  (Init.Nat.pred (Rlength (cons_ORlist l1 l2))) <=
pos_Rl l1 (Init.Nat.pred (Rlength l1))
l1, l2:Rlist
H:ordered_Rlist l1
H0:ordered_Rlist l2
H1:pos_Rl l1 (Init.Nat.pred (Rlength l1)) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
pos_Rl l1 (Init.Nat.pred (Rlength l1)) <=
pos_Rl (cons_ORlist l1 l2)
  (Init.Nat.pred (Rlength (cons_ORlist l1 l2)))
  induction  l1 as [| r l1 Hrecl1].l2:Rlist
H:ordered_Rlist nil
H0:ordered_Rlist l2
H1:pos_Rl nil (Init.Nat.pred (Rlength nil)) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
pos_Rl (cons_ORlist nil l2)
  (Init.Nat.pred (Rlength (cons_ORlist nil l2))) <=
pos_Rl nil (Init.Nat.pred (Rlength nil))
r:R
l1, l2:Rlist
H:ordered_Rlist (cons r l1)
H0:ordered_Rlist l2
H1:pos_Rl (cons r l1)
  (Init.Nat.pred (Rlength (cons r l1))) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
Hrecl1:ordered_Rlist l1 ->
pos_Rl l1 (Init.Nat.pred (Rlength l1)) =
pos_Rl l2 (Init.Nat.pred (Rlength l2)) ->
pos_Rl (cons_ORlist l1 l2)
  (Init.Nat.pred
     (Rlength (cons_ORlist l1 l2))) <=
pos_Rl l1 (Init.Nat.pred (Rlength l1))
pos_Rl (cons_ORlist (cons r l1) l2)
  (Init.Nat.pred
     (Rlength (cons_ORlist (cons r l1) l2))) <=
pos_Rl (cons r l1)
  (Init.Nat.pred (Rlength (cons r l1)))
l1, l2:Rlist
H:ordered_Rlist l1
H0:ordered_Rlist l2
H1:pos_Rl l1 (Init.Nat.pred (Rlength l1)) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
pos_Rl l1 (Init.Nat.pred (Rlength l1)) <=
pos_Rl (cons_ORlist l1 l2)
  (Init.Nat.pred (Rlength (cons_ORlist l1 l2)))
  simpl; simpl in H1; right; symmetry ; assumption.r:R
l1, l2:Rlist
H:ordered_Rlist (cons r l1)
H0:ordered_Rlist l2
H1:pos_Rl (cons r l1)
  (Init.Nat.pred (Rlength (cons r l1))) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
Hrecl1:ordered_Rlist l1 ->
pos_Rl l1 (Init.Nat.pred (Rlength l1)) =
pos_Rl l2 (Init.Nat.pred (Rlength l2)) ->
pos_Rl (cons_ORlist l1 l2)
  (Init.Nat.pred
     (Rlength (cons_ORlist l1 l2))) <=
pos_Rl l1 (Init.Nat.pred (Rlength l1))
pos_Rl (cons_ORlist (cons r l1) l2)
  (Init.Nat.pred
     (Rlength (cons_ORlist (cons r l1) l2))) <=
pos_Rl (cons r l1)
  (Init.Nat.pred (Rlength (cons r l1)))
l1, l2:Rlist
H:ordered_Rlist l1
H0:ordered_Rlist l2
H1:pos_Rl l1 (Init.Nat.pred (Rlength l1)) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
pos_Rl l1 (Init.Nat.pred (Rlength l1)) <=
pos_Rl (cons_ORlist l1 l2)
  (Init.Nat.pred (Rlength (cons_ORlist l1 l2)))
  assert
    (H2 :
      In
      (pos_Rl (cons_ORlist (cons r l1) l2)
        (pred (Rlength (cons_ORlist (cons r l1) l2))))
      (cons_ORlist (cons r l1) l2));
    [ elim
      (RList_P3 (cons_ORlist (cons r l1) l2)
        (pos_Rl (cons_ORlist (cons r l1) l2)
          (pred (Rlength (cons_ORlist (cons r l1) l2)))));
      intros; apply H3; exists (pred (Rlength (cons_ORlist (cons r l1) l2)));
        split; [ reflexivity | rewrite RList_P11; simpl; apply lt_n_Sn ]
      | elim
        (RList_P9 (cons r l1) l2
          (pos_Rl (cons_ORlist (cons r l1) l2)
            (pred (Rlength (cons_ORlist (cons r l1) l2)))));
        intros; assert (H5 := H3 H2); elim H5; intro;
          [ apply RList_P7; assumption | rewrite H1; apply RList_P7; assumption ] ].l1, l2:Rlist
H:ordered_Rlist l1
H0:ordered_Rlist l2
H1:pos_Rl l1 (Init.Nat.pred (Rlength l1)) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
pos_Rl l1 (Init.Nat.pred (Rlength l1)) <=
pos_Rl (cons_ORlist l1 l2)
  (Init.Nat.pred (Rlength (cons_ORlist l1 l2)))
  induction  l1 as [| r l1 Hrecl1].l2:Rlist
H:ordered_Rlist nil
H0:ordered_Rlist l2
H1:pos_Rl nil (Init.Nat.pred (Rlength nil)) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
pos_Rl nil (Init.Nat.pred (Rlength nil)) <=
pos_Rl (cons_ORlist nil l2)
  (Init.Nat.pred (Rlength (cons_ORlist nil l2)))
r:R
l1, l2:Rlist
H:ordered_Rlist (cons r l1)
H0:ordered_Rlist l2
H1:pos_Rl (cons r l1)
  (Init.Nat.pred (Rlength (cons r l1))) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
Hrecl1:ordered_Rlist l1 ->
pos_Rl l1 (Init.Nat.pred (Rlength l1)) =
pos_Rl l2 (Init.Nat.pred (Rlength l2)) ->
pos_Rl l1 (Init.Nat.pred (Rlength l1)) <=
pos_Rl (cons_ORlist l1 l2)
  (Init.Nat.pred
     (Rlength (cons_ORlist l1 l2)))
pos_Rl (cons r l1)
  (Init.Nat.pred (Rlength (cons r l1))) <=
pos_Rl (cons_ORlist (cons r l1) l2)
  (Init.Nat.pred
     (Rlength (cons_ORlist (cons r l1) l2)))
  simpl; simpl in H1; right; assumption.r:R
l1, l2:Rlist
H:ordered_Rlist (cons r l1)
H0:ordered_Rlist l2
H1:pos_Rl (cons r l1)
  (Init.Nat.pred (Rlength (cons r l1))) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
Hrecl1:ordered_Rlist l1 ->
pos_Rl l1 (Init.Nat.pred (Rlength l1)) =
pos_Rl l2 (Init.Nat.pred (Rlength l2)) ->
pos_Rl l1 (Init.Nat.pred (Rlength l1)) <=
pos_Rl (cons_ORlist l1 l2)
  (Init.Nat.pred
     (Rlength (cons_ORlist l1 l2)))
pos_Rl (cons r l1)
  (Init.Nat.pred (Rlength (cons r l1))) <=
pos_Rl (cons_ORlist (cons r l1) l2)
  (Init.Nat.pred
     (Rlength (cons_ORlist (cons r l1) l2)))
  elim
    (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))));
    intros;
      assert
        (H4 :
          In (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))) (cons r l1) \/
          In (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))) l2);
        [ left; change (In (pos_Rl (cons r l1) (Rlength l1)) (cons r l1));
          elim (RList_P3 (cons r l1) (pos_Rl (cons r l1) (Rlength l1)));
            intros; apply H5; exists (Rlength l1); split;
              [ reflexivity | simpl; apply lt_n_Sn ]
          | assert (H5 := H3 H4); apply RList_P7;
            [ apply RList_P2; assumption
              | elim
                (RList_P9 (cons r l1) l2
                  (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))));
                intros; apply H7; left;
                  elim
                    (RList_P3 (cons r l1)
                      (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))));
                    intros; apply H9; exists (pred (Rlength (cons r l1)));
                      split; [ reflexivity | simpl; apply lt_n_Sn ] ] ].
Qed.

Lemma RList_P17 :
  forall (l1:Rlist) (x:R) (i:nat),
    ordered_Rlist l1 ->
    In x l1 ->
    pos_Rl l1 i < x -> (i < pred (Rlength l1))%nat -> pos_Rl l1 (S i) <= x.forall (l1 : Rlist) (x : R) (i : nat),
ordered_Rlist l1 ->
In x l1 ->
pos_Rl l1 i < x ->
(i < Init.Nat.pred (Rlength l1))%nat ->
pos_Rl l1 (S i) <= x
Proof.forall (l1 : Rlist) (x : R) (i : nat),
ordered_Rlist l1 ->
In x l1 ->
pos_Rl l1 i < x ->
(i < Init.Nat.pred (Rlength l1))%nat ->
pos_Rl l1 (S i) <= x
  simple induction l1.l1:Rlist
forall (x : R) (i : nat),
ordered_Rlist nil ->
In x nil ->
pos_Rl nil i < x ->
(i < Init.Nat.pred (Rlength nil))%nat ->
pos_Rl nil (S i) <= x
l1:Rlist
forall (r : R) (r0 : Rlist),
(forall (x : R) (i : nat),
 ordered_Rlist r0 ->
 In x r0 ->
 pos_Rl r0 i < x ->
 (i < Init.Nat.pred (Rlength r0))%nat ->
 pos_Rl r0 (S i) <= x) ->
forall (x : R) (i : nat),
ordered_Rlist (cons r r0) ->
In x (cons r r0) ->
pos_Rl (cons r r0) i < x ->
(i < Init.Nat.pred (Rlength (cons r r0)))%nat ->
pos_Rl (cons r r0) (S i) <= x
  intros; elim H0.l1:Rlist
forall (r : R) (r0 : Rlist),
(forall (x : R) (i : nat),
 ordered_Rlist r0 ->
 In x r0 ->
 pos_Rl r0 i < x ->
 (i < Init.Nat.pred (Rlength r0))%nat ->
 pos_Rl r0 (S i) <= x) ->
forall (x : R) (i : nat),
ordered_Rlist (cons r r0) ->
In x (cons r r0) ->
pos_Rl (cons r r0) i < x ->
(i < Init.Nat.pred (Rlength (cons r r0)))%nat ->
pos_Rl (cons r r0) (S i) <= x
  intros; induction  i as [| i Hreci].l1:Rlist
r:R
r0:Rlist
H:forall (x0 : R) (i : nat),
ordered_Rlist r0 ->
In x0 r0 ->
pos_Rl r0 i < x0 ->
(i < Init.Nat.pred (Rlength r0))%nat ->
pos_Rl r0 (S i) <= x0
x:R
H0:ordered_Rlist (cons r r0)
H1:In x (cons r r0)
H2:pos_Rl (cons r r0) 0 < x
H3:(0 < Init.Nat.pred (Rlength (cons r r0)))%nat
pos_Rl (cons r r0) 1 <= x
l1:Rlist
r:R
r0:Rlist
H:forall (x0 : R) (i0 : nat),
ordered_Rlist r0 ->
In x0 r0 ->
pos_Rl r0 i0 < x0 ->
(i0 < Init.Nat.pred (Rlength r0))%nat ->
pos_Rl r0 (S i0) <= x0
x:R
i:nat
H0:ordered_Rlist (cons r r0)
H1:In x (cons r r0)
H2:pos_Rl (cons r r0) (S i) < x
H3:(S i < Init.Nat.pred (Rlength (cons r r0)))%nat
Hreci:pos_Rl (cons r r0) i < x ->
(i < Init.Nat.pred (Rlength (cons r r0)))%nat ->
pos_Rl (cons r r0) (S i) <= x
pos_Rl (cons r r0) (S (S i)) <= x
  simpl; elim H1; intro;
    [ simpl in H2; rewrite H4 in H2; elim (Rlt_irrefl _ H2)
      | apply RList_P5; [ apply RList_P4 with r; assumption | assumption ] ].l1:Rlist
r:R
r0:Rlist
H:forall (x0 : R) (i0 : nat),
ordered_Rlist r0 ->
In x0 r0 ->
pos_Rl r0 i0 < x0 ->
(i0 < Init.Nat.pred (Rlength r0))%nat ->
pos_Rl r0 (S i0) <= x0
x:R
i:nat
H0:ordered_Rlist (cons r r0)
H1:In x (cons r r0)
H2:pos_Rl (cons r r0) (S i) < x
H3:(S i < Init.Nat.pred (Rlength (cons r r0)))%nat
Hreci:pos_Rl (cons r r0) i < x ->
(i < Init.Nat.pred (Rlength (cons r r0)))%nat ->
pos_Rl (cons r r0) (S i) <= x
pos_Rl (cons r r0) (S (S i)) <= x
  simpl; simpl in H2; elim H1; intro.l1:Rlist
r:R
r0:Rlist
H:forall (x0 : R) (i0 : nat),
ordered_Rlist r0 ->
In x0 r0 ->
pos_Rl r0 i0 < x0 ->
(i0 < Init.Nat.pred (Rlength r0))%nat ->
pos_Rl r0 (S i0) <= x0
x:R
i:nat
H0:ordered_Rlist (cons r r0)
H1:In x (cons r r0)
H2:pos_Rl r0 i < x
H3:(S i < Init.Nat.pred (Rlength (cons r r0)))%nat
Hreci:pos_Rl (cons r r0) i < x ->
(i < Init.Nat.pred (Rlength (cons r r0)))%nat ->
pos_Rl (cons r r0) (S i) <= x
H4:x = r
pos_Rl r0 (S i) <= x
l1:Rlist
r:R
r0:Rlist
H:forall (x0 : R) (i0 : nat),
ordered_Rlist r0 ->
In x0 r0 ->
pos_Rl r0 i0 < x0 ->
(i0 < Init.Nat.pred (Rlength r0))%nat ->
pos_Rl r0 (S i0) <= x0
x:R
i:nat
H0:ordered_Rlist (cons r r0)
H1:In x (cons r r0)
H2:pos_Rl r0 i < x
H3:(S i < Init.Nat.pred (Rlength (cons r r0)))%nat
Hreci:pos_Rl (cons r r0) i < x ->
(i < Init.Nat.pred (Rlength (cons r r0)))%nat ->
pos_Rl (cons r r0) (S i) <= x
H4:In x r0
pos_Rl r0 (S i) <= x
  rewrite H4 in H2; assert (H5 : r <= pos_Rl r0 i);
    [ apply Rle_trans with (pos_Rl r0 0);
      [ apply (H0 0%nat); simpl; simpl in H3; apply neq_O_lt;
        red; intro; rewrite <- H5 in H3; elim (lt_n_O _ H3)
        | elim (RList_P6 r0); intros; apply H5;
          [ apply RList_P4 with r; assumption
            | apply le_O_n
            | simpl in H3; apply lt_S_n; apply lt_trans with (Rlength r0);
              [ apply H3 | apply lt_n_Sn ] ] ]
      | elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H5 H2)) ].l1:Rlist
r:R
r0:Rlist
H:forall (x0 : R) (i0 : nat),
ordered_Rlist r0 ->
In x0 r0 ->
pos_Rl r0 i0 < x0 ->
(i0 < Init.Nat.pred (Rlength r0))%nat ->
pos_Rl r0 (S i0) <= x0
x:R
i:nat
H0:ordered_Rlist (cons r r0)
H1:In x (cons r r0)
H2:pos_Rl r0 i < x
H3:(S i < Init.Nat.pred (Rlength (cons r r0)))%nat
Hreci:pos_Rl (cons r r0) i < x ->
(i < Init.Nat.pred (Rlength (cons r r0)))%nat ->
pos_Rl (cons r r0) (S i) <= x
H4:In x r0
pos_Rl r0 (S i) <= x
  apply H; try assumption;
    [ apply RList_P4 with r; assumption
      | simpl in H3; apply lt_S_n;
        replace (S (pred (Rlength r0))) with (Rlength r0);
        [ apply H3
          | apply S_pred with 0%nat; apply neq_O_lt; red; intro;
            rewrite <- H5 in H3; elim (lt_n_O _ H3) ] ].
Qed.

Lemma RList_P18 :
  forall (l:Rlist) (f:R -> R), Rlength (app_Rlist l f) = Rlength l.forall (l : Rlist) (f : R -> R),
Rlength (app_Rlist l f) = Rlength l
Proof.forall (l : Rlist) (f : R -> R),
Rlength (app_Rlist l f) = Rlength l
  simple induction l; intros;
    [ reflexivity | simpl; rewrite H; reflexivity ].
Qed.

Lemma RList_P19 :
  forall l:Rlist,
    l <> nil ->  exists r : R, (exists r0 : Rlist, l = cons r r0).forall l : Rlist,
l <> nil -> exists (r : R) (r0 : Rlist), l = cons r r0
Proof.forall l : Rlist,
l <> nil -> exists (r : R) (r0 : Rlist), l = cons r r0
  intros; induction  l as [| r l Hrecl];
    [ elim H; reflexivity | exists r; exists l; reflexivity ].
Qed.

Lemma RList_P20 :
  forall l:Rlist,
    (2 <= Rlength l)%nat ->
    exists r : R,
      (exists r1 : R, (exists l' : Rlist, l = cons r (cons r1 l'))).forall l : Rlist,
(2 <= Rlength l)%nat ->
exists (r r1 : R) (l' : Rlist),
  l = cons r (cons r1 l')
Proof.forall l : Rlist,
(2 <= Rlength l)%nat ->
exists (r r1 : R) (l' : Rlist),
  l = cons r (cons r1 l')
  intros; induction  l as [| r l Hrecl];
    [ simpl in H; elim (le_Sn_O _ H)
      | induction  l as [| r0 l Hrecl0];
        [ simpl in H; elim (le_Sn_O _ (le_S_n _ _ H))
          | exists r; exists r0; exists l; reflexivity ] ].
Qed.

Lemma RList_P21 : forall l l':Rlist, l = l' -> Rtail l = Rtail l'.forall l l' : Rlist, l = l' -> Rtail l = Rtail l'
Proof.forall l l' : Rlist, l = l' -> Rtail l = Rtail l'
  intros; rewrite H; reflexivity.
Qed.

Lemma RList_P22 :
  forall l1 l2:Rlist, l1 <> nil -> pos_Rl (cons_Rlist l1 l2) 0 = pos_Rl l1 0.forall l1 l2 : Rlist,
l1 <> nil -> pos_Rl (cons_Rlist l1 l2) 0 = pos_Rl l1 0
Proof.forall l1 l2 : Rlist,
l1 <> nil -> pos_Rl (cons_Rlist l1 l2) 0 = pos_Rl l1 0
  simple induction l1; [ intros; elim H; reflexivity | intros; reflexivity ].
Qed.

Lemma RList_P23 :
  forall l1 l2:Rlist,
    Rlength (cons_Rlist l1 l2) = (Rlength l1 + Rlength l2)%nat.forall l1 l2 : Rlist,
Rlength (cons_Rlist l1 l2) =
(Rlength l1 + Rlength l2)%nat
Proof.forall l1 l2 : Rlist,
Rlength (cons_Rlist l1 l2) =
(Rlength l1 + Rlength l2)%nat
  simple induction l1;
    [ intro; reflexivity | intros; simpl; rewrite H; reflexivity ].
Qed.

Lemma RList_P24 :
  forall l1 l2:Rlist,
    l2 <> nil ->
    pos_Rl (cons_Rlist l1 l2) (pred (Rlength (cons_Rlist l1 l2))) =
    pos_Rl l2 (pred (Rlength l2)).forall l1 l2 : Rlist,
l2 <> nil ->
pos_Rl (cons_Rlist l1 l2)
  (Init.Nat.pred (Rlength (cons_Rlist l1 l2))) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
Proof.forall l1 l2 : Rlist,
l2 <> nil ->
pos_Rl (cons_Rlist l1 l2)
  (Init.Nat.pred (Rlength (cons_Rlist l1 l2))) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
  simple induction l1.l1:Rlist
forall l2 : Rlist,
l2 <> nil ->
pos_Rl (cons_Rlist nil l2)
  (Init.Nat.pred (Rlength (cons_Rlist nil l2))) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
l1:Rlist
forall (r : R) (r0 : Rlist),
(forall l2 : Rlist,
 l2 <> nil ->
 pos_Rl (cons_Rlist r0 l2)
   (Init.Nat.pred (Rlength (cons_Rlist r0 l2))) =
 pos_Rl l2 (Init.Nat.pred (Rlength l2))) ->
forall l2 : Rlist,
l2 <> nil ->
pos_Rl (cons_Rlist (cons r r0) l2)
  (Init.Nat.pred (Rlength (cons_Rlist (cons r r0) l2))) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
  intros; reflexivity.l1:Rlist
forall (r : R) (r0 : Rlist),
(forall l2 : Rlist,
 l2 <> nil ->
 pos_Rl (cons_Rlist r0 l2)
   (Init.Nat.pred (Rlength (cons_Rlist r0 l2))) =
 pos_Rl l2 (Init.Nat.pred (Rlength l2))) ->
forall l2 : Rlist,
l2 <> nil ->
pos_Rl (cons_Rlist (cons r r0) l2)
  (Init.Nat.pred (Rlength (cons_Rlist (cons r r0) l2))) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
  intros; rewrite <- (H l2 H0); induction  l2 as [| r1 l2 Hrecl2].l1:Rlist
r:R
r0:Rlist
H:forall l2 : Rlist,
l2 <> nil ->
pos_Rl (cons_Rlist r0 l2)
  (Init.Nat.pred (Rlength (cons_Rlist r0 l2))) =
pos_Rl l2 (Init.Nat.pred (Rlength l2))
H0:nil <> nil
pos_Rl (cons_Rlist (cons r r0) nil)
  (Init.Nat.pred
     (Rlength (cons_Rlist (cons r r0) nil))) =
pos_Rl (cons_Rlist r0 nil)
  (Init.Nat.pred (Rlength (cons_Rlist r0 nil)))
l1:Rlist
r:R
r0:Rlist
H:forall l0 : Rlist,
l0 <> nil ->
pos_Rl (cons_Rlist r0 l0)
  (Init.Nat.pred (Rlength (cons_Rlist r0 l0))) =
pos_Rl l0 (Init.Nat.pred (Rlength l0))
r1:R
l2:Rlist
H0:cons r1 l2 <> nil
Hrecl2:l2 <> nil ->
pos_Rl (cons_Rlist (cons r r0) l2)
  (Init.Nat.pred
     (Rlength (cons_Rlist (cons r r0) l2))) =
pos_Rl (cons_Rlist r0 l2)
  (Init.Nat.pred (Rlength (cons_Rlist r0 l2)))
pos_Rl (cons_Rlist (cons r r0) (cons r1 l2))
  (Init.Nat.pred
     (Rlength (cons_Rlist (cons r r0) (cons r1 l2)))) =
pos_Rl (cons_Rlist r0 (cons r1 l2))
  (Init.Nat.pred
     (Rlength (cons_Rlist r0 (cons r1 l2))))
  elim H0; reflexivity.l1:Rlist
r:R
r0:Rlist
H:forall l0 : Rlist,
l0 <> nil ->
pos_Rl (cons_Rlist r0 l0)
  (Init.Nat.pred (Rlength (cons_Rlist r0 l0))) =
pos_Rl l0 (Init.Nat.pred (Rlength l0))
r1:R
l2:Rlist
H0:cons r1 l2 <> nil
Hrecl2:l2 <> nil ->
pos_Rl (cons_Rlist (cons r r0) l2)
  (Init.Nat.pred
     (Rlength (cons_Rlist (cons r r0) l2))) =
pos_Rl (cons_Rlist r0 l2)
  (Init.Nat.pred (Rlength (cons_Rlist r0 l2)))
pos_Rl (cons_Rlist (cons r r0) (cons r1 l2))
  (Init.Nat.pred
     (Rlength (cons_Rlist (cons r r0) (cons r1 l2)))) =
pos_Rl (cons_Rlist r0 (cons r1 l2))
  (Init.Nat.pred
     (Rlength (cons_Rlist r0 (cons r1 l2))))
  do 2 rewrite RList_P23;
    replace (Rlength (cons r r0) + Rlength (cons r1 l2))%nat with
    (S (S (Rlength r0 + Rlength l2)));
    [ replace (Rlength r0 + Rlength (cons r1 l2))%nat with
      (S (Rlength r0 + Rlength l2));
      [ reflexivity
        | simpl; apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR;
          rewrite S_INR; ring ]
      | simpl; apply INR_eq; do 3 rewrite S_INR; do 2 rewrite plus_INR;
        rewrite S_INR; ring ].
Qed.

Lemma RList_P25 :
  forall l1 l2:Rlist,
    ordered_Rlist l1 ->
    ordered_Rlist l2 ->
    pos_Rl l1 (pred (Rlength l1)) <= pos_Rl l2 0 ->
    ordered_Rlist (cons_Rlist l1 l2).forall l1 l2 : Rlist,
ordered_Rlist l1 ->
ordered_Rlist l2 ->
pos_Rl l1 (Init.Nat.pred (Rlength l1)) <= pos_Rl l2 0 ->
ordered_Rlist (cons_Rlist l1 l2)
Proof.forall l1 l2 : Rlist,
ordered_Rlist l1 ->
ordered_Rlist l2 ->
pos_Rl l1 (Init.Nat.pred (Rlength l1)) <= pos_Rl l2 0 ->
ordered_Rlist (cons_Rlist l1 l2)
  simple induction l1.l1:Rlist
forall l2 : Rlist,
ordered_Rlist nil ->
ordered_Rlist l2 ->
pos_Rl nil (Init.Nat.pred (Rlength nil)) <=
pos_Rl l2 0 -> ordered_Rlist (cons_Rlist nil l2)
l1:Rlist
forall (r : R) (r0 : Rlist),
(forall l2 : Rlist,
 ordered_Rlist r0 ->
 ordered_Rlist l2 ->
 pos_Rl r0 (Init.Nat.pred (Rlength r0)) <= pos_Rl l2 0 ->
 ordered_Rlist (cons_Rlist r0 l2)) ->
forall l2 : Rlist,
ordered_Rlist (cons r r0) ->
ordered_Rlist l2 ->
pos_Rl (cons r r0)
  (Init.Nat.pred (Rlength (cons r r0))) <= pos_Rl l2 0 ->
ordered_Rlist (cons_Rlist (cons r r0) l2)
  intros; simpl; assumption.l1:Rlist
forall (r : R) (r0 : Rlist),
(forall l2 : Rlist,
 ordered_Rlist r0 ->
 ordered_Rlist l2 ->
 pos_Rl r0 (Init.Nat.pred (Rlength r0)) <= pos_Rl l2 0 ->
 ordered_Rlist (cons_Rlist r0 l2)) ->
forall l2 : Rlist,
ordered_Rlist (cons r r0) ->
ordered_Rlist l2 ->
pos_Rl (cons r r0)
  (Init.Nat.pred (Rlength (cons r r0))) <= pos_Rl l2 0 ->
ordered_Rlist (cons_Rlist (cons r r0) l2)
  simple induction r0.l1:Rlist
r:R
r0:Rlist
(forall l2 : Rlist,
 ordered_Rlist nil ->
 ordered_Rlist l2 ->
 pos_Rl nil (Init.Nat.pred (Rlength nil)) <=
 pos_Rl l2 0 -> ordered_Rlist (cons_Rlist nil l2)) ->
forall l2 : Rlist,
ordered_Rlist (cons r nil) ->
ordered_Rlist l2 ->
pos_Rl (cons r nil)
  (Init.Nat.pred (Rlength (cons r nil))) <=
pos_Rl l2 0 ->
ordered_Rlist (cons_Rlist (cons r nil) l2)
l1:Rlist
r:R
r0:Rlist
forall (r1 : R) (r2 : Rlist),
((forall l2 : Rlist,
  ordered_Rlist r2 ->
  ordered_Rlist l2 ->
  pos_Rl r2 (Init.Nat.pred (Rlength r2)) <=
  pos_Rl l2 0 -> ordered_Rlist (cons_Rlist r2 l2)) ->
 forall l2 : Rlist,
 ordered_Rlist (cons r r2) ->
 ordered_Rlist l2 ->
 pos_Rl (cons r r2)
   (Init.Nat.pred (Rlength (cons r r2))) <=
 pos_Rl l2 0 ->
 ordered_Rlist (cons_Rlist (cons r r2) l2)) ->
(forall l2 : Rlist,
 ordered_Rlist (cons r1 r2) ->
 ordered_Rlist l2 ->
 pos_Rl (cons r1 r2)
   (Init.Nat.pred (Rlength (cons r1 r2))) <=
 pos_Rl l2 0 ->
 ordered_Rlist (cons_Rlist (cons r1 r2) l2)) ->
forall l2 : Rlist,
ordered_Rlist (cons r (cons r1 r2)) ->
ordered_Rlist l2 ->
pos_Rl (cons r (cons r1 r2))
  (Init.Nat.pred (Rlength (cons r (cons r1 r2)))) <=
pos_Rl l2 0 ->
ordered_Rlist (cons_Rlist (cons r (cons r1 r2)) l2)
  intros; simpl; simpl in H2; unfold ordered_Rlist; intros;
    simpl in H3.l1:Rlist
r:R
r0:Rlist
H:forall l0 : Rlist,
ordered_Rlist nil ->
ordered_Rlist l0 ->
pos_Rl nil (Init.Nat.pred (Rlength nil)) <=
pos_Rl l0 0 -> ordered_Rlist (cons_Rlist nil l0)
l2:Rlist
H0:ordered_Rlist (cons r nil)
H1:ordered_Rlist l2
H2:r <= pos_Rl l2 0
i:nat
H3:(i < Rlength l2)%nat
pos_Rl (cons r l2) i <= pos_Rl (cons r l2) (S i)
l1:Rlist
r:R
r0:Rlist
forall (r1 : R) (r2 : Rlist),
((forall l2 : Rlist,
  ordered_Rlist r2 ->
  ordered_Rlist l2 ->
  pos_Rl r2 (Init.Nat.pred (Rlength r2)) <=
  pos_Rl l2 0 -> ordered_Rlist (cons_Rlist r2 l2)) ->
 forall l2 : Rlist,
 ordered_Rlist (cons r r2) ->
 ordered_Rlist l2 ->
 pos_Rl (cons r r2)
   (Init.Nat.pred (Rlength (cons r r2))) <=
 pos_Rl l2 0 ->
 ordered_Rlist (cons_Rlist (cons r r2) l2)) ->
(forall l2 : Rlist,
 ordered_Rlist (cons r1 r2) ->
 ordered_Rlist l2 ->
 pos_Rl (cons r1 r2)
   (Init.Nat.pred (Rlength (cons r1 r2))) <=
 pos_Rl l2 0 ->
 ordered_Rlist (cons_Rlist (cons r1 r2) l2)) ->
forall l2 : Rlist,
ordered_Rlist (cons r (cons r1 r2)) ->
ordered_Rlist l2 ->
pos_Rl (cons r (cons r1 r2))
  (Init.Nat.pred (Rlength (cons r (cons r1 r2)))) <=
pos_Rl l2 0 ->
ordered_Rlist (cons_Rlist (cons r (cons r1 r2)) l2)
  induction  i as [| i Hreci].l1:Rlist
r:R
r0:Rlist
H:forall l0 : Rlist,
ordered_Rlist nil ->
ordered_Rlist l0 ->
pos_Rl nil (Init.Nat.pred (Rlength nil)) <=
pos_Rl l0 0 -> ordered_Rlist (cons_Rlist nil l0)
l2:Rlist
H0:ordered_Rlist (cons r nil)
H1:ordered_Rlist l2
H2:r <= pos_Rl l2 0
H3:(0 < Rlength l2)%nat
pos_Rl (cons r l2) 0 <= pos_Rl (cons r l2) 1
l1:Rlist
r:R
r0:Rlist
H:forall l0 : Rlist,
ordered_Rlist nil ->
ordered_Rlist l0 ->
pos_Rl nil (Init.Nat.pred (Rlength nil)) <=
pos_Rl l0 0 -> ordered_Rlist (cons_Rlist nil l0)
l2:Rlist
H0:ordered_Rlist (cons r nil)
H1:ordered_Rlist l2
H2:r <= pos_Rl l2 0
i:nat
H3:(S i < Rlength l2)%nat
Hreci:(i < Rlength l2)%nat ->
pos_Rl (cons r l2) i <=
pos_Rl (cons r l2) (S i)
pos_Rl (cons r l2) (S i) <=
pos_Rl (cons r l2) (S (S i))
l1:Rlist
r:R
r0:Rlist
forall (r1 : R) (r2 : Rlist),
((forall l2 : Rlist,
  ordered_Rlist r2 ->
  ordered_Rlist l2 ->
  pos_Rl r2 (Init.Nat.pred (Rlength r2)) <=
  pos_Rl l2 0 -> ordered_Rlist (cons_Rlist r2 l2)) ->
 forall l2 : Rlist,
 ordered_Rlist (cons r r2) ->
 ordered_Rlist l2 ->
 pos_Rl (cons r r2)
   (Init.Nat.pred (Rlength (cons r r2))) <=
 pos_Rl l2 0 ->
 ordered_Rlist (cons_Rlist (cons r r2) l2)) ->
(forall l2 : Rlist,
 ordered_Rlist (cons r1 r2) ->
 ordered_Rlist l2 ->
 pos_Rl (cons r1 r2)
   (Init.Nat.pred (Rlength (cons r1 r2))) <=
 pos_Rl l2 0 ->
 ordered_Rlist (cons_Rlist (cons r1 r2) l2)) ->
forall l2 : Rlist,
ordered_Rlist (cons r (cons r1 r2)) ->
ordered_Rlist l2 ->
pos_Rl (cons r (cons r1 r2))
  (Init.Nat.pred (Rlength (cons r (cons r1 r2)))) <=
pos_Rl l2 0 ->
ordered_Rlist (cons_Rlist (cons r (cons r1 r2)) l2)
  simpl; assumption.l1:Rlist
r:R
r0:Rlist
H:forall l0 : Rlist,
ordered_Rlist nil ->
ordered_Rlist l0 ->
pos_Rl nil (Init.Nat.pred (Rlength nil)) <=
pos_Rl l0 0 -> ordered_Rlist (cons_Rlist nil l0)
l2:Rlist
H0:ordered_Rlist (cons r nil)
H1:ordered_Rlist l2
H2:r <= pos_Rl l2 0
i:nat
H3:(S i < Rlength l2)%nat
Hreci:(i < Rlength l2)%nat ->
pos_Rl (cons r l2) i <=
pos_Rl (cons r l2) (S i)
pos_Rl (cons r l2) (S i) <=
pos_Rl (cons r l2) (S (S i))
l1:Rlist
r:R
r0:Rlist
forall (r1 : R) (r2 : Rlist),
((forall l2 : Rlist,
  ordered_Rlist r2 ->
  ordered_Rlist l2 ->
  pos_Rl r2 (Init.Nat.pred (Rlength r2)) <=
  pos_Rl l2 0 -> ordered_Rlist (cons_Rlist r2 l2)) ->
 forall l2 : Rlist,
 ordered_Rlist (cons r r2) ->
 ordered_Rlist l2 ->
 pos_Rl (cons r r2)
   (Init.Nat.pred (Rlength (cons r r2))) <=
 pos_Rl l2 0 ->
 ordered_Rlist (cons_Rlist (cons r r2) l2)) ->
(forall l2 : Rlist,
 ordered_Rlist (cons r1 r2) ->
 ordered_Rlist l2 ->
 pos_Rl (cons r1 r2)
   (Init.Nat.pred (Rlength (cons r1 r2))) <=
 pos_Rl l2 0 ->
 ordered_Rlist (cons_Rlist (cons r1 r2) l2)) ->
forall l2 : Rlist,
ordered_Rlist (cons r (cons r1 r2)) ->
ordered_Rlist l2 ->
pos_Rl (cons r (cons r1 r2))
  (Init.Nat.pred (Rlength (cons r (cons r1 r2)))) <=
pos_Rl l2 0 ->
ordered_Rlist (cons_Rlist (cons r (cons r1 r2)) l2)
  change (pos_Rl l2 i <= pos_Rl l2 (S i)); apply (H1 i); apply lt_S_n;
    replace (S (pred (Rlength l2))) with (Rlength l2);
    [ assumption
      | apply S_pred with 0%nat; apply neq_O_lt; red; intro;
        rewrite <- H4 in H3; elim (lt_n_O _ H3) ].l1:Rlist
r:R
r0:Rlist
forall (r1 : R) (r2 : Rlist),
((forall l2 : Rlist,
  ordered_Rlist r2 ->
  ordered_Rlist l2 ->
  pos_Rl r2 (Init.Nat.pred (Rlength r2)) <=
  pos_Rl l2 0 -> ordered_Rlist (cons_Rlist r2 l2)) ->
 forall l2 : Rlist,
 ordered_Rlist (cons r r2) ->
 ordered_Rlist l2 ->
 pos_Rl (cons r r2)
   (Init.Nat.pred (Rlength (cons r r2))) <=
 pos_Rl l2 0 ->
 ordered_Rlist (cons_Rlist (cons r r2) l2)) ->
(forall l2 : Rlist,
 ordered_Rlist (cons r1 r2) ->
 ordered_Rlist l2 ->
 pos_Rl (cons r1 r2)
   (Init.Nat.pred (Rlength (cons r1 r2))) <=
 pos_Rl l2 0 ->
 ordered_Rlist (cons_Rlist (cons r1 r2) l2)) ->
forall l2 : Rlist,
ordered_Rlist (cons r (cons r1 r2)) ->
ordered_Rlist l2 ->
pos_Rl (cons r (cons r1 r2))
  (Init.Nat.pred (Rlength (cons r (cons r1 r2)))) <=
pos_Rl l2 0 ->
ordered_Rlist (cons_Rlist (cons r (cons r1 r2)) l2)
  intros; clear H; assert (H : ordered_Rlist (cons_Rlist (cons r1 r2) l2)).l1:Rlist
r:R
r0:Rlist
r1:R
r2:Rlist
H0:forall l0 : Rlist,
ordered_Rlist (cons r1 r2) ->
ordered_Rlist l0 ->
pos_Rl (cons r1 r2)
  (Init.Nat.pred (Rlength (cons r1 r2))) <=
pos_Rl l0 0 ->
ordered_Rlist (cons_Rlist (cons r1 r2) l0)
l2:Rlist
H1:ordered_Rlist (cons r (cons r1 r2))
H2:ordered_Rlist l2
H3:pos_Rl (cons r (cons r1 r2))
  (Init.Nat.pred (Rlength (cons r (cons r1 r2)))) <=
pos_Rl l2 0
ordered_Rlist (cons_Rlist (cons r1 r2) l2)
l1:Rlist
r:R
r0:Rlist
r1:R
r2:Rlist
H0:forall l0 : Rlist,
ordered_Rlist (cons r1 r2) ->
ordered_Rlist l0 ->
pos_Rl (cons r1 r2)
  (Init.Nat.pred (Rlength (cons r1 r2))) <=
pos_Rl l0 0 ->
ordered_Rlist (cons_Rlist (cons r1 r2) l0)
l2:Rlist
H1:ordered_Rlist (cons r (cons r1 r2))
H2:ordered_Rlist l2
H3:pos_Rl (cons r (cons r1 r2))
  (Init.Nat.pred (Rlength (cons r (cons r1 r2)))) <=
pos_Rl l2 0
H:ordered_Rlist (cons_Rlist (cons r1 r2) l2)
ordered_Rlist (cons_Rlist (cons r (cons r1 r2)) l2)
  apply H0; try assumption.l1:Rlist
r:R
r0:Rlist
r1:R
r2:Rlist
H0:forall l0 : Rlist,
ordered_Rlist (cons r1 r2) ->
ordered_Rlist l0 ->
pos_Rl (cons r1 r2)
  (Init.Nat.pred (Rlength (cons r1 r2))) <=
pos_Rl l0 0 ->
ordered_Rlist (cons_Rlist (cons r1 r2) l0)
l2:Rlist
H1:ordered_Rlist (cons r (cons r1 r2))
H2:ordered_Rlist l2
H3:pos_Rl (cons r (cons r1 r2))
  (Init.Nat.pred (Rlength (cons r (cons r1 r2)))) <=
pos_Rl l2 0
ordered_Rlist (cons r1 r2)
l1:Rlist
r:R
r0:Rlist
r1:R
r2:Rlist
H0:forall l0 : Rlist,
ordered_Rlist (cons r1 r2) ->
ordered_Rlist l0 ->
pos_Rl (cons r1 r2)
  (Init.Nat.pred (Rlength (cons r1 r2))) <=
pos_Rl l0 0 ->
ordered_Rlist (cons_Rlist (cons r1 r2) l0)
l2:Rlist
H1:ordered_Rlist (cons r (cons r1 r2))
H2:ordered_Rlist l2
H3:pos_Rl (cons r (cons r1 r2))
  (Init.Nat.pred (Rlength (cons r (cons r1 r2)))) <=
pos_Rl l2 0
H:ordered_Rlist (cons_Rlist (cons r1 r2) l2)
ordered_Rlist (cons_Rlist (cons r (cons r1 r2)) l2)
  apply RList_P4 with r; assumption.l1:Rlist
r:R
r0:Rlist
r1:R
r2:Rlist
H0:forall l0 : Rlist,
ordered_Rlist (cons r1 r2) ->
ordered_Rlist l0 ->
pos_Rl (cons r1 r2)
  (Init.Nat.pred (Rlength (cons r1 r2))) <=
pos_Rl l0 0 ->
ordered_Rlist (cons_Rlist (cons r1 r2) l0)
l2:Rlist
H1:ordered_Rlist (cons r (cons r1 r2))
H2:ordered_Rlist l2
H3:pos_Rl (cons r (cons r1 r2))
  (Init.Nat.pred (Rlength (cons r (cons r1 r2)))) <=
pos_Rl l2 0
H:ordered_Rlist (cons_Rlist (cons r1 r2) l2)
ordered_Rlist (cons_Rlist (cons r (cons r1 r2)) l2)
  unfold ordered_Rlist; intros; simpl in H4;
    induction  i as [| i Hreci].l1:Rlist
r:R
r0:Rlist
r1:R
r2:Rlist
H0:forall l0 : Rlist,
ordered_Rlist (cons r1 r2) ->
ordered_Rlist l0 ->
pos_Rl (cons r1 r2)
  (Init.Nat.pred (Rlength (cons r1 r2))) <=
pos_Rl l0 0 ->
ordered_Rlist (cons_Rlist (cons r1 r2) l0)
l2:Rlist
H1:ordered_Rlist (cons r (cons r1 r2))
H2:ordered_Rlist l2
H3:pos_Rl (cons r (cons r1 r2))
  (Init.Nat.pred (Rlength (cons r (cons r1 r2)))) <=
pos_Rl l2 0
H:ordered_Rlist (cons_Rlist (cons r1 r2) l2)
H4:(0 < S (Rlength (cons_Rlist r2 l2)))%nat
pos_Rl (cons_Rlist (cons r (cons r1 r2)) l2) 0 <=
pos_Rl (cons_Rlist (cons r (cons r1 r2)) l2) 1
l1:Rlist
r:R
r0:Rlist
r1:R
r2:Rlist
H0:forall l0 : Rlist,
ordered_Rlist (cons r1 r2) ->
ordered_Rlist l0 ->
pos_Rl (cons r1 r2)
  (Init.Nat.pred (Rlength (cons r1 r2))) <=
pos_Rl l0 0 ->
ordered_Rlist (cons_Rlist (cons r1 r2) l0)
l2:Rlist
H1:ordered_Rlist (cons r (cons r1 r2))
H2:ordered_Rlist l2
H3:pos_Rl (cons r (cons r1 r2))
  (Init.Nat.pred (Rlength (cons r (cons r1 r2)))) <=
pos_Rl l2 0
H:ordered_Rlist (cons_Rlist (cons r1 r2) l2)
i:nat
H4:(S i < S (Rlength (cons_Rlist r2 l2)))%nat
Hreci:(i < S (Rlength (cons_Rlist r2 l2)))%nat ->
pos_Rl (cons_Rlist (cons r (cons r1 r2)) l2) i <=
pos_Rl (cons_Rlist (cons r (cons r1 r2)) l2)
  (S i)
pos_Rl (cons_Rlist (cons r (cons r1 r2)) l2) (S i) <=
pos_Rl (cons_Rlist (cons r (cons r1 r2)) l2) (S (S i))
  simpl; apply (H1 0%nat); simpl; apply lt_O_Sn.l1:Rlist
r:R
r0:Rlist
r1:R
r2:Rlist
H0:forall l0 : Rlist,
ordered_Rlist (cons r1 r2) ->
ordered_Rlist l0 ->
pos_Rl (cons r1 r2)
  (Init.Nat.pred (Rlength (cons r1 r2))) <=
pos_Rl l0 0 ->
ordered_Rlist (cons_Rlist (cons r1 r2) l0)
l2:Rlist
H1:ordered_Rlist (cons r (cons r1 r2))
H2:ordered_Rlist l2
H3:pos_Rl (cons r (cons r1 r2))
  (Init.Nat.pred (Rlength (cons r (cons r1 r2)))) <=
pos_Rl l2 0
H:ordered_Rlist (cons_Rlist (cons r1 r2) l2)
i:nat
H4:(S i < S (Rlength (cons_Rlist r2 l2)))%nat
Hreci:(i < S (Rlength (cons_Rlist r2 l2)))%nat ->
pos_Rl (cons_Rlist (cons r (cons r1 r2)) l2) i <=
pos_Rl (cons_Rlist (cons r (cons r1 r2)) l2)
  (S i)
pos_Rl (cons_Rlist (cons r (cons r1 r2)) l2) (S i) <=
pos_Rl (cons_Rlist (cons r (cons r1 r2)) l2) (S (S i))
  change
    (pos_Rl (cons_Rlist (cons r1 r2) l2) i <=
      pos_Rl (cons_Rlist (cons r1 r2) l2) (S i));
    apply (H i); simpl; apply lt_S_n; assumption.
Qed.

Lemma RList_P26 :
  forall (l1 l2:Rlist) (i:nat),
    (i < Rlength l1)%nat -> pos_Rl (cons_Rlist l1 l2) i = pos_Rl l1 i.forall (l1 l2 : Rlist) (i : nat),
(i < Rlength l1)%nat ->
pos_Rl (cons_Rlist l1 l2) i = pos_Rl l1 i
Proof.forall (l1 l2 : Rlist) (i : nat),
(i < Rlength l1)%nat ->
pos_Rl (cons_Rlist l1 l2) i = pos_Rl l1 i
  simple induction l1.l1:Rlist
forall (l2 : Rlist) (i : nat),
(i < Rlength nil)%nat ->
pos_Rl (cons_Rlist nil l2) i = pos_Rl nil i
l1:Rlist
forall (r : R) (r0 : Rlist),
(forall (l2 : Rlist) (i : nat),
 (i < Rlength r0)%nat ->
 pos_Rl (cons_Rlist r0 l2) i = pos_Rl r0 i) ->
forall (l2 : Rlist) (i : nat),
(i < Rlength (cons r r0))%nat ->
pos_Rl (cons_Rlist (cons r r0) l2) i =
pos_Rl (cons r r0) i
  intros; elim (lt_n_O _ H).l1:Rlist
forall (r : R) (r0 : Rlist),
(forall (l2 : Rlist) (i : nat),
 (i < Rlength r0)%nat ->
 pos_Rl (cons_Rlist r0 l2) i = pos_Rl r0 i) ->
forall (l2 : Rlist) (i : nat),
(i < Rlength (cons r r0))%nat ->
pos_Rl (cons_Rlist (cons r r0) l2) i =
pos_Rl (cons r r0) i
  intros; induction  i as [| i Hreci].l1:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i : nat),
(i < Rlength r0)%nat ->
pos_Rl (cons_Rlist r0 l0) i = pos_Rl r0 i
l2:Rlist
H0:(0 < Rlength (cons r r0))%nat
pos_Rl (cons_Rlist (cons r r0) l2) 0 =
pos_Rl (cons r r0) 0
l1:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(i0 < Rlength r0)%nat ->
pos_Rl (cons_Rlist r0 l0) i0 = pos_Rl r0 i0
l2:Rlist
i:nat
H0:(S i < Rlength (cons r r0))%nat
Hreci:(i < Rlength (cons r r0))%nat ->
pos_Rl (cons_Rlist (cons r r0) l2) i =
pos_Rl (cons r r0) i
pos_Rl (cons_Rlist (cons r r0) l2) (S i) =
pos_Rl (cons r r0) (S i)
  apply RList_P22; discriminate.l1:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(i0 < Rlength r0)%nat ->
pos_Rl (cons_Rlist r0 l0) i0 = pos_Rl r0 i0
l2:Rlist
i:nat
H0:(S i < Rlength (cons r r0))%nat
Hreci:(i < Rlength (cons r r0))%nat ->
pos_Rl (cons_Rlist (cons r r0) l2) i =
pos_Rl (cons r r0) i
pos_Rl (cons_Rlist (cons r r0) l2) (S i) =
pos_Rl (cons r r0) (S i)
  apply (H l2 i); simpl in H0; apply lt_S_n; assumption.
Qed.

Lemma RList_P27 :
  forall l1 l2 l3:Rlist,
    cons_Rlist l1 (cons_Rlist l2 l3) = cons_Rlist (cons_Rlist l1 l2) l3.forall l1 l2 l3 : Rlist,
cons_Rlist l1 (cons_Rlist l2 l3) =
cons_Rlist (cons_Rlist l1 l2) l3
Proof.forall l1 l2 l3 : Rlist,
cons_Rlist l1 (cons_Rlist l2 l3) =
cons_Rlist (cons_Rlist l1 l2) l3
  simple induction l1; intros;
    [ reflexivity | simpl; rewrite (H l2 l3); reflexivity ].
Qed.

Lemma RList_P28 : forall l:Rlist, cons_Rlist l nil = l.forall l : Rlist, cons_Rlist l nil = l
Proof.forall l : Rlist, cons_Rlist l nil = l
  simple induction l;
    [ reflexivity | intros; simpl; rewrite H; reflexivity ].
Qed.

Lemma RList_P29 :
  forall (l2 l1:Rlist) (i:nat),
    (Rlength l1 <= i)%nat ->
    (i < Rlength (cons_Rlist l1 l2))%nat ->
    pos_Rl (cons_Rlist l1 l2) i = pos_Rl l2 (i - Rlength l1).forall (l2 l1 : Rlist) (i : nat),
(Rlength l1 <= i)%nat ->
(i < Rlength (cons_Rlist l1 l2))%nat ->
pos_Rl (cons_Rlist l1 l2) i =
pos_Rl l2 (i - Rlength l1)
Proof.forall (l2 l1 : Rlist) (i : nat),
(Rlength l1 <= i)%nat ->
(i < Rlength (cons_Rlist l1 l2))%nat ->
pos_Rl (cons_Rlist l1 l2) i =
pos_Rl l2 (i - Rlength l1)
  simple induction l2.l2:Rlist
forall (l1 : Rlist) (i : nat),
(Rlength l1 <= i)%nat ->
(i < Rlength (cons_Rlist l1 nil))%nat ->
pos_Rl (cons_Rlist l1 nil) i =
pos_Rl nil (i - Rlength l1)
l2:Rlist
forall (r : R) (r0 : Rlist),
(forall (l1 : Rlist) (i : nat),
 (Rlength l1 <= i)%nat ->
 (i < Rlength (cons_Rlist l1 r0))%nat ->
 pos_Rl (cons_Rlist l1 r0) i =
 pos_Rl r0 (i - Rlength l1)) ->
forall (l1 : Rlist) (i : nat),
(Rlength l1 <= i)%nat ->
(i < Rlength (cons_Rlist l1 (cons r r0)))%nat ->
pos_Rl (cons_Rlist l1 (cons r r0)) i =
pos_Rl (cons r r0) (i - Rlength l1)
  intros; rewrite RList_P28 in H0; elim (lt_irrefl _ (le_lt_trans _ _ _ H H0)).l2:Rlist
forall (r : R) (r0 : Rlist),
(forall (l1 : Rlist) (i : nat),
 (Rlength l1 <= i)%nat ->
 (i < Rlength (cons_Rlist l1 r0))%nat ->
 pos_Rl (cons_Rlist l1 r0) i =
 pos_Rl r0 (i - Rlength l1)) ->
forall (l1 : Rlist) (i : nat),
(Rlength l1 <= i)%nat ->
(i < Rlength (cons_Rlist l1 (cons r r0)))%nat ->
pos_Rl (cons_Rlist l1 (cons r r0)) i =
pos_Rl (cons r r0) (i - Rlength l1)
  intros;
    replace (cons_Rlist l1 (cons r r0)) with
    (cons_Rlist (cons_Rlist l1 (cons r nil)) r0).l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
pos_Rl (cons_Rlist (cons_Rlist l1 (cons r nil)) r0) i =
pos_Rl (cons r r0) (i - Rlength l1)
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
cons_Rlist (cons_Rlist l1 (cons r nil)) r0 =
cons_Rlist l1 (cons r r0)
  inversion H0.l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
H2:Rlength l1 = i
pos_Rl (cons_Rlist (cons_Rlist l1 (cons r nil)) r0)
  (Rlength l1) =
pos_Rl (cons r r0) (Rlength l1 - Rlength l1)
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
pos_Rl (cons_Rlist (cons_Rlist l1 (cons r nil)) r0)
  (S m) = pos_Rl (cons r r0) (S m - Rlength l1)
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
cons_Rlist (cons_Rlist l1 (cons r nil)) r0 =
cons_Rlist l1 (cons r r0)
  rewrite <- minus_n_n; simpl; rewrite RList_P26.l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
H2:Rlength l1 = i
pos_Rl (cons_Rlist l1 (cons r nil)) (Rlength l1) = r
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
H2:Rlength l1 = i
(Rlength l1 < Rlength (cons_Rlist l1 (cons r nil)))%nat
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
pos_Rl (cons_Rlist (cons_Rlist l1 (cons r nil)) r0)
  (S m) = pos_Rl (cons r r0) (S m - Rlength l1)
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
cons_Rlist (cons_Rlist l1 (cons r nil)) r0 =
cons_Rlist l1 (cons r r0)
  clear l2 r0 H i H0 H1 H2; induction  l1 as [| r0 l1 Hrecl1].r:R
pos_Rl (cons_Rlist nil (cons r nil)) (Rlength nil) = r
r, r0:R
l1:Rlist
Hrecl1:pos_Rl (cons_Rlist l1 (cons r nil))
  (Rlength l1) = r
pos_Rl (cons_Rlist (cons r0 l1) (cons r nil))
  (Rlength (cons r0 l1)) = r
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
H2:Rlength l1 = i
(Rlength l1 < Rlength (cons_Rlist l1 (cons r nil)))%nat
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
pos_Rl (cons_Rlist (cons_Rlist l1 (cons r nil)) r0)
  (S m) = pos_Rl (cons r r0) (S m - Rlength l1)
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
cons_Rlist (cons_Rlist l1 (cons r nil)) r0 =
cons_Rlist l1 (cons r r0)
  reflexivity.r, r0:R
l1:Rlist
Hrecl1:pos_Rl (cons_Rlist l1 (cons r nil))
  (Rlength l1) = r
pos_Rl (cons_Rlist (cons r0 l1) (cons r nil))
  (Rlength (cons r0 l1)) = r
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
H2:Rlength l1 = i
(Rlength l1 < Rlength (cons_Rlist l1 (cons r nil)))%nat
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
pos_Rl (cons_Rlist (cons_Rlist l1 (cons r nil)) r0)
  (S m) = pos_Rl (cons r r0) (S m - Rlength l1)
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
cons_Rlist (cons_Rlist l1 (cons r nil)) r0 =
cons_Rlist l1 (cons r r0)
  simpl; assumption.l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
H2:Rlength l1 = i
(Rlength l1 < Rlength (cons_Rlist l1 (cons r nil)))%nat
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
pos_Rl (cons_Rlist (cons_Rlist l1 (cons r nil)) r0)
  (S m) = pos_Rl (cons r r0) (S m - Rlength l1)
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
cons_Rlist (cons_Rlist l1 (cons r nil)) r0 =
cons_Rlist l1 (cons r r0)
  rewrite RList_P23; rewrite plus_comm; simpl; apply lt_n_Sn.l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
pos_Rl (cons_Rlist (cons_Rlist l1 (cons r nil)) r0)
  (S m) = pos_Rl (cons r r0) (S m - Rlength l1)
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
cons_Rlist (cons_Rlist l1 (cons r nil)) r0 =
cons_Rlist l1 (cons r r0)
  replace (S m - Rlength l1)%nat with (S (S m - S (Rlength l1))).l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
pos_Rl (cons_Rlist (cons_Rlist l1 (cons r nil)) r0)
  (S m) =
pos_Rl (cons r r0) (S (S m - S (Rlength l1)))
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
S (S m - S (Rlength l1)) = (S m - Rlength l1)%nat
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
cons_Rlist (cons_Rlist l1 (cons r nil)) r0 =
cons_Rlist l1 (cons r r0)
  rewrite H3; simpl;
    replace (S (Rlength l1)) with (Rlength (cons_Rlist l1 (cons r nil))).l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
pos_Rl (cons_Rlist (cons_Rlist l1 (cons r nil)) r0) i =
pos_Rl r0 (i - Rlength (cons_Rlist l1 (cons r nil)))
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
Rlength (cons_Rlist l1 (cons r nil)) = S (Rlength l1)
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
S (S m - S (Rlength l1)) = (S m - Rlength l1)%nat
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
cons_Rlist (cons_Rlist l1 (cons r nil)) r0 =
cons_Rlist l1 (cons r r0)
  apply (H (cons_Rlist l1 (cons r nil)) i).l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
(Rlength (cons_Rlist l1 (cons r nil)) <= i)%nat
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
(i <
 Rlength (cons_Rlist (cons_Rlist l1 (cons r nil)) r0))%nat
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
Rlength (cons_Rlist l1 (cons r nil)) = S (Rlength l1)
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
S (S m - S (Rlength l1)) = (S m - Rlength l1)%nat
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
cons_Rlist (cons_Rlist l1 (cons r nil)) r0 =
cons_Rlist l1 (cons r r0)
  rewrite RList_P23; rewrite plus_comm; simpl; rewrite <- H3;
    apply le_n_S; assumption.l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
(i <
 Rlength (cons_Rlist (cons_Rlist l1 (cons r nil)) r0))%nat
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
Rlength (cons_Rlist l1 (cons r nil)) = S (Rlength l1)
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
S (S m - S (Rlength l1)) = (S m - Rlength l1)%nat
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
cons_Rlist (cons_Rlist l1 (cons r nil)) r0 =
cons_Rlist l1 (cons r r0)
  repeat rewrite RList_P23; simpl; rewrite RList_P23 in H1;
    rewrite plus_comm in H1; simpl in H1; rewrite (plus_comm (Rlength l1));
      simpl; rewrite plus_comm; apply H1.l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
Rlength (cons_Rlist l1 (cons r nil)) = S (Rlength l1)
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
S (S m - S (Rlength l1)) = (S m - Rlength l1)%nat
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
cons_Rlist (cons_Rlist l1 (cons r nil)) r0 =
cons_Rlist l1 (cons r r0)
  rewrite RList_P23; rewrite plus_comm; reflexivity.l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
m:nat
H2:(Rlength l1 <= m)%nat
H3:S m = i
S (S m - S (Rlength l1)) = (S m - Rlength l1)%nat
l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
cons_Rlist (cons_Rlist l1 (cons r nil)) r0 =
cons_Rlist l1 (cons r r0)
  change (S (m - Rlength l1) = (S m - Rlength l1)%nat);
    apply minus_Sn_m; assumption.l2:Rlist
r:R
r0:Rlist
H:forall (l0 : Rlist) (i0 : nat),
(Rlength l0 <= i0)%nat ->
(i0 < Rlength (cons_Rlist l0 r0))%nat ->
pos_Rl (cons_Rlist l0 r0) i0 =
pos_Rl r0 (i0 - Rlength l0)
l1:Rlist
i:nat
H0:(Rlength l1 <= i)%nat
H1:(i < Rlength (cons_Rlist l1 (cons r r0)))%nat
cons_Rlist (cons_Rlist l1 (cons r nil)) r0 =
cons_Rlist l1 (cons r r0)
  replace (cons r r0) with (cons_Rlist (cons r nil) r0);
  [ symmetry ; apply RList_P27 | reflexivity ].
Qed.