Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 731 insertions, 414 deletions

diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index 6e6f2716b..40848009a 100644
--- a/theories/Reals/RList.v
+++ b/theories/Reals/RList.v
@@ -8,420 +8,737 @@
  
 (*i $Id$ i*)
 
-Require Rbase.
-Require Rfunctions.
-V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Require Import Rbase.
+Require Import Rfunctions.
 Open Local Scope R_scope.
 
 Inductive Rlist : Type :=
-| nil : Rlist
-| cons : R -> Rlist -> Rlist.
-
-Fixpoint In [x:R;l:Rlist] : Prop :=
-Cases l of
-| nil => False
-| (cons a l') => ``x==a``\/(In x l') end.
-
-Fixpoint Rlength [l:Rlist] : nat :=
-Cases l of
-| nil => O
-| (cons a l') => (S (Rlength l')) end.
-
-Fixpoint MaxRlist [l:Rlist] : R :=
- Cases l of
- | nil => R0
- | (cons a l1) => 
-   Cases l1 of
-   | nil => a
-   | (cons a' l2) => (Rmax a (MaxRlist l1)) 
-   end
-end.
-
-Fixpoint MinRlist [l:Rlist] : R :=
-Cases l of
- | nil => R1 
- | (cons a l1) => 
-   Cases l1 of
-   | nil => a
-   | (cons a' l2) => (Rmin a (MinRlist l1)) 
-   end
-end.
-
-Lemma MaxRlist_P1 : (l:Rlist;x:R) (In x l)->``x<=(MaxRlist l)``.
-Intros; Induction l.
-Simpl in H; Elim H.
-Induction l.
-Simpl in H; Elim H; Intro.
-Simpl; 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; Case (total_order_Rle r (MaxRlist (cons r0 l))); Intro.
-Apply Hrecl; Simpl; Tauto.
-Apply Rle_trans with (MaxRlist (cons r0 l)); [Apply Hrecl; Simpl; Tauto | Left; Auto with real].
-Unfold Rmax; Case (total_order_Rle r (MaxRlist (cons r0 l))); Intro.
-Apply Hrecl; Simpl; Tauto.
-Apply Rle_trans with (MaxRlist (cons r0 l)); [Apply Hrecl; Simpl; Tauto | Left; Auto with real].
-Reflexivity.
-Qed.
-
-Fixpoint AbsList [l:Rlist] : R->Rlist :=
-[x:R] Cases l of
-| nil => nil
-| (cons a l') => (cons ``(Rabsolu (a-x))/2`` (AbsList l' x))
-end.
-
-Lemma MinRlist_P1 : (l:Rlist;x:R) (In x l)->``(MinRlist l)<=x``.
-Intros; Induction l.
-Simpl in H; Elim H.
-Induction l.
-Simpl in H; Elim H; Intro.
-Simpl; Right; Symmetry; 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; Case (total_order_Rle r (MinRlist (cons r0 l))); Intro.
-Apply Rle_trans with (MinRlist (cons r0 l)).
-Assumption.
-Apply Hrecl; Simpl; Tauto.
-Apply Hrecl; Simpl; Tauto.
-Apply Rle_trans with (MinRlist (cons r0 l)).
-Apply Rmin_r.
-Apply Hrecl; Simpl; Tauto.
-Reflexivity.
-Qed.
-
-Lemma AbsList_P1 : (l:Rlist;x,y:R) (In y l) -> (In ``(Rabsolu (y-x))/2`` (AbsList l x)).
-Intros; Induction l.
-Elim H.
-Simpl; Simpl in H; Elim H; Intro.
-Left; Rewrite H0; Reflexivity.
-Right; Apply Hrecl; Assumption.
-Qed.
-
-Lemma MinRlist_P2 : (l:Rlist) ((y:R)(In y l)->``0<y``)->``0<(MinRlist l)``.
-Intros; Induction l.
-Apply Rlt_R0_R1.
-Induction l.
-Simpl; Apply H; Simpl; Tauto.
-Replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))).
-Unfold Rmin; Case (total_order_Rle r (MinRlist (cons r0 l))); Intro.
-Apply H; Simpl; Tauto.
-Apply Hrecl; Intros; Apply H; Simpl; Simpl in H0; Tauto.
-Reflexivity.
-Qed.
-
-Lemma AbsList_P2 : (l:Rlist;x,y:R) (In y (AbsList l x)) -> (EXT z : R | (In z l)/\``y==(Rabsolu (z-x))/2``).
-Intros; Induction l.
-Elim H.
-Elim H; Intro.
-Exists r; Split.
-Simpl; Tauto.
-Assumption.
-Assert H1 := (Hrecl H0); Elim H1; Intros; Elim H2; Clear H2; Intros; Exists x0; Simpl; Simpl in H2; Tauto.
-Qed.
-
-Lemma MaxRlist_P2 : (l:Rlist) (EXT y:R | (In y l)) -> (In (MaxRlist l) l).
-Intros; Induction l.
-Simpl in H; Elim H; Trivial.
-Induction l.
-Simpl; Left; Reflexivity.
-Change (In (Rmax r (MaxRlist (cons r0 l))) (cons r (cons r0 l))); Unfold Rmax; Case (total_order_Rle r (MaxRlist (cons r0 l))); Intro.
-Right; Apply Hrecl; Exists r0; Left; Reflexivity.
-Left; Reflexivity.
-Qed.
-
-Fixpoint pos_Rl [l:Rlist] : nat->R :=
-[i:nat] Cases l of
-| nil => R0
-| (cons a l') =>
- Cases i of
- | O => a
- | (S i') => (pos_Rl l' i')
- end
-end.
-
-Lemma pos_Rl_P1 : (l:Rlist;a:R) (lt O (Rlength l)) -> (pos_Rl (cons a l) (Rlength l))==(pos_Rl l (pred (Rlength l))).
-Intros; Induction l; [Elim (lt_n_O ? H) | Simpl; Case (Rlength l); [Reflexivity | Intro; Reflexivity]].
-Qed.
-
-Lemma pos_Rl_P2 : (l:Rlist;x:R) (In x l)<->(EX i:nat | (lt i (Rlength l))/\x==(pos_Rl l i)).
-Intros; Induction l.
-Split; Intro; [Elim H | Elim H; Intros; Elim H0; Intros; Elim (lt_n_O ? H1)].
-Split; Intro.
-Elim H; Intro.
-Exists O; Split; [Simpl; Apply lt_O_Sn | Simpl; Apply H0].
-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].
-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; Apply S_pred with O; 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 : (l:Rlist;P:R->R->Prop) ((x:R)(In x l)->(EXT y:R | (P x y))) -> (EXT l':Rlist | (Rlength l)=(Rlength l')/\(i:nat) (lt i (Rlength l))->(P (pos_Rl l i) (pos_Rl l' i))).
-Intros; Induction l.
-Exists nil; Intros; Split; [Reflexivity | Intros; Simpl in H0; Elim (lt_n_O ? H0)].
-Assert H0 : (In r (cons r l)).
-Simpl; Left; Reflexivity.
-Assert H1 := (H ? H0); Assert H2 : (x:R)(In x l)->(EXT y:R | (P x y)).
-Intros; Apply H; Simpl; Right; Assumption.
-Assert H3 := (Hrecl H2); Elim H1; Intros; Elim H3; Intros; Exists (cons x x0); Intros; Elim H5; Clear H5; Intros; Split.
-Simpl; Rewrite H5; Reflexivity.
-Intros; Elim (zerop i); Intro.
-Rewrite a; Simpl; Assumption.
-Assert H8 : i=(S (pred i)).
-Apply S_pred with O; Assumption.
-Rewrite H8; Simpl; Apply H6; Simpl in H7; Apply lt_S_n; Rewrite <- H8; Assumption.
-Qed.
-
-Definition ordered_Rlist [l:Rlist] : Prop := (i:nat) (lt i (pred (Rlength l))) -> (Rle (pos_Rl l i) (pos_Rl l (S i))).
-
-Fixpoint insert [l:Rlist] : R->Rlist :=
-[x:R] Cases l of
-| nil => (cons x nil)
-| (cons a l') =>
- Cases (total_order_Rle a x) of
- | (leftT _) => (cons a (insert l' x))
- | (rightT _) => (cons x l)
- end
-end.
-
-Fixpoint cons_Rlist [l:Rlist] : Rlist->Rlist :=
-[k:Rlist] Cases l of
-| nil => k
-| (cons a l') => (cons a (cons_Rlist l' k)) end.
-
-Fixpoint cons_ORlist [k:Rlist] : Rlist->Rlist :=
-[l:Rlist] Cases k of
-| nil => l
-| (cons a k') => (cons_ORlist k' (insert l a))
-end.
-
-Fixpoint app_Rlist [l:Rlist] : (R->R)->Rlist :=
-[f:R->R] Cases l of
-| nil => nil
-| (cons a l') => (cons (f a) (app_Rlist l' f))
-end.
-
-Fixpoint mid_Rlist [l:Rlist] : R->Rlist :=
-[x:R] Cases l of
-| nil => nil
-| (cons a l') => (cons ``(x+a)/2`` (mid_Rlist l' a))
-end.
-
-Definition Rtail [l:Rlist] : Rlist :=
-Cases l of
-| nil => nil
-| (cons a l') => l'
-end.
-
-Definition FF [l:Rlist;f:R->R] : Rlist := 
-Cases l of
-| nil => nil
-| (cons a l') => (app_Rlist (mid_Rlist l' a) f)
-end.
-
-Lemma RList_P0 : (l:Rlist;a:R) ``(pos_Rl (insert l a) O) == a`` \/ ``(pos_Rl (insert l a) O) == (pos_Rl l O)``.
-Intros; Induction l; [Left; Reflexivity | Simpl; Case (total_order_Rle r a); Intro; [Right; Reflexivity | Left; Reflexivity]].
-Qed.
-
-Lemma RList_P1 : (l:Rlist;a:R) (ordered_Rlist l) -> (ordered_Rlist (insert l a)).
-Intros; Induction l.
-Simpl; Unfold ordered_Rlist; Intros; Simpl in H0; Elim (lt_n_O ? H0).
-Simpl; Case (total_order_Rle r a); Intro.
-Assert H1 : (ordered_Rlist l).
-Unfold ordered_Rlist; Unfold ordered_Rlist in H; Intros; Assert H1 : (lt (S i) (pred (Rlength (cons r l)))); [Simpl; Replace (Rlength l) with (S (pred (Rlength l))); [Apply lt_n_S; Assumption | Symmetry; Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H1 in H0; Simpl in H0; Elim (lt_n_O ? H0)] | Apply (H ? H1)].
-Assert H2 := (Hrecl H1); Unfold ordered_Rlist; Intros; Induction i.
-Simpl; Assert H3 := (RList_P0 l a); Elim H3; Intro.
-Rewrite H4; Assumption.
-Induction l; [Simpl; Assumption | Rewrite H4; Apply (H O); Simpl; Apply lt_O_Sn].
-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 O; Apply neq_O_lt; Red; Intro; Rewrite <- H3 in H0; Elim (lt_n_O ? H0)].
-Unfold ordered_Rlist; Intros; Induction i; [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 : (l1,l2:Rlist) (ordered_Rlist l2) ->(ordered_Rlist (cons_ORlist l1 l2)).
-Induction l1; [Intros; Simpl; Apply H | Intros; Simpl; Apply H; Apply RList_P1; Assumption].
-Qed.
-
-Lemma RList_P3 : (l:Rlist;x:R) (In x l) <-> (EX i:nat | x==(pos_Rl l i)/\(lt i (Rlength l))).
-Intros; Split; Intro; Induction l.
-Elim H.
-Elim H; Intro; [Exists O; 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]].
-Elim H; Intros; Elim H0; Intros; Elim (lt_n_O ? H2).
-Simpl; Elim H; Intros; Elim H0; Clear H0; Intros; Induction x0; [Left; Apply H0 | Right; Apply Hrecl; Exists x0; Split; [Apply H0 | Simpl in H1; Apply lt_S_n; Assumption]].
-Qed.
-
-Lemma RList_P4 : (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 O; Apply neq_O_lt; Red; Intro; Rewrite <- H1 in H0; Elim (lt_n_O ? H0)].
-Qed.
-
-Lemma RList_P5 : (l:Rlist;x:R) (ordered_Rlist l) -> (In x l) -> ``(pos_Rl l O)<=x``.
-Intros; Induction l; [Elim H0 | Simpl; Elim H0; Intro; [Rewrite H1; Right; Reflexivity | Apply Rle_trans with (pos_Rl l O); [Apply (H O); Simpl; Induction l; [Elim H1 | Simpl; Apply lt_O_Sn] | Apply Hrecl; [EApply RList_P4; Apply H | Assumption]]]].
-Qed.
-
-Lemma RList_P6 : (l:Rlist) (ordered_Rlist l)<->((i,j:nat)(le i j)->(lt j (Rlength l))->``(pos_Rl l i)<=(pos_Rl l j)``).
-Induction l; Split; Intro.
-Intros; Right; Reflexivity.
-Unfold ordered_Rlist; Intros; Simpl in H0; Elim (lt_n_O ? H0).
-Intros; Induction i; [Induction j; [Right; Reflexivity | Simpl; Apply Rle_trans with (pos_Rl r0 O); [Apply (H0 O); 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; [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]]].
-Unfold ordered_Rlist; Intros; Apply H0; [Apply le_n_Sn | Simpl; Simpl in H1; Apply lt_n_S; Assumption].
-Qed.
-
-Lemma RList_P7 : (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 O; Apply neq_O_lt; Red; 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; Intro; Rewrite <- H7 in H5; Elim (lt_n_O ? H5)].
-Qed.
-
-Lemma RList_P8 : (l:Rlist;a,x:R) (In x (insert l a)) <-> x==a\/(In x l).
-Induction l.
-Intros; Split; Intro; Simpl in H; Apply H.
-Intros; Split; Intro; [Simpl in H0; Generalize H0; Case (total_order_Rle 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 (total_order_Rle 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 : (l1,l2:Rlist;x:R) (In x (cons_ORlist l1 l2)) <-> (In x l1)\/(In x l2).
-Induction l1.
-Intros; Split; Intro; [Simpl in H; Right; Assumption | Simpl; Elim H; Intro; [Elim H0 | Assumption]].
-Intros; Split.
-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]].
-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 : (l:Rlist;a:R) (Rlength (insert l a))==(S (Rlength l)).
-Intros; Induction l; [Reflexivity | Simpl; Case (total_order_Rle r a); Intro; [Simpl; Rewrite Hrecl; Reflexivity | Reflexivity]].
-Qed.
-
-Lemma RList_P11 : (l1,l2:Rlist) (Rlength (cons_ORlist l1 l2))=(plus (Rlength l1) (Rlength l2)).
-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 : (l:Rlist;i:nat;f:R->R) (lt i (Rlength l)) -> (pos_Rl (app_Rlist l f) i)==(f (pos_Rl l i)).
-Induction l; [Intros; Elim (lt_n_O ? H) | Intros; Induction i; [Reflexivity | Simpl; Apply H; Apply lt_S_n; Apply H0]].
-Qed.
-
-Lemma RList_P13 : (l:Rlist;i:nat;a:R) (lt i (pred (Rlength l))) -> ``(pos_Rl (mid_Rlist l a) (S i)) == ((pos_Rl l i)+(pos_Rl l (S i)))/2``.
-Induction l.
-Intros; Simpl in H; Elim (lt_n_O ? H).
-Induction r0.
-Intros; Simpl in H0; Elim (lt_n_O ? H0).
-Intros; Simpl in H1; Induction i.
-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``; Apply H0; Simpl; Apply lt_S_n; Assumption.
-Qed.
-
-Lemma RList_P14 : (l:Rlist;a:R) (Rlength (mid_Rlist l a))=(Rlength l).
-Induction l; Intros; [Reflexivity | Simpl; Rewrite (H r); Reflexivity].
-Qed.
-
-Lemma RList_P15 : (l1,l2:Rlist) (ordered_Rlist l1) -> (ordered_Rlist l2) -> (pos_Rl l1 O)==(pos_Rl l2 O) -> (pos_Rl (cons_ORlist l1 l2) O)==(pos_Rl l1 O).
-Intros; Apply Rle_antisym.
-Induction l1; [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]]].
-Induction l1; [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 O; 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 : (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.
-Simpl; Simpl in H1; Right; Symmetry; 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; 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.
-Simpl; 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)); 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 : (l1:Rlist;x:R;i:nat) (ordered_Rlist l1) -> (In x l1) -> ``(pos_Rl l1 i)<x`` -> (lt i (pred (Rlength l1))) -> ``(pos_Rl l1 (S i))<=x``.
-Induction l1.
-Intros; Elim H0.
-Intros; Induction i.
-Simpl; Elim H1; Intro; [Simpl in H2; Rewrite H4 in H2; Elim (Rlt_antirefl ? H2) | Apply RList_P5; [Apply RList_P4 with r; Assumption | Assumption]].
-Simpl; Simpl in H2; Elim H1; Intro.
-Rewrite H4 in H2; Assert H5 : ``r<=(pos_Rl r0 i)``; [Apply Rle_trans with (pos_Rl r0 O); [Apply (H0 O); 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_antirefl ? (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 O; Apply neq_O_lt; Red; Intro; Rewrite <- H5 in H3; Elim (lt_n_O ? H3)]].
-Qed.
-
-Lemma RList_P18 : (l:Rlist;f:R->R) (Rlength (app_Rlist l f))=(Rlength l).
-Induction l; Intros; [Reflexivity | Simpl; Rewrite H; Reflexivity].
-Qed.
-
-Lemma RList_P19 : (l:Rlist) ~l==nil -> (EXT r:R | (EXT r0:Rlist | l==(cons r r0))).
-Intros; Induction l; [Elim H; Reflexivity | Exists r; Exists l; Reflexivity].
-Qed.
-
-Lemma RList_P20 : (l:Rlist) (le (2) (Rlength l)) -> (EXT r:R | (EXT r1:R | (EXT l':Rlist | l==(cons r (cons r1 l'))))). 
-Intros; Induction l; [Simpl in H; Elim (le_Sn_O ? H) | Induction l; [Simpl in H; Elim (le_Sn_O ? (le_S_n ? ? H)) | Exists r; Exists r0; Exists l; Reflexivity]].
-Qed.
-
-Lemma RList_P21 : (l,l':Rlist) l==l' -> (Rtail l)==(Rtail l').
-Intros; Rewrite H; Reflexivity.
-Qed.
-
-Lemma RList_P22 : (l1,l2:Rlist) ~l1==nil -> (pos_Rl (cons_Rlist l1 l2) O)==(pos_Rl l1 O).
-Induction l1; [Intros; Elim H; Reflexivity | Intros; Reflexivity].
-Qed.
-
-Lemma RList_P23 : (l1,l2:Rlist) (Rlength (cons_Rlist l1 l2))==(plus (Rlength l1) (Rlength l2)).
-Induction l1; [Intro; Reflexivity | Intros; Simpl; Rewrite H; Reflexivity].
-Qed.
-
-Lemma RList_P24 : (l1,l2:Rlist) ~l2==nil -> (pos_Rl (cons_Rlist l1 l2) (pred (Rlength (cons_Rlist l1 l2)))) == (pos_Rl l2 (pred (Rlength l2))).
-Induction l1.
-Intros; Reflexivity.
-Intros; Rewrite <- (H l2 H0); Induction l2.
-Elim H0; Reflexivity.
-Do 2 Rewrite RList_P23; Replace (plus (Rlength (cons r r0)) (Rlength (cons r1 l2))) with (S (S (plus (Rlength r0) (Rlength l2)))); [Replace (plus (Rlength r0) (Rlength (cons r1 l2))) with (S (plus (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 : (l1,l2:Rlist) (ordered_Rlist l1) -> (ordered_Rlist l2) -> ``(pos_Rl l1 (pred (Rlength l1)))<=(pos_Rl l2 O)`` -> (ordered_Rlist (cons_Rlist l1 l2)).
-Induction l1.
-Intros; Simpl; Assumption.
-Induction r0.
-Intros; Simpl; Simpl in H2; Unfold ordered_Rlist; Intros; Simpl in H3.
-Induction i.
-Simpl; Assumption.
-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 O; Apply neq_O_lt; Red; 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; Intros; Simpl in H4; Induction i.
-Simpl; Apply (H1 O); Simpl; Apply lt_O_Sn.
-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 : (l1,l2:Rlist;i:nat) (lt i (Rlength l1)) -> (pos_Rl (cons_Rlist l1 l2) i)==(pos_Rl l1 i).
-Induction l1.
-Intros; Elim (lt_n_O ? H).
-Intros; Induction i.
-Apply RList_P22; Discriminate.
-Apply (H l2 i); Simpl in H0; Apply lt_S_n; Assumption.
-Qed.
-
-Lemma RList_P27 : (l1,l2,l3:Rlist) (cons_Rlist l1 (cons_Rlist l2 l3))==(cons_Rlist (cons_Rlist l1 l2) l3).
-Induction l1; Intros; [Reflexivity | Simpl; Rewrite (H l2 l3); Reflexivity].
-Qed.
-
-Lemma RList_P28 : (l:Rlist) (cons_Rlist l nil)==l.
-Induction l; [Reflexivity | Intros; Simpl; Rewrite H; Reflexivity].
-Qed.
-
-Lemma RList_P29 : (l2,l1:Rlist;i:nat) (le (Rlength l1) i) -> (lt i (Rlength (cons_Rlist l1 l2))) -> (pos_Rl (cons_Rlist l1 l2) i)==(pos_Rl l2 (minus i (Rlength l1))).
-Induction l2.
-Intros; Rewrite RList_P28 in H0; Elim (lt_n_n ? (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; Rewrite RList_P26.
-Clear l2 r0 H i H0 H1 H2; Induction l1.
-Reflexivity.
-Simpl; Assumption.
-Rewrite RList_P23; Rewrite plus_sym; Simpl; Apply lt_n_Sn.
-Replace (minus (S m) (Rlength l1)) with (S (minus (S m) (S (Rlength l1)))).
-Rewrite H3; Simpl; 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_sym; Simpl; Rewrite <- H3; Apply le_n_S; Assumption.
-Repeat Rewrite RList_P23; Simpl; Rewrite RList_P23 in H1; Rewrite plus_sym in H1; Simpl in H1; Rewrite (plus_sym (Rlength l1)); Simpl; Rewrite plus_sym; Apply H1.
-Rewrite RList_P23; Rewrite plus_sym; Reflexivity.
-Change (S (minus m (Rlength l1)))=(minus (S m) (Rlength l1)); Apply minus_Sn_m; Assumption.
-Replace (cons r r0) with (cons_Rlist (cons r nil) r0); [Symmetry; Apply RList_P27 | Reflexivity].
-Qed.
+  | 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'
+  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.
+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)
+  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.
+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.
+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.
+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.
+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.
+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
+  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 ] ].
+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 ].
+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)).
+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 :=
+  forall i:nat, (i < pred (Rlength l))%nat -> pos_Rl l i <= pos_Rl l (S i).
+
+Fixpoint insert (l:Rlist) (x:R) {struct l} : 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) {struct l} : Rlist :=
+  match l with
+  | 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)
+  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)
+  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)
+  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.
+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) ].
+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 ].
+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 ] ].
+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) ].
+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 ] ] ] ].
+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).
+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) ].
+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 ].
+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 ].
+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 ] ].
+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 ].
+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 ] ].
+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.
+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 ].
+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 ] ] ].
+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)
+          (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) ] ].
+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 ].
+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 ].
+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'))). 
+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.
+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 ].
+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 ].
+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 ].
+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.
+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.
+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 ].
+Qed.
+
+Lemma RList_P28 : forall l:Rlist, cons_Rlist l nil = l.
+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 ].
+Qed.
\ No newline at end of file