Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 588 insertions, 549 deletions

diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index 551aec98..19f2b4ff 100644
--- a/theories/Reals/RList.v
+++ b/theories/Reals/RList.v
@@ -5,208 +5,217 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
- 
-(*i $Id: RList.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+
+(*i $Id: RList.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
 Open Local Scope R_scope.
 
 Inductive Rlist : Type :=
-  | nil : Rlist
-  | cons : R -> Rlist -> Rlist.
+| nil : Rlist
+| cons : R -> Rlist -> Rlist.
 
 Fixpoint In (x:R) (l:Rlist) {struct l} : Prop :=
   match l with
-  | nil => False
-  | cons a l' => x = a \/ In x l'
+    | 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')
+    | nil => 0%nat
+    | cons a l' => S (Rlength l')
   end.
 
 Fixpoint MaxRlist (l:Rlist) : R :=
   match l with
-  | nil => 0
-  | cons a l1 =>
+    | nil => 0
+    | cons a l1 =>
       match l1 with
-      | nil => a
-      | cons a' l2 => Rmax a (MaxRlist l1)
+        | nil => a
+        | cons a' l2 => Rmax a (MaxRlist l1)
       end
   end.
 
 Fixpoint MinRlist (l:Rlist) : R :=
   match l with
-  | nil => 1
-  | cons a l1 =>
+    | nil => 1
+    | cons a l1 =>
       match l1 with
-      | nil => a
-      | cons a' l2 => Rmin a (MinRlist l1)
+        | 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.
-intros; induction  l as [| r l Hrecl].
-simpl in H; elim H.
-induction  l as [| r0 l Hrecl0].
-simpl in H; elim H; intro.
-simpl in |- *; right; assumption.
-elim H0.
-replace (MaxRlist (cons r (cons r0 l))) with (Rmax r (MaxRlist (cons r0 l))).
-simpl in H; decompose [or] H.
-rewrite H0; apply RmaxLess1.
-unfold Rmax in |- *; case (Rle_dec r (MaxRlist (cons r0 l))); intro.
-apply Hrecl; simpl in |- *; tauto.
-apply Rle_trans with (MaxRlist (cons r0 l));
- [ apply Hrecl; simpl in |- *; tauto | left; auto with real ].
-unfold Rmax in |- *; case (Rle_dec r (MaxRlist (cons r0 l))); intro.
-apply Hrecl; simpl in |- *; tauto.
-apply Rle_trans with (MaxRlist (cons r0 l));
- [ apply Hrecl; simpl in |- *; tauto | left; auto with real ].
-reflexivity.
+Proof.
+  intros; induction  l as [| r l Hrecl].
+  simpl in H; elim H.
+  induction  l as [| r0 l Hrecl0].
+  simpl in H; elim H; intro.
+  simpl in |- *; right; assumption.
+  elim H0.
+  replace (MaxRlist (cons r (cons r0 l))) with (Rmax r (MaxRlist (cons r0 l))).
+  simpl in H; decompose [or] H.
+  rewrite H0; apply RmaxLess1.
+  unfold Rmax in |- *; case (Rle_dec r (MaxRlist (cons r0 l))); intro.
+  apply Hrecl; simpl in |- *; tauto.
+  apply Rle_trans with (MaxRlist (cons r0 l));
+    [ apply Hrecl; simpl in |- *; tauto | left; auto with real ].
+  unfold Rmax in |- *; case (Rle_dec r (MaxRlist (cons r0 l))); intro.
+  apply Hrecl; simpl in |- *; tauto.
+  apply Rle_trans with (MaxRlist (cons r0 l));
+    [ apply Hrecl; simpl in |- *; tauto | left; auto with real ].
+  reflexivity.
 Qed.
 
 Fixpoint AbsList (l:Rlist) (x:R) {struct l} : Rlist :=
   match l with
-  | nil => nil
-  | cons a l' => cons (Rabs (a - x) / 2) (AbsList l' x)
+    | 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.
-intros; induction  l as [| r l Hrecl].
-simpl in H; elim H.
-induction  l as [| r0 l Hrecl0].
-simpl in H; elim H; intro.
-simpl in |- *; right; symmetry  in |- *; assumption.
-elim H0.
-replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))).
-simpl in H; decompose [or] H.
-rewrite H0; apply Rmin_l.
-unfold Rmin in |- *; case (Rle_dec r (MinRlist (cons r0 l))); intro.
-apply Rle_trans with (MinRlist (cons r0 l)).
-assumption.
-apply Hrecl; simpl in |- *; tauto.
-apply Hrecl; simpl in |- *; tauto.
-apply Rle_trans with (MinRlist (cons r0 l)).
-apply Rmin_r.
-apply Hrecl; simpl in |- *; tauto.
-reflexivity.
+Proof.
+  intros; induction  l as [| r l Hrecl].
+  simpl in H; elim H.
+  induction  l as [| r0 l Hrecl0].
+  simpl in H; elim H; intro.
+  simpl in |- *; right; symmetry  in |- *; assumption.
+  elim H0.
+  replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))).
+  simpl in H; decompose [or] H.
+  rewrite H0; apply Rmin_l.
+  unfold Rmin in |- *; case (Rle_dec r (MinRlist (cons r0 l))); intro.
+  apply Rle_trans with (MinRlist (cons r0 l)).
+  assumption.
+  apply Hrecl; simpl in |- *; tauto.
+  apply Hrecl; simpl in |- *; tauto.
+  apply Rle_trans with (MinRlist (cons r0 l)).
+  apply Rmin_r.
+  apply Hrecl; simpl in |- *; tauto.
+  reflexivity.
 Qed.
 
 Lemma AbsList_P1 :
- forall (l:Rlist) (x y:R), In y l -> In (Rabs (y - x) / 2) (AbsList l x).
-intros; induction  l as [| r l Hrecl].
-elim H.
-simpl in |- *; simpl in H; elim H; intro.
-left; rewrite H0; reflexivity.
-right; apply Hrecl; assumption.
+  forall (l:Rlist) (x y:R), In y l -> In (Rabs (y - x) / 2) (AbsList l x).
+Proof.
+  intros; induction  l as [| r l Hrecl].
+  elim H.
+  simpl in |- *; simpl in H; elim H; intro.
+  left; rewrite H0; reflexivity.
+  right; apply Hrecl; assumption.
 Qed.
 
 Lemma MinRlist_P2 :
- forall l:Rlist, (forall y:R, In y l -> 0 < y) -> 0 < MinRlist l.
-intros; induction  l as [| r l Hrecl].
-apply Rlt_0_1.
-induction  l as [| r0 l Hrecl0].
-simpl in |- *; apply H; simpl in |- *; tauto.
-replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))).
-unfold Rmin in |- *; case (Rle_dec r (MinRlist (cons r0 l))); intro.
-apply H; simpl in |- *; tauto.
-apply Hrecl; intros; apply H; simpl in |- *; simpl in H0; tauto.
-reflexivity.
+  forall l:Rlist, (forall y:R, In y l -> 0 < y) -> 0 < MinRlist l.
+Proof.
+  intros; induction  l as [| r l Hrecl].
+  apply Rlt_0_1.
+  induction  l as [| r0 l Hrecl0].
+  simpl in |- *; apply H; simpl in |- *; tauto.
+  replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))).
+  unfold Rmin in |- *; case (Rle_dec r (MinRlist (cons r0 l))); intro.
+  apply H; simpl in |- *; tauto.
+  apply Hrecl; intros; apply H; simpl in |- *; simpl in H0; tauto.
+  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.
-intros; induction  l as [| r l Hrecl].
-elim H.
-elim H; intro.
-exists r; split.
-simpl in |- *; tauto.
-assumption.
-assert (H1 := Hrecl H0); elim H1; intros; elim H2; clear H2; intros;
- exists x0; simpl in |- *; simpl in H2; tauto.
+  forall (l:Rlist) (x y:R),
+    In y (AbsList l x) ->  exists z : R, In z l /\ y = Rabs (z - x) / 2.
+Proof.
+  intros; induction  l as [| r l Hrecl].
+  elim H.
+  elim H; intro.
+  exists r; split.
+  simpl in |- *; tauto.
+  assumption.
+  assert (H1 := Hrecl H0); elim H1; intros; elim H2; clear H2; intros;
+    exists x0; simpl in |- *; simpl in H2; tauto.
 Qed.
 
 Lemma MaxRlist_P2 :
- forall l:Rlist, (exists y : R, In y l) -> In (MaxRlist l) l.
-intros; induction  l as [| r l Hrecl].
-simpl in H; elim H; trivial.
-induction  l as [| r0 l Hrecl0].
-simpl in |- *; left; reflexivity.
-change (In (Rmax r (MaxRlist (cons r0 l))) (cons r (cons r0 l))) in |- *;
- unfold Rmax in |- *; case (Rle_dec r (MaxRlist (cons r0 l))); 
- intro.
-right; apply Hrecl; exists r0; left; reflexivity.
-left; reflexivity.
+  forall l:Rlist, (exists y : R, In y l) -> In (MaxRlist l) l.
+Proof.
+  intros; induction  l as [| r l Hrecl].
+  simpl in H; elim H; trivial.
+  induction  l as [| r0 l Hrecl0].
+  simpl in |- *; left; reflexivity.
+  change (In (Rmax r (MaxRlist (cons r0 l))) (cons r (cons r0 l))) in |- *;
+    unfold Rmax in |- *; case (Rle_dec r (MaxRlist (cons r0 l))); 
+      intro.
+  right; apply Hrecl; exists r0; left; reflexivity.
+  left; reflexivity.
 Qed.
 
 Fixpoint pos_Rl (l:Rlist) (i:nat) {struct l} : R :=
   match l with
-  | nil => 0
-  | cons a l' => match i with
-                 | O => a
-                 | S i' => pos_Rl l' i'
-                 end
+    | 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)).
-intros; induction  l as [| r l Hrecl];
- [ elim (lt_n_O _ H)
- | simpl in |- *; case (Rlength l); [ reflexivity | intro; reflexivity ] ].
+  forall (l:Rlist) (a:R),
+    (0 < Rlength l)%nat ->
+    pos_Rl (cons a l) (Rlength l) = pos_Rl l (pred (Rlength l)).
+Proof.
+  intros; induction  l as [| r l Hrecl];
+    [ elim (lt_n_O _ H)
+      | simpl in |- *; 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).
-intros; induction  l as [| r l Hrecl].
-split; intro;
- [ elim H | elim H; intros; elim H0; intros; elim (lt_n_O _ H1) ].
-split; intro.
-elim H; intro.
-exists 0%nat; split;
- [ simpl in |- *; apply lt_O_Sn | simpl in |- *; apply H0 ].
-elim Hrecl; intros; assert (H3 := H1 H0); elim H3; intros; elim H4; intros;
- exists (S x0); split;
- [ simpl in |- *; apply lt_n_S; assumption | simpl in |- *; assumption ].
-elim H; intros; elim H0; intros; elim (zerop x0); intro.
-rewrite a in H2; simpl in H2; left; assumption.
-right; elim Hrecl; intros; apply H4; assert (H5 : S (pred x0) = x0).
-symmetry  in |- *; apply S_pred with 0%nat; assumption.
-exists (pred x0); split;
- [ simpl in H1; apply lt_S_n; rewrite H5; assumption
- | rewrite <- H5 in H2; simpl in H2; assumption ].
+  forall (l:Rlist) (x:R),
+    In x l <-> (exists i : nat, (i < Rlength l)%nat /\ x = pos_Rl l i).
+Proof.
+  intros; induction  l as [| r l Hrecl].
+  split; intro;
+    [ elim H | elim H; intros; elim H0; intros; elim (lt_n_O _ H1) ].
+  split; intro.
+  elim H; intro.
+  exists 0%nat; split;
+    [ simpl in |- *; apply lt_O_Sn | simpl in |- *; apply H0 ].
+  elim Hrecl; intros; assert (H3 := H1 H0); elim H3; intros; elim H4; intros;
+    exists (S x0); split;
+      [ simpl in |- *; apply lt_n_S; assumption | simpl in |- *; assumption ].
+  elim H; intros; elim H0; intros; elim (zerop x0); intro.
+  rewrite a in H2; simpl in H2; left; assumption.
+  right; elim Hrecl; intros; apply H4; assert (H5 : S (pred x0) = x0).
+  symmetry  in |- *; apply S_pred with 0%nat; assumption.
+  exists (pred x0); split;
+    [ simpl in H1; apply lt_S_n; rewrite H5; assumption
+      | rewrite <- H5 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) ->
+  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].
-exists nil; intros; split;
- [ reflexivity | intros; simpl in H0; elim (lt_n_O _ H0) ].
-assert (H0 : In r (cons r l)).
-simpl in |- *; left; reflexivity.
-assert (H1 := H _ H0);
- assert (H2 : forall x:R, In x l ->  exists y : R, P x y).
-intros; apply H; simpl in |- *; right; assumption.
-assert (H3 := Hrecl H2); elim H1; intros; elim H3; intros; exists (cons x x0);
- intros; elim H5; clear H5; intros; split.
-simpl in |- *; rewrite H5; reflexivity.
-intros; elim (zerop i); intro.
-rewrite a; simpl in |- *; assumption.
-assert (H8 : i = S (pred i)).
-apply S_pred with 0%nat; assumption.
-rewrite H8; simpl in |- *; apply H6; simpl in H7; apply lt_S_n; rewrite <- H8;
- assumption.
+      Rlength l = Rlength l' /\
+      (forall i:nat, (i < Rlength l)%nat -> P (pos_Rl l i) (pos_Rl l' i)).
+Proof.
+  intros; induction  l as [| r l Hrecl].
+  exists nil; intros; split;
+    [ reflexivity | intros; simpl in H0; elim (lt_n_O _ H0) ].
+  assert (H0 : In r (cons r l)).
+  simpl in |- *; left; reflexivity.
+  assert (H1 := H _ H0);
+    assert (H2 : forall x:R, In x l ->  exists y : R, P x y).
+  intros; apply H; simpl in |- *; right; assumption.
+  assert (H3 := Hrecl H2); elim H1; intros; elim H3; intros; exists (cons x x0);
+    intros; elim H5; clear H5; intros; split.
+  simpl in |- *; rewrite H5; reflexivity.
+  intros; elim (zerop i); intro.
+  rewrite a; simpl in |- *; assumption.
+  assert (H8 : i = S (pred i)).
+  apply S_pred with 0%nat; assumption.
+  rewrite H8; simpl in |- *; apply H6; simpl in H7; apply lt_S_n; rewrite <- H8;
+    assumption.
 Qed.
 
 Definition ordered_Rlist (l:Rlist) : Prop :=
@@ -214,531 +223,561 @@ Definition ordered_Rlist (l:Rlist) : Prop :=
 
 Fixpoint insert (l:Rlist) (x:R) {struct l} : Rlist :=
   match l with
-  | nil => cons x nil
-  | cons a l' =>
+    | nil => cons x nil
+    | cons a l' =>
       match Rle_dec a x with
-      | left _ => cons a (insert l' x)
-      | right _ => cons x l
+        | left _ => cons a (insert l' x)
+        | right _ => cons x l
       end
   end.
 
 Fixpoint cons_Rlist (l k:Rlist) {struct l} : Rlist :=
   match l with
-  | nil => k
-  | cons a l' => cons a (cons_Rlist l' k)
+    | nil => k
+    | cons a l' => cons a (cons_Rlist l' k)
   end.
 
 Fixpoint cons_ORlist (k l:Rlist) {struct k} : Rlist :=
   match k with
-  | nil => l
-  | cons a k' => cons_ORlist k' (insert l a)
+    | nil => l
+    | cons a k' => cons_ORlist k' (insert l a)
   end.
 
 Fixpoint app_Rlist (l:Rlist) (f:R -> R) {struct l} : Rlist :=
   match l with
-  | nil => nil
-  | cons a l' => cons (f a) (app_Rlist l' f)
+    | nil => nil
+    | cons a l' => cons (f a) (app_Rlist l' f)
   end.
 
 Fixpoint mid_Rlist (l:Rlist) (x:R) {struct l} : Rlist :=
   match l with
