Renommages dans RList

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

1 files changed, 40 insertions, 41 deletions

diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index 7f8a92d08..82c920621 100644
--- a/theories/Reals/RList.v
+++ b/theories/Reals/RList.v
@@ -20,15 +20,14 @@ Cases l of
 | nil => False
 | (cons a l') => ``x==a``\/(In x l') end.
 
-Fixpoint longueur [l:Rlist] : nat :=
+Fixpoint Rlength [l:Rlist] : nat :=
 Cases l of
 | nil => O
-| (cons a l') => (S (longueur l')) end.
+| (cons a l') => (S (Rlength l')) end.
 
-(* Cette fonction renvoie le maximum des éléments d'une liste non vide *)
 Fixpoint MaxRlist [l:Rlist] : R :=
  Cases l of
- | nil => R0 (* valeur de retour si la liste de départ est vide *)
+ | nil => R0
  | (cons a l1) => 
    Cases l1 of
    | nil => a
@@ -38,7 +37,7 @@ end.
 
 Fixpoint MinRlist [l:Rlist] : R :=
 Cases l of
- | nil => R1 (* valeur de retour si la liste de départ est vide *)
+ | nil => R1 
  | (cons a l1) => 
    Cases l1 of
    | nil => a
@@ -142,11 +141,11 @@ Fixpoint pos_Rl [l:Rlist] : nat->R :=
  end
 end.
 
-Lemma pos_Rl_P1 : (l:Rlist;a:R) (lt O (longueur l)) -> (pos_Rl (cons a l) (longueur l))==(pos_Rl l (pred (longueur l))).
-Intros; Induction l; [Elim (lt_n_O ? H) | Simpl; Case (longueur l); [Reflexivity | Intro; Reflexivity]].
+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 (longueur l))/\x==(pos_Rl l i)).
+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.
@@ -160,7 +159,7 @@ 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 | (longueur l)=(longueur l')/\(i:nat) (lt i (longueur l))->(P (pos_Rl l i) (pos_Rl l' i))).
+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)).
@@ -176,7 +175,7 @@ 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 (longueur l))) -> (Rle (pos_Rl l i) (pos_Rl l (S i))).
+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
@@ -232,12 +231,12 @@ 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 (longueur (cons r l)))); [Simpl; Replace (longueur l) with (S (pred (longueur 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)].
+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 (longueur (insert l a)))) with (longueur (insert l a)); [Assumption | Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H3 in H0; Elim (lt_n_O ? H0)].
+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.
 
@@ -245,7 +244,7 @@ Lemma RList_P2 : (l1,l2:Rlist) (ordered_Rlist l2) ->(ordered_Rlist (cons_ORlist
 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 (longueur l))).
+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]].
@@ -254,14 +253,14 @@ Simpl; Elim H; Intros; Elim H0; Clear H0; Intros; Induction x0; [Left; Apply H0
 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 (longueur l1) with (S (pred (longueur 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)].
+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 (longueur l))->``(pos_Rl l i)<=(pos_Rl l j)``).
+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).
@@ -269,8 +268,8 @@ Intros; Induction i; [Induction j; [Right; Reflexivity | Simpl; Apply Rle_trans
 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 (longueur 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 : (longueur l)=(S (pred (longueur l))).
+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.
@@ -289,19 +288,19 @@ Simpl; Intros; Elim (H (insert l2 r) x); Intros; Assert H3 := (H1 H0); Elim H3;
 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) (longueur (insert l a))==(S (longueur l)).
+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) (longueur (cons_ORlist l1 l2))=(plus (longueur l1) (longueur l2)).
+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 (longueur l)) -> (pos_Rl (app_Rlist l f) i)==(f (pos_Rl l i)).
+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 (longueur l))) -> ``(pos_Rl (mid_Rlist l a) (S i)) == ((pos_Rl l i)+(pos_Rl l (S i)))/2``.
+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.
@@ -311,7 +310,7 @@ 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) (longueur (mid_Rlist l a))=(longueur l).
+Lemma RList_P14 : (l:Rlist;a:R) (Rlength (mid_Rlist l a))=(Rlength l).
 Induction l; Intros; [Reflexivity | Simpl; Rewrite (H r); Reflexivity].
 Qed.
 