-  | nil => nil
-  | cons a l' => cons ((x + a) / 2) (mid_Rlist l' a)
+    | 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'
+    | 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
+    | 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.
-intros; induction  l as [| r l Hrecl];
- [ left; reflexivity
- | simpl in |- *; case (Rle_dec r a); intro;
-    [ right; reflexivity | left; reflexivity ] ].
+  forall (l:Rlist) (a:R),
+    pos_Rl (insert l a) 0 = a \/ pos_Rl (insert l a) 0 = pos_Rl l 0.
+Proof.
+  intros; induction  l as [| r l Hrecl];
+    [ left; reflexivity
+      | simpl in |- *; 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).
-intros; induction  l as [| r l Hrecl].
-simpl in |- *; unfold ordered_Rlist in |- *; intros; simpl in H0;
- elim (lt_n_O _ H0).
-simpl in |- *; case (Rle_dec r a); intro.
-assert (H1 : ordered_Rlist l).
-unfold ordered_Rlist in |- *; unfold ordered_Rlist in H; intros;
- assert (H1 : (S i < pred (Rlength (cons r l)))%nat);
- [ simpl in |- *; replace (Rlength l) with (S (pred (Rlength l)));
-    [ apply lt_n_S; assumption
-    | symmetry  in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *;
-       intro; rewrite <- H1 in H0; simpl in H0; elim (lt_n_O _ H0) ]
- | apply (H _ H1) ].
-assert (H2 := Hrecl H1); unfold ordered_Rlist in |- *; intros;
- induction  i as [| i Hreci].
-simpl in |- *; assert (H3 := RList_P0 l a); elim H3; intro.
-rewrite H4; assumption.
-induction  l as [| r1 l Hrecl0];
- [ simpl in |- *; assumption
- | rewrite H4; apply (H 0%nat); simpl in |- *; apply lt_O_Sn ].
-simpl in |- *; 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 in |- *; intro;
-    rewrite <- H3 in H0; elim (lt_n_O _ H0) ].
-unfold ordered_Rlist in |- *; intros; induction  i as [| i Hreci];
- [ simpl in |- *; auto with real
- | change (pos_Rl (cons r l) i <= pos_Rl (cons r l) (S i)) in |- *; apply H;
-    simpl in H0; simpl in |- *; apply (lt_S_n _ _ H0) ].
+  forall (l:Rlist) (a:R), ordered_Rlist l -> ordered_Rlist (insert l a).
+Proof.
+  intros; induction  l as [| r l Hrecl].
+  simpl in |- *; unfold ordered_Rlist in |- *; intros; simpl in H0;
+    elim (lt_n_O _ H0).
+  simpl in |- *; case (Rle_dec r a); intro.
+  assert (H1 : ordered_Rlist l).
+  unfold ordered_Rlist in |- *; unfold ordered_Rlist in H; intros;
+    assert (H1 : (S i < pred (Rlength (cons r l)))%nat);
+      [ simpl in |- *; replace (Rlength l) with (S (pred (Rlength l)));
+        [ apply lt_n_S; assumption
+          | symmetry  in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *;
+            intro; rewrite <- H1 in H0; simpl in H0; elim (lt_n_O _ H0) ]
+        | apply (H _ H1) ].
+  assert (H2 := Hrecl H1); unfold ordered_Rlist in |- *; intros;
+    induction  i as [| i Hreci].
+  simpl in |- *; assert (H3 := RList_P0 l a); elim H3; intro.
+  rewrite H4; assumption.
+  induction  l as [| r1 l Hrecl0];
+    [ simpl in |- *; assumption
+      | rewrite H4; apply (H 0%nat); simpl in |- *; apply lt_O_Sn ].
+  simpl in |- *; 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 in |- *; intro;
+        rewrite <- H3 in H0; elim (lt_n_O _ H0) ].
+  unfold ordered_Rlist in |- *; intros; induction  i as [| i Hreci];
+    [ simpl in |- *; auto with real
+      | change (pos_Rl (cons r l) i <= pos_Rl (cons r l) (S i)) in |- *; apply H;
+        simpl in H0; simpl in |- *; apply (lt_S_n _ _ H0) ].
 Qed.
 
 Lemma RList_P2 :
- forall l1 l2:Rlist, ordered_Rlist l2 -> ordered_Rlist (cons_ORlist l1 l2).
-simple induction l1;
- [ intros; simpl in |- *; apply H
- | intros; simpl in |- *; apply H; apply RList_P1; assumption ].
+  forall l1 l2:Rlist, ordered_Rlist l2 -> ordered_Rlist (cons_ORlist l1 l2).
+Proof.
+  simple induction l1;
+    [ intros; simpl in |- *; apply H
+      | intros; simpl in |- *; 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).
-intros; split; intro;
- [ induction  l as [| r l Hrecl] | induction  l as [| r l Hrecl] ].
-elim H.
-elim H; intro;
- [ exists 0%nat; split; [ apply H0 | simpl in |- *; apply lt_O_Sn ]
- | elim (Hrecl H0); intros; elim H1; clear H1; intros; exists (S x0); split;
-    [ apply H1 | simpl in |- *; apply lt_n_S; assumption ] ].
-elim H; intros; elim H0; intros; elim (lt_n_O _ H2).
-simpl in |- *; 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 ] ].
+  forall (l:Rlist) (x:R),
+    In x l <-> (exists i : nat, x = pos_Rl l i /\ (i < Rlength l)%nat).
+Proof.
+  intros; split; intro;
+    [ induction  l as [| r l Hrecl] | induction  l as [| r l Hrecl] ].
+  elim H.
+  elim H; intro;
+    [ exists 0%nat; split; [ apply H0 | simpl in |- *; apply lt_O_Sn ]
+      | elim (Hrecl H0); intros; elim H1; clear H1; intros; exists (S x0); split;
+        [ apply H1 | simpl in |- *; apply lt_n_S; assumption ] ].
+  elim H; intros; elim H0; intros; elim (lt_n_O _ H2).
+  simpl in |- *; 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.
-intros; unfold ordered_Rlist in |- *; intros; apply (H (S i)); simpl in |- *;
- replace (Rlength l1) with (S (pred (Rlength l1)));
- [ apply lt_n_S; assumption
- | symmetry  in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *;
-    intro; rewrite <- H1 in H0; elim (lt_n_O _ H0) ].
+  forall (l1:Rlist) (a:R), ordered_Rlist (cons a l1) -> ordered_Rlist l1.
+Proof.
+  intros; unfold ordered_Rlist in |- *; intros; apply (H (S i)); simpl in |- *;
+    replace (Rlength l1) with (S (pred (Rlength l1)));
+    [ apply lt_n_S; assumption
+      | symmetry  in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *;
+        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.
-intros; induction  l as [| r l Hrecl];
- [ elim H0
- | simpl in |- *; elim H0; intro;
-    [ rewrite H1; right; reflexivity
-    | apply Rle_trans with (pos_Rl l 0);
-       [ apply (H 0%nat); simpl in |- *; induction  l as [| r0 l Hrecl0];
-          [ elim H1 | simpl in |- *; apply lt_O_Sn ]
-       | apply Hrecl; [ eapply RList_P4; apply H | assumption ] ] ] ].
+  forall (l:Rlist) (x:R), ordered_Rlist l -> In x l -> pos_Rl l 0 <= x.
+Proof.
+  intros; induction  l as [| r l Hrecl];
+    [ elim H0
+      | simpl in |- *; elim H0; intro;
+        [ rewrite H1; right; reflexivity
+          | apply Rle_trans with (pos_Rl l 0);
+            [ apply (H 0%nat); simpl in |- *; induction  l as [| r0 l Hrecl0];
+              [ elim H1 | simpl in |- *; 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,
+  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.
-intros; right; reflexivity.
-unfold ordered_Rlist in |- *; intros; simpl in H0; elim (lt_n_O _ H0).
-intros; induction  i as [| i Hreci];
- [ induction  j as [| j Hrecj];
-    [ right; reflexivity
-    | simpl in |- *; apply Rle_trans with (pos_Rl r0 0);
-       [ apply (H0 0%nat); simpl in |- *; simpl in H2; apply neq_O_lt;
-          red in |- *; 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 in |- *; elim H; intros; apply H3;
-       [ apply RList_P4 with r; assumption
-       | apply le_S_n; assumption
-       | simpl in H2; apply lt_S_n; assumption ] ] ].
-unfold ordered_Rlist in |- *; intros; apply H0;
- [ apply le_n_Sn | simpl in |- *; simpl in H1; apply lt_n_S; assumption ].
+Proof.
+  simple induction l; split; intro.
+  intros; right; reflexivity.
+  unfold ordered_Rlist in |- *; intros; simpl in H0; elim (lt_n_O _ H0).
+  intros; induction  i as [| i Hreci];
+    [ induction  j as [| j Hrecj];
+      [ right; reflexivity
+        | simpl in |- *; apply Rle_trans with (pos_Rl r0 0);
+          [ apply (H0 0%nat); simpl in |- *; simpl in H2; apply neq_O_lt;
+            red in |- *; 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 in |- *; elim H; intros; apply H3;
+            [ apply RList_P4 with r; assumption
+              | apply le_S_n; assumption
+              | simpl in H2; apply lt_S_n; assumption ] ] ].
+  unfold ordered_Rlist in |- *; intros; apply H0;
+    [ apply le_n_Sn | simpl in |- *; 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)).
-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))).
-apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;
- rewrite <- H6 in H5; elim (lt_n_O _ H5).
-apply H3;
- [ rewrite H6 in H5; apply lt_n_Sm_le; assumption
- | apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H7 in H5;
-    elim (lt_n_O _ H5) ].
+  forall (l:Rlist) (x:R),
+    ordered_Rlist l -> In x l -> x <= pos_Rl l (pred (Rlength l)).
+Proof.
+  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))).
+  apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;
+    rewrite <- H6 in H5; elim (lt_n_O _ H5).
+  apply H3;
+    [ rewrite H6 in H5; apply lt_n_Sm_le; assumption
+      | apply lt_pred_n_n; apply neq_O_lt; red in |- *; 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.
-simple induction l.
-intros; split; intro; simpl in H; apply H.
-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 in |- *; 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 ].
+  forall (l:Rlist) (a x:R), In x (insert l a) <-> x = a \/ In x l.
+Proof.
+  simple induction l.
+  intros; split; intro; simpl in H; apply H.
+  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 in |- *; 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.
-simple induction l1.
-intros; split; intro;
- [ simpl in H; right; assumption
- | simpl in |- *; elim H; intro; [ elim H0 | assumption ] ].
-intros; split.
-simpl in |- *; 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 ] ].
-intro; simpl in |- *; 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 ].
+  forall (l1 l2:Rlist) (x:R), In x (cons_ORlist l1 l2) <-> In x l1 \/ In x l2.
+Proof.
+  simple induction l1.
+  intros; split; intro;
+    [ simpl in H; right; assumption
+      | simpl in |- *; elim H; intro; [ elim H0 | assumption ] ].
+  intros; split.
+  simpl in |- *; 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 ] ].
+  intro; simpl in |- *; 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).
-intros; induction  l as [| r l Hrecl];
- [ reflexivity
- | simpl in |- *; case (Rle_dec r a); intro;
-    [ simpl in |- *; rewrite Hrecl; reflexivity | reflexivity ] ].
+  forall (l:Rlist) (a:R), Rlength (insert l a) = S (Rlength l).
+Proof.
+  intros; induction  l as [| r l Hrecl];
+    [ reflexivity
+      | simpl in |- *; case (Rle_dec r a); intro;
+        [ simpl in |- *; rewrite Hrecl; reflexivity | reflexivity ] ].
 Qed.
 
 Lemma RList_P11 :