@@ -321,27 +320,27 @@ Induction l1; [Simpl; Simpl in H1; Right; Symmetry; Assumption | Elim (RList_P9
 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 (longueur l1)))==(pos_Rl l2 (pred (longueur l2))) -> (pos_Rl (cons_ORlist l1 l2) (pred (longueur (cons_ORlist l1 l2))))==(pos_Rl l1 (pred (longueur l1))).
+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 (longueur (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 (longueur (cons_ORlist (cons r l1) l2))))); Intros; Apply H3; Exists (pred (longueur (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 (longueur (cons_ORlist (cons r l1) l2))))); Intros; Assert H5 := (H3 H2); Elim H5; Intro; [Apply RList_P7; Assumption | Rewrite H1; Apply RList_P7; 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 (longueur (cons r l1))))); Intros; Assert H4 : (In (pos_Rl (cons r l1) (pred (longueur (cons r l1)))) (cons r l1))\/(In (pos_Rl (cons r l1) (pred (longueur (cons r l1)))) l2); [Left; Change (In (pos_Rl (cons r l1) (longueur l1)) (cons r l1)); Elim (RList_P3 (cons r l1) (pos_Rl (cons r l1) (longueur l1))); Intros; Apply H5; Exists (longueur 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 (longueur (cons r l1))))); Intros; Apply H7; Left; Elim (RList_P3 (cons r l1) (pos_Rl (cons r l1) (pred (longueur (cons r l1))))); Intros; Apply H9; Exists (pred (longueur (cons r l1))); Split; [Reflexivity | Simpl; Apply lt_n_Sn]]].
+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 (longueur l1))) -> ``(pos_Rl l1 (S i))<=x``.
+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 (longueur 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 (longueur r0))) with (longueur r0); [Apply H3 | Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H5 in H3; Elim (lt_n_O ? H3)]].
+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) (longueur (app_Rlist l f))=(longueur l).
+Lemma RList_P18 : (l:Rlist;f:R->R) (Rlength (app_Rlist l f))=(Rlength l).
 Induction l; Intros; [Reflexivity | Simpl; Rewrite H; Reflexivity].
 Qed.
 
@@ -349,7 +348,7 @@ 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) (longueur l)) -> (EXT r:R | (EXT r1:R | (EXT l':Rlist | l==(cons r (cons r1 l'))))). 
+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.
 
@@ -361,26 +360,26 @@ Lemma RList_P22 : (l1,l2:Rlist) ~l1==nil -> (pos_Rl (cons_Rlist l1 l2) O)==(pos_
 Induction l1; [Intros; Elim H; Reflexivity | Intros; Reflexivity].
 Qed.
 
-Lemma RList_P23 : (l1,l2:Rlist) (longueur (cons_Rlist l1 l2))==(plus (longueur l1) (longueur l2)).
+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 (longueur (cons_Rlist l1 l2)))) == (pos_Rl l2 (pred (longueur l2))).
+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 (longueur (cons r r0)) (longueur (cons r1 l2))) with (S (S (plus (longueur r0) (longueur l2)))); [Replace (plus (longueur r0) (longueur (cons r1 l2))) with (S (plus (longueur r0) (longueur 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].
+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 (longueur l1)))<=(pos_Rl l2 O)`` -> (ordered_Rlist (cons_Rlist l1 l2)).
+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 (longueur l2))) with (longueur l2); [Assumption | Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H4 in H3; Elim (lt_n_O ? H3)].
+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.
@@ -389,7 +388,7 @@ 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 (longueur l1)) -> (pos_Rl (cons_Rlist l1 l2) i)==(pos_Rl l1 i).
+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.
@@ -405,7 +404,7 @@ 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 (longueur l1) i) -> (lt i (longueur (cons_Rlist l1 l2))) -> (pos_Rl (cons_Rlist l1 l2) i)==(pos_Rl l2 (minus i (longueur l1))).
+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).
@@ -415,12 +414,12 @@ 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) (longueur l1)) with (S (minus (S m) (S (longueur l1)))).
-Rewrite H3; Simpl; Replace (S (longueur l1)) with (longueur (cons_Rlist l1 (cons r nil))).
+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 (longueur l1)); Simpl; Rewrite plus_sym; Apply H1.
+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 (longueur l1)))=(minus (S m) (longueur l1)); Apply minus_Sn_m; Assumption.
+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.