- forall l1 l2:Rlist,
-   Rlength (cons_ORlist l1 l2) = (Rlength l1 + Rlength l2)%nat.
-simple induction l1;
- [ intro; reflexivity
- | intros; simpl in |- *; rewrite (H (insert l2 r)); rewrite RList_P10;
-    apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; 
-    rewrite S_INR; ring ].
+  forall l1 l2:Rlist,
+    Rlength (cons_ORlist l1 l2) = (Rlength l1 + Rlength l2)%nat.
+Proof.
+  simple induction l1;
+    [ intro; reflexivity
+      | intros; simpl in |- *; 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).
-simple induction l;
- [ intros; elim (lt_n_O _ H)
- | intros; induction  i as [| i Hreci];
-    [ reflexivity | simpl in |- *; apply H; apply lt_S_n; apply H0 ] ].
+  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.
+  simple induction l;
+    [ intros; elim (lt_n_O _ H)
+      | intros; induction  i as [| i Hreci];
+        [ reflexivity | simpl in |- *; 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.
-simple induction l.
-intros; simpl in H; elim (lt_n_O _ H).
-simple induction r0.
-intros; simpl in H0; elim (lt_n_O _ H0).
-intros; simpl in H1; induction  i as [| i Hreci].
-reflexivity.
-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) 
- in |- *; apply H0; simpl in |- *; apply lt_S_n; assumption.
+  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.
+Proof.
+  simple induction l.
+  intros; simpl in H; elim (lt_n_O _ H).
+  simple induction r0.
+  intros; simpl in H0; elim (lt_n_O _ H0).
+  intros; simpl in H1; induction  i as [| i Hreci].
+  reflexivity.
+  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) 
+    in |- *; apply H0; simpl in |- *; apply lt_S_n; assumption.
 Qed.
 
 Lemma RList_P14 : forall (l:Rlist) (a:R), Rlength (mid_Rlist l a) = Rlength l.
-simple induction l; intros;
- [ reflexivity | simpl in |- *; rewrite (H r); reflexivity ].
+Proof.
+  simple induction l; intros;
+    [ reflexivity | simpl in |- *; 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.
-intros; apply Rle_antisym.
-induction  l1 as [| r l1 Hrecl1];
- [ simpl in |- *; simpl in H1; right; symmetry  in |- *; 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 ] ] ].
-induction  l1 as [| r l1 Hrecl1];
- [ simpl in |- *; 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 in |- *; 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 ] ] ].
+  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.
+  intros; apply Rle_antisym.
+  induction  l1 as [| r l1 Hrecl1];
+    [ simpl in |- *; simpl in H1; right; symmetry  in |- *; 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 ] ] ].
+  induction  l1 as [| r l1 Hrecl1];
+    [ simpl in |- *; 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 in |- *; 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)).
-intros; apply Rle_antisym.
-induction  l1 as [| r l1 Hrecl1].
-simpl in |- *; simpl in H1; right; symmetry  in |- *; assumption. 
-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 in |- *; apply lt_n_Sn ]
- | elim
-    (RList_P9 (cons r l1) l2
-       (pos_Rl (cons_ORlist (cons r l1) l2)
+  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)).
+Proof.
+  intros; apply Rle_antisym.
+  induction  l1 as [| r l1 Hrecl1].
+  simpl in |- *; simpl in H1; right; symmetry  in |- *; assumption. 
+  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; assert (H5 := H3 H2); elim H5; intro;
-    [ apply RList_P7; assumption | rewrite H1; apply RList_P7; assumption ] ].
-induction  l1 as [| r l1 Hrecl1].
-simpl in |- *; simpl in H1; right; assumption.
-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)) in |- *;
-    elim (RList_P3 (cons r l1) (pos_Rl (cons r l1) (Rlength l1))); 
-    intros; apply H5; exists (Rlength l1); split;
-    [ reflexivity | simpl in |- *; 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 in |- *; apply lt_n_Sn ] ] ].
+      intros; apply H3; exists (pred (Rlength (cons_ORlist (cons r l1) l2)));
+        split; [ reflexivity | rewrite RList_P11; simpl in |- *; 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 ] ].
+  induction  l1 as [| r l1 Hrecl1].
+  simpl in |- *; simpl in H1; right; assumption.
+  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)) in |- *;
+          elim (RList_P3 (cons r l1) (pos_Rl (cons r l1) (Rlength l1))); 
+            intros; apply H5; exists (Rlength l1); split;
+              [ reflexivity | simpl in |- *; 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 in |- *; 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.
-simple induction l1.
-intros; elim H0.
-intros; induction  i as [| i Hreci].
-simpl in |- *; elim H1; intro;
- [ simpl in H2; rewrite H4 in H2; elim (Rlt_irrefl _ H2)
- | apply RList_P5; [ apply RList_P4 with r; assumption | assumption ] ].
-simpl in |- *; simpl in H2; elim H1; intro.
-rewrite H4 in H2; assert (H5 : r <= pos_Rl r0 i);
- [ apply Rle_trans with (pos_Rl r0 0);
-    [ apply (H0 0%nat); simpl in |- *; simpl in H3; apply neq_O_lt;
-       red in |- *; 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)) ].
-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 in |- *; intro;
-       rewrite <- H5 in H3; elim (lt_n_O _ H3) ] ].
+  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.
+Proof.
+  simple induction l1.
+  intros; elim H0.
+  intros; induction  i as [| i Hreci].
+  simpl in |- *; elim H1; intro;
+    [ simpl in H2; rewrite H4 in H2; elim (Rlt_irrefl _ H2)
+      | apply RList_P5; [ apply RList_P4 with r; assumption | assumption ] ].
+  simpl in |- *; simpl in H2; elim H1; intro.
+  rewrite H4 in H2; assert (H5 : r <= pos_Rl r0 i);
+    [ apply Rle_trans with (pos_Rl r0 0);
+      [ apply (H0 0%nat); simpl in |- *; simpl in H3; apply neq_O_lt;
+        red in |- *; 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)) ].
+  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 in |- *; 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.
-simple induction l; intros;
- [ reflexivity | simpl in |- *; rewrite H; reflexivity ].
+  forall (l:Rlist) (f:R -> R), Rlength (app_Rlist l f) = Rlength l.
+Proof.
+  simple induction l; intros;
+    [ reflexivity | simpl in |- *; rewrite H; reflexivity ].
 Qed.
 
 Lemma RList_P19 :
- forall l:Rlist,
-   l <> nil ->  exists r : R, (exists r0 : Rlist, l = cons r r0).
-intros; induction  l as [| r l Hrecl];
- [ elim H; reflexivity | exists r; exists l; reflexivity ].
+  forall l:Rlist,
+    l <> nil ->  exists r : R, (exists r0 : Rlist, l = cons r r0).
+Proof.
+  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 ->
+  forall l:Rlist,
+    (2 <= Rlength l)%nat ->
     exists r : R,
-     (exists r1 : R, (exists 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 ] ].
+      (exists r1 : R, (exists l' : Rlist, l = cons r (cons r1 l'))). 
+Proof.
+  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'.
-intros; rewrite H; reflexivity.
+Proof.
+  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.
-simple induction l1; [ intros; elim H; reflexivity | intros; reflexivity ].
+  forall l1 l2:Rlist, l1 <> nil -> pos_Rl (cons_Rlist l1 l2) 0 = pos_Rl l1 0.
+Proof.
+  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.
-simple induction l1;
- [ intro; reflexivity | intros; simpl in |- *; rewrite H; reflexivity ].
+  forall l1 l2:Rlist,
+    Rlength (cons_Rlist l1 l2) = (Rlength l1 + Rlength l2)%nat.
+Proof.
+  simple induction l1;
+    [ intro; reflexivity | intros; simpl in |- *; 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)).
-simple induction l1.
-intros; reflexivity.
-intros; rewrite <- (H l2 H0); induction  l2 as [| r1 l2 Hrecl2].
-elim H0; reflexivity.
-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 in |- *; apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR;
-       rewrite S_INR; ring ]
- | simpl in |- *; apply INR_eq; do 3 rewrite S_INR; do 2 rewrite plus_INR;
-    rewrite S_INR; ring ].
+  forall l1 l2:Rlist,
+    l2 <> nil ->
+    pos_Rl (cons_Rlist l1 l2) (pred (Rlength (cons_Rlist l1 l2))) =
+    pos_Rl l2 (pred (Rlength l2)).
+Proof.
+  simple induction l1.
+  intros; reflexivity.
+  intros; rewrite <- (H l2 H0); induction  l2 as [| r1 l2 Hrecl2].
+  elim H0; reflexivity.
+  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 in |- *; apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR;
+          rewrite S_INR; ring ]
+      | simpl in |- *; 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).
-simple induction l1.
-intros; simpl in |- *; assumption.
-simple induction r0.
-intros; simpl in |- *; simpl in H2; unfold ordered_Rlist in |- *; intros;
- simpl in H3.
-induction  i as [| i Hreci].
-simpl in |- *; assumption.
-change (pos_Rl l2 i <= pos_Rl l2 (S i)) in |- *; 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 in |- *; intro;
-    rewrite <- H4 in H3; elim (lt_n_O _ H3) ].
-intros; clear H; assert (H : ordered_Rlist (cons_Rlist (cons r1 r2) l2)).
-apply H0; try assumption.
-apply RList_P4 with r; assumption.
-unfold ordered_Rlist in |- *; intros; simpl in H4;
- induction  i as [| i Hreci].
-simpl in |- *; apply (H1 0%nat); simpl in |- *; apply lt_O_Sn.
-change
-  (pos_Rl (cons_Rlist (cons r1 r2) l2) i <=
-   pos_Rl (cons_Rlist (cons r1 r2) l2) (S i)) in |- *; 
- apply (H i); simpl in |- *; apply lt_S_n; assumption.
+  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).
+Proof.
+  simple induction l1.
+  intros; simpl in |- *; assumption.
+  simple induction r0.
+  intros; simpl in |- *; simpl in H2; unfold ordered_Rlist in |- *; intros;
+    simpl in H3.
+  induction  i as [| i Hreci].
+  simpl in |- *; assumption.
+  change (pos_Rl l2 i <= pos_Rl l2 (S i)) in |- *; 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 in |- *; intro;
+        rewrite <- H4 in H3; elim (lt_n_O _ H3) ].
+  intros; clear H; assert (H : ordered_Rlist (cons_Rlist (cons r1 r2) l2)).
+  apply H0; try assumption.
+  apply RList_P4 with r; assumption.
+  unfold ordered_Rlist in |- *; intros; simpl in H4;
+    induction  i as [| i Hreci].
+  simpl in |- *; apply (H1 0%nat); simpl in |- *; apply lt_O_Sn.
+  change
+    (pos_Rl (cons_Rlist (cons r1 r2) l2) i <=
+      pos_Rl (cons_Rlist (cons r1 r2) l2) (S i)) in |- *; 
+    apply (H i); simpl in |- *; 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.
-simple induction l1.
-intros; elim (lt_n_O _ H).
-intros; induction  i as [| i Hreci].
-apply RList_P22; discriminate.
-apply (H l2 i); simpl in H0; apply lt_S_n; assumption.
+  forall (l1 l2:Rlist) (i:nat),
+    (i < Rlength l1)%nat -> pos_Rl (cons_Rlist l1 l2) i = pos_Rl l1 i.
+Proof.
+  simple induction l1.
+  intros; elim (lt_n_O _ H).
+  intros; induction  i as [| i Hreci].
+  apply RList_P22; discriminate.
+  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.
-simple induction l1; intros;
- [ reflexivity | simpl in |- *; rewrite (H l2 l3); reflexivity ].
+  forall l1 l2 l3:Rlist,
+    cons_Rlist l1 (cons_Rlist l2 l3) = cons_Rlist (cons_Rlist l1 l2) l3.
+Proof.
+  simple induction l1; intros;
+    [ reflexivity | simpl in |- *; rewrite (H l2 l3); reflexivity ].
 Qed.
 
 Lemma RList_P28 : forall l:Rlist, cons_Rlist l nil = l.
-simple induction l;
- [ reflexivity | intros; simpl in |- *; rewrite H; reflexivity ].
+Proof.
+  simple induction l;
+    [ reflexivity | intros; simpl in |- *; 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).
-simple induction l2.
-intros; rewrite RList_P28 in H0; elim (lt_irrefl _ (le_lt_trans _ _ _ H H0)).
-intros;
- replace (cons_Rlist l1 (cons r r0)) with
-  (cons_Rlist (cons_Rlist l1 (cons r nil)) r0).
-inversion H0.
-rewrite <- minus_n_n; simpl in |- *; rewrite RList_P26.
-clear l2 r0 H i H0 H1 H2; induction  l1 as [| r0 l1 Hrecl1].
-reflexivity.
-simpl in |- *; assumption.
-rewrite RList_P23; rewrite plus_comm; simpl in |- *; apply lt_n_Sn.
-replace (S m - Rlength l1)%nat with (S (S m - S (Rlength l1))).
-rewrite H3; simpl in |- *;
- replace (S (Rlength l1)) with (Rlength (cons_Rlist l1 (cons r nil))).
-apply (H (cons_Rlist l1 (cons r nil)) i).
-rewrite RList_P23; rewrite plus_comm; simpl in |- *; rewrite <- H3;
- apply le_n_S; assumption.
-repeat rewrite RList_P23; simpl in |- *; rewrite RList_P23 in H1;
- rewrite plus_comm in H1; simpl in H1; rewrite (plus_comm (Rlength l1));
- simpl in |- *; rewrite plus_comm; apply H1.
-rewrite RList_P23; rewrite plus_comm; reflexivity.
-change (S (m - Rlength l1) = (S m - Rlength l1)%nat) in |- *;
- apply minus_Sn_m; assumption.
-replace (cons r r0) with (cons_Rlist (cons r nil) r0);
- [ symmetry  in |- *; apply RList_P27 | reflexivity ].
+  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.
+  simple induction l2.
+  intros; rewrite RList_P28 in H0; elim (lt_irrefl _ (le_lt_trans _ _ _ H H0)).
+  intros;
+    replace (cons_Rlist l1 (cons r r0)) with
+    (cons_Rlist (cons_Rlist l1 (cons r nil)) r0).
+  inversion H0.
+  rewrite <- minus_n_n; simpl in |- *; rewrite RList_P26.
+  clear l2 r0 H i H0 H1 H2; induction  l1 as [| r0 l1 Hrecl1].
+  reflexivity.
+  simpl in |- *; assumption.
+  rewrite RList_P23; rewrite plus_comm; simpl in |- *; apply lt_n_Sn.
+  replace (S m - Rlength l1)%nat with (S (S m - S (Rlength l1))).
+  rewrite H3; simpl in |- *;
+    replace (S (Rlength l1)) with (Rlength (cons_Rlist l1 (cons r nil))).
+  apply (H (cons_Rlist l1 (cons r nil)) i).
+  rewrite RList_P23; rewrite plus_comm; simpl in |- *; rewrite <- H3;
+    apply le_n_S; assumption.
+  repeat rewrite RList_P23; simpl in |- *; rewrite RList_P23 in H1;
+    rewrite plus_comm in H1; simpl in H1; rewrite (plus_comm (Rlength l1));
+      simpl in |- *; rewrite plus_comm; apply H1.
+  rewrite RList_P23; rewrite plus_comm; reflexivity.
+  change (S (m - Rlength l1) = (S m - Rlength l1)%nat) in |- *;
+    apply minus_Sn_m; assumption.
+  replace (cons r r0) with (cons_Rlist (cons r nil) r0);
+  [ symmetry  in |- *; apply RList_P27 | reflexivity ].
 Qed.