Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase et Pcompare_antisym

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

3 files changed, 709 insertions, 680 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index e11194a5d..53d78d3b7 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -196,6 +196,8 @@ Qed.
 
 (** Properties of comparison *)
 
+Require Pcompare.
+
 Theorem Ncompare_Eq_eq : (n,m:entier) (Ncompare n m) = EGAL -> n = m.
 Proof.
 NewDestruct n as [|n]; NewDestruct m as [|m]; Simpl; Intro H;
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index d22a5ca49..14aa0dec1 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -11,7 +11,7 @@
 (**********************************************************************)
 (** Binary positive numbers *)
 
-(** Original version by Pierre Crégut, CNET, Lannion, France *)
+(** Original development by Pierre Crégut, CNET, Lannion, France *)
 
 Inductive positive : Set :=
   xI : positive -> positive
@@ -205,83 +205,6 @@ Fixpoint compare [x,y:positive]: relation -> relation :=
 V8Infix "?=" compare (at level 70, no associativity) : positive_scope.
 
 (**********************************************************************)
-(** Properties of comparison on binary positive numbers *)
-
-Theorem compare_convert1 : 
- (x,y:positive) 
-  ~(compare x y SUPERIEUR) = EGAL /\ ~(compare x y INFERIEUR) = EGAL.
-Proof.
-Intro x; NewInduction x as [p IHp|p IHp|]; Intro y; NewDestruct y as [q|q|];
-  Split;Simpl;Auto;
-  Discriminate Orelse (Elim (IHp q); Auto).
-Qed.
-
-Theorem compare_convert_EGAL : (x,y:positive) (compare x y EGAL) = EGAL -> x=y.
-Proof.
-Intro x; NewInduction x as [p IHp|p IHp|]; 
-  Intro y; NewDestruct y as [q|q|];Simpl;Auto; Intro H; [
-  Rewrite (IHp q); Trivial
-| Absurd (compare p q SUPERIEUR)=EGAL ;
-   [ Elim (compare_convert1 p q);Auto | Assumption ]
-| Discriminate H
-| Absurd (compare p q INFERIEUR) = EGAL; 
-    [ Elim (compare_convert1 p q);Auto | Assumption ]
-| Rewrite (IHp q);Auto 
-| Discriminate H
-| Discriminate H
-| Discriminate H ].
-Qed.
-
-Lemma ZLSI:
- (x,y:positive) (compare x y SUPERIEUR) = INFERIEUR -> 
-                (compare x y EGAL) = INFERIEUR.
-Proof.
-Intro x; Induction x;Intro y; Induction y;Simpl;Auto; 
-  Discriminate Orelse Intros H;Discriminate H.
-Qed.
-
-Lemma ZLIS:
- (x,y:positive) (compare x y INFERIEUR) = SUPERIEUR -> 
-                (compare x y EGAL) = SUPERIEUR.
-Proof.
-Intro x; Induction x;Intro y; Induction y;Simpl;Auto; 
-  Discriminate Orelse Intros H;Discriminate H.
-Qed.
-
-Lemma ZLII:
- (x,y:positive) (compare x y INFERIEUR) = INFERIEUR ->
-                (compare x y EGAL) = INFERIEUR \/ x = y.
-Proof.
-(Intro x; NewInduction x as [p IHp|p IHp|];
- Intro y; NewDestruct y as [q|q|];Simpl;Auto;Try Discriminate);
- Intro H2; Elim (IHp q H2);Auto; Intros E;Rewrite E;
- Auto.
-Qed.
-
-Lemma ZLSS:
- (x,y:positive) (compare x y SUPERIEUR) = SUPERIEUR ->
-                (compare x y EGAL) = SUPERIEUR \/ x = y.
-Proof.
-(Intro x; NewInduction x as [p IHp|p IHp|];
- Intro y; NewDestruct y as [q|q|];Simpl;Auto;Try Discriminate);
- Intro H2; Elim (IHp q H2);Auto; Intros E;Rewrite E;
- Auto.
-Qed.
-
-Lemma Dcompare : (r:relation) r=EGAL \/ r = INFERIEUR \/ r = SUPERIEUR.
-Proof.
-Induction r; Auto. 
-Qed.
-
-Tactic Definition ElimPcompare c1 c2:=
-  Elim (Dcompare (compare c1 c2 EGAL)); [ Idtac | 
-     Let x = FreshId "H" In Intro x; Case x; Clear x ].
-
-Theorem convert_compare_EGAL: (x:positive)(compare x x EGAL)=EGAL.
-Intro x; Induction x; Auto.
-Qed.
-
-(**********************************************************************)
 (** Miscellaneous properties of binary positive numbers *)
 
 Lemma ZL11: (x:positive) (x=xH) \/ ~(x=xH).
@@ -587,7 +510,13 @@ Definition Prec : (A:Set)A->(positive->A->A)->positive->A :=
   | (xI p) => (f (plus_iter p p) (iterate_add [_]A f p p (Prec p)))
   end}.
 
-(** Test *)
+(** Peano case analysis *)
+
+Theorem Pcase : (P:(positive->Prop))
+  (P xH) ->((n:positive)(P (add_un n))) ->(n:positive)(P n).
+Proof.
+Intros; Apply Pind; Auto.
+Qed.
 
 Check
  let fact = (Prec positive xH [p;r](times (add_un p) r)) in
@@ -596,6 +525,232 @@ Check
  in ((refl_equal ? ?) :: (fact seven) = five_thousand_forty).
 
 (**********************************************************************)
+(** Properties of multiplication on binary positive numbers *)
+
+(** One is right neutral for multiplication *)
+
+Lemma times_x_1 : (x:positive) (times x xH) = x.
+Proof.
+Intro x;NewInduction x; Simpl.
+  Rewrite IHx; Reflexivity.
+  Rewrite IHx; Reflexivity.
+  Reflexivity.
+Qed.
+
+(** Right reduction properties for multiplication *)
+
+Lemma times_x_double : (x,y:positive) (times x (xO y)) = (xO (times x y)).
+Proof.
+Intros x y; NewInduction x; Simpl.
+  Rewrite IHx; Reflexivity.
+  Rewrite IHx; Reflexivity.
+  Reflexivity.
+Qed.
+
+Lemma times_x_double_plus_one :
+ (x,y:positive) (times x (xI y)) = (add x (xO (times x y))).
+Proof.
+Intros x y; NewInduction x; Simpl.
+  Rewrite IHx; Do 2 Rewrite add_assoc; Rewrite add_sym with x:=y; Reflexivity.
+  Rewrite IHx; Reflexivity.
+  Reflexivity.
+Qed.
+
+(** Commutativity of multiplication *)
+
+Theorem times_sym : (x,y:positive) (times x y) = (times y x).
+Proof.
+Intros x y; NewInduction y; Simpl.
+  Rewrite <- IHy; Apply times_x_double_plus_one.
+  Rewrite <- IHy; Apply times_x_double.
+  Apply times_x_1.
+Qed.
+
+(** Distributivity of multiplication over addition *)
+
+Theorem times_add_distr:
+  (x,y,z:positive) (times x (add y z)) = (add (times x y) (times x z)).
+Proof.
+Intros x y z; NewInduction x; Simpl.
+  Rewrite IHx; Rewrite <- add_assoc with y := (xO (times x y));
+    Rewrite -> add_assoc with x := (xO (times x y));
+    Rewrite -> add_sym with x := (xO (times x y));
+    Rewrite <- add_assoc with y := (xO (times x y));
+    Rewrite -> add_assoc with y := z; Reflexivity.
+  Rewrite IHx; Reflexivity.
+  Reflexivity.
+Qed.
+
+Theorem times_add_distr_l:
+  (x,y,z:positive) (times (add x y) z) = (add (times x z) (times y z)).
+Proof.
+Intros x y z; Do 3 Rewrite times_sym with y:=z; Apply times_add_distr.
+Qed.
+
+(** Associativity of multiplication *)
+
+Theorem times_assoc :
+  ((x,y,z:positive) (times x (times y z))= (times (times x y) z)).
+Proof.
+Intro x;NewInduction x as [x|x|]; Simpl; Intros y z.
+  Rewrite IHx; Rewrite times_add_distr_l; Reflexivity.
+  Rewrite IHx; Reflexivity.
+  Reflexivity.
+Qed.
+
+(** Parity properties of multiplication *)
+
+Lemma times_discr_xO_xI : 
+  (x,y,z:positive)(times (xI x) z)<>(times (xO y) z).
+Proof.
+Intros x y z; NewInduction z as [|z IHz|]; Try Discriminate.
+Intro H; Apply IHz; Clear IHz.
+Do 2 Rewrite times_x_double in H.
+Injection H; Clear H; Intro H; Exact H.
+Qed.
+
+Lemma times_discr_xO : (x,y:positive)(times (xO x) y)<>y.
+Proof.
+Intros x y; NewInduction y; Try Discriminate.
+Rewrite times_x_double; Injection; Assumption.
+Qed.
+
+(** Simplification properties of multiplication *)
+
+Theorem simpl_times_r : (x,y,z:positive) (times x z)=(times y z) -> x=y.
+Proof.
+Intro x;NewInduction x as [p IHp|p IHp|]; Intro y; NewDestruct y as [q|q|]; Intros z H;
+    Reflexivity Orelse Apply (f_equal positive) Orelse Apply False_ind.
+  Simpl in H; Apply IHp with (xO z); Simpl; Do 2 Rewrite times_x_double;
+    Apply simpl_add_l with 1 := H.
+  Apply times_discr_xO_xI with 1 := H.
+  Simpl in H; Rewrite add_sym in H; Apply add_no_neutral with 1 := H.
+  Symmetry in H; Apply times_discr_xO_xI with 1 := H.
+  Apply IHp with (xO z); Simpl; Do 2 Rewrite times_x_double; Assumption.
+  Apply times_discr_xO with 1:=H.
+  Simpl in H; Symmetry in H; Rewrite add_sym in H; 
+    Apply add_no_neutral with 1 := H.
+  Symmetry in H; Apply times_discr_xO with 1:=H.
+Qed.
+
+Theorem simpl_times_l : (x,y,z:positive) (times z x)=(times z y) -> x=y.
+Proof.
+Intros x y z H; Apply simpl_times_r with z:=z.
+Rewrite times_sym with x:=x; Rewrite times_sym with x:=y; Assumption.
+Qed.
+
+(**********************************************************************)
+(** Properties of comparison on binary positive numbers *)
+
+Theorem compare_convert1 : 
+ (x,y:positive) 
+  ~(compare x y SUPERIEUR) = EGAL /\ ~(compare x y INFERIEUR) = EGAL.
+Proof.
+Intro x; NewInduction x as [p IHp|p IHp|]; Intro y; NewDestruct y as [q|q|];
+  Split;Simpl;Auto;
+  Discriminate Orelse (Elim (IHp q); Auto).
+Qed.
+
+Theorem compare_convert_EGAL : (x,y:positive) (compare x y EGAL) = EGAL -> x=y.
+Proof.
+Intro x; NewInduction x as [p IHp|p IHp|]; 
+  Intro y; NewDestruct y as [q|q|];Simpl;Auto; Intro H; [
+  Rewrite (IHp q); Trivial
+| Absurd (compare p q SUPERIEUR)=EGAL ;
+   [ Elim (compare_convert1 p q);Auto | Assumption ]
+| Discriminate H
+| Absurd (compare p q INFERIEUR) = EGAL; 
+    [ Elim (compare_convert1 p q);Auto | Assumption ]
+| Rewrite (IHp q);Auto 
+| Discriminate H
+| Discriminate H
+| Discriminate H ].
+Qed.
+
+Lemma ZLSI:
+ (x,y:positive) (compare x y SUPERIEUR) = INFERIEUR -> 
+                (compare x y EGAL) = INFERIEUR.
+Proof.
+Intro x; Induction x;Intro y; Induction y;Simpl;Auto; 
+  Discriminate Orelse Intros H;Discriminate H.
+Qed.
+
+Lemma ZLIS:
+ (x,y:positive) (compare x y INFERIEUR) = SUPERIEUR -> 
+                (compare x y EGAL) = SUPERIEUR.
+Proof.
+Intro x; Induction x;Intro y; Induction y;Simpl;Auto; 
+  Discriminate Orelse Intros H;Discriminate H.
+Qed.
+
+Lemma ZLII:
+ (x,y:positive) (compare x y INFERIEUR) = INFERIEUR ->
+                (compare x y EGAL) = INFERIEUR \/ x = y.
+Proof.
+(Intro x; NewInduction x as [p IHp|p IHp|];
+ Intro y; NewDestruct y as [q|q|];Simpl;Auto;Try Discriminate);
+ Intro H2; Elim (IHp q H2);Auto; Intros E;Rewrite E;
+ Auto.
+Qed.
+
+Lemma ZLSS:
+ (x,y:positive) (compare x y SUPERIEUR) = SUPERIEUR ->
+                (compare x y EGAL) = SUPERIEUR \/ x = y.
+Proof.
+(Intro x; NewInduction x as [p IHp|p IHp|];
+ Intro y; NewDestruct y as [q|q|];Simpl;Auto;Try Discriminate);
+ Intro H2; Elim (IHp q H2);Auto; Intros E;Rewrite E;
+ Auto.
+Qed.
+
+Lemma Dcompare : (r:relation) r=EGAL \/ r = INFERIEUR \/ r = SUPERIEUR.
+Proof.
+Induction r; Auto. 
+Qed.
+
+Tactic Definition ElimPcompare c1 c2:=
+  Elim (Dcompare (compare c1 c2 EGAL)); [ Idtac | 
+     Let x = FreshId "H" In Intro x; Case x; Clear x ].
+
+Theorem convert_compare_EGAL: (x:positive)(compare x x EGAL)=EGAL.
+Intro x; Induction x; Auto.
+Qed.
+
+Lemma Pcompare_antisym :
+  (x,y:positive)(r:relation) (Op (compare x y r)) = (compare y x (Op r)).
+Proof.
+Intro x; NewInduction x as [p IHp|p IHp|]; Intro y; NewDestruct y; 
+Intro r; Reflexivity Orelse (Symmetry; Assumption) Orelse Discriminate H
+Orelse Simpl; Apply IHp Orelse Try Rewrite IHp; Try Reflexivity.
+Qed.
+
+Lemma ZC1:
+  (x,y:positive)(compare x y EGAL)=SUPERIEUR -> (compare y x EGAL)=INFERIEUR.
+Proof.
+Intros; Change EGAL with (Op EGAL).
+Rewrite <- Pcompare_antisym; Rewrite H; Reflexivity.
+Qed.
+
+Lemma ZC2:
+  (x,y:positive)(compare x y EGAL)=INFERIEUR -> (compare y x EGAL)=SUPERIEUR.
+Proof.
+Intros; Change EGAL with (Op EGAL).
+Rewrite <- Pcompare_antisym; Rewrite H; Reflexivity.
+Qed.
+
+Lemma ZC3: (x,y:positive)(compare x y EGAL)=EGAL -> (compare y x EGAL)=EGAL.
+Proof.
+Intros; Change EGAL with (Op EGAL).
+Rewrite <- Pcompare_antisym; Rewrite H; Reflexivity.
+Qed.
+
+Lemma ZC4: (x,y:positive) (compare x y EGAL) = (Op (compare y x EGAL)).
+Proof.
+Intros; Change 1 EGAL with (Op EGAL).
+Symmetry; Apply Pcompare_antisym.
+Qed.
+
+(**********************************************************************)
 (** Properties of subtraction on binary positive numbers *)
 
 Lemma ZS: (p:positive_mask) (Zero_suivi_de_mask p) = IsNul -> p = IsNul.
@@ -642,7 +797,7 @@ Intro x; NewInduction x as [p|p|]; Intro y; NewDestruct y as [q|q|]; Simpl;
 | NewDestruct p; Simpl; [ Discriminate H | Discriminate H | Reflexivity ] ].
 Qed.
 
-(** Properties valid only for x>y *)
+(** Properties of subtraction valid only for x>y *)
 
 Lemma sub_pos_SUPERIEUR:
   (x,y:positive)(compare x y EGAL)=SUPERIEUR -> 
@@ -727,603 +882,3 @@ Intros z H1;Elim H1;Intros H2 H3; Elim H3;Intros H4 H5;
 Unfold true_sub ;Rewrite H2; Exact H4.
 Qed.
 
-(**********************************************************************)
-(** Properties of the injection from binary positive numbers to Peano 
-    natural numbers *)
-
-Require Le.
-Require Lt.
-Require Gt.
-Require Plus.
-Require Mult.
-Require Minus.
-
-(** [nat_of_P] is a morphism for addition *)
-
-Lemma convert_add_un :
-  (x:positive)(m:nat)
-    (positive_to_nat (add_un x) m) = (plus m (positive_to_nat x m)).
-Proof.
-Intro x; NewInduction x as [p IHp|p IHp|]; Simpl; Auto; Intro m; Rewrite IHp;
-Rewrite plus_assoc_l; Trivial.
-Qed.
-
-Lemma cvt_add_un :
-  (p:positive) (convert (add_un p)) = (S (convert p)).
-Proof.
-  Intro; Change (S (convert p)) with (plus (S O) (convert p));
-  Unfold convert; Apply convert_add_un.
-Qed.
-
-Theorem convert_add_carry :
-  (x,y:positive)(m:nat)
-    (positive_to_nat (add_carry x y) m) =
-    (plus m (positive_to_nat (add x y) m)).
-Proof.
-Intro x; NewInduction x as [p IHp|p IHp|];
-  Intro y; NewDestruct y; Simpl; Auto with arith; Intro m; [
-  Rewrite IHp; Rewrite plus_assoc_l; Trivial with arith
-| Rewrite IHp; Rewrite plus_assoc_l; Trivial with arith
-| Rewrite convert_add_un; Rewrite plus_assoc_l; Trivial with arith
-| Rewrite convert_add_un; Apply plus_assoc_r ].
-Qed.
-
-Theorem cvt_carry :
-  (x,y:positive)(convert (add_carry x y)) = (S (convert (add x y))).
-Proof.
-Intros;Unfold convert; Rewrite convert_add_carry; Simpl; Trivial with arith.
-Qed.
-
-Theorem add_verif :
-  (x,y:positive)(m:nat)
-    (positive_to_nat (add x y) m) = 
-    (plus (positive_to_nat x m) (positive_to_nat y m)).
-Proof.
-Intro x; NewInduction x as [p IHp|p IHp|];
-  Intro y; NewDestruct y;Simpl;Auto with arith; [
-  Intros m;Rewrite convert_add_carry; Rewrite IHp; 
-  Rewrite plus_assoc_r; Rewrite plus_assoc_r; 
-  Rewrite (plus_permute m (positive_to_nat p (plus m m))); Trivial with arith
-| Intros m; Rewrite IHp; Apply plus_assoc_l
-| Intros m; Rewrite convert_add_un; 
-  Rewrite (plus_sym (plus m (positive_to_nat p (plus m m))));
-  Apply plus_assoc_r
-| Intros m; Rewrite IHp; Apply plus_permute
-| Intros m; Rewrite convert_add_un; Apply plus_assoc_r ].
-Qed.
-
-Theorem convert_add:
-  (x,y:positive) (convert (add x y)) = (plus (convert x) (convert y)).
-Proof.
-Intros x y; Exact (add_verif x y (S O)).
-Qed.
-
-(** [Pmult_nat] is a morphism for addition *)
-
-Lemma ZL2:
-  (y:positive)(m:nat)
-    (positive_to_nat y (plus m m)) =
-              (plus (positive_to_nat y m) (positive_to_nat y m)).
-Proof.
-Intro y; NewInduction y as [p H|p H|]; Intro m; [
-  Simpl; Rewrite H; Rewrite plus_assoc_r; 
-  Rewrite (plus_permute m (positive_to_nat p (plus m m)));
-  Rewrite plus_assoc_r; Auto with arith
-| Simpl; Rewrite H; Auto with arith
-| Simpl; Trivial with arith ].
-Qed.
-
-Lemma ZL6:
-  (p:positive) (positive_to_nat p (S (S O))) = (plus (convert p) (convert p)).
-Proof.
-Intro p;Change (2) with (plus (S O) (S O)); Rewrite ZL2; Trivial.
-Qed.
- 
-(** [nat_of_P] is a morphism for multiplication *)
-
-Theorem times_convert :
-  (x,y:positive) (convert (times x y)) = (mult (convert x) (convert y)).
-Proof.
-Intros x y; NewInduction x as [ x' H | x' H | ]; [
-  Change (times (xI x') y) with (add y (xO (times x' y))); Rewrite convert_add;
-  Unfold 2 3 convert; Simpl; Do 2 Rewrite ZL6; Rewrite H;
-  Rewrite -> mult_plus_distr; Reflexivity
-| Unfold 1 2 convert; Simpl; Do 2 Rewrite ZL6;
-  Rewrite H; Rewrite mult_plus_distr; Reflexivity
-| Simpl; Rewrite <- plus_n_O; Reflexivity ].
-Qed.
-V7only [
-  Comments "Compatibility with the old version of times and times_convert".
-  Syntactic Definition times1 :=
-    [x:positive;_:positive->positive;y:positive](times x y).
-  Syntactic Definition times1_convert :=
-    [x,y:positive;_:positive->positive](times_convert x y).
-].
-
-(** [nat_of_P] is strictly positive *)
-
-Lemma compare_positive_to_nat_O : 
-	(p:positive)(m:nat)(le m (positive_to_nat p m)).
-NewInduction p; Simpl; Auto with arith.
-Intro m; Apply le_trans with (plus m m);  Auto with arith.
-Qed.
-
-Lemma compare_convert_O : (p:positive)(lt O (convert p)).
-Intro; Unfold convert; Apply lt_le_trans with (S O); Auto with arith.
-Apply compare_positive_to_nat_O.
-Qed.
-
-(** Pmult_nat permutes with multiplication *)
-
-Lemma positive_to_nat_mult : (p:positive) (n,m:nat)
-    (positive_to_nat p (mult m n))=(mult m (positive_to_nat p n)).
-Proof.
-  Induction p. Intros. Simpl. Rewrite mult_plus_distr_r. Rewrite <- (mult_plus_distr_r m n n).
-  Rewrite (H (plus n n) m). Reflexivity.
-  Intros. Simpl. Rewrite <- (mult_plus_distr_r m n n). Apply H.
-  Trivial.
-Qed.
-
-Lemma positive_to_nat_2 : (p:positive)
-    (positive_to_nat p (2))=(mult (2) (positive_to_nat p (1))).
-Proof.
-  Intros. Rewrite <- positive_to_nat_mult. Reflexivity.
-Qed.
-
-Lemma positive_to_nat_4 : (p:positive)
-    (positive_to_nat p (4))=(mult (2) (positive_to_nat p (2))).
-Proof.
-  Intros. Rewrite <- positive_to_nat_mult. Reflexivity.
-Qed.
-
-(** Mapping of xH, xO and xI through [nat_of_P] *)
-
-Lemma convert_xH : (convert xH)=(1).
-Proof.
-  Reflexivity.
-Qed.
-
-Lemma convert_xO : (p:positive) (convert (xO p))=(mult (2) (convert p)).
-Proof.
-  Induction p. Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2.
-  Rewrite positive_to_nat_4. Rewrite H. Simpl. Rewrite <- plus_Snm_nSm. Reflexivity.
-  Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4.
-  Rewrite H. Reflexivity.
-  Reflexivity.
-Qed.
-
-Lemma convert_xI : (p:positive) (convert (xI p))=(S (mult (2) (convert p))).
-Proof.
-  Induction p. Unfold convert. Simpl. Intro p0. Intro. Rewrite positive_to_nat_2.
-  Rewrite positive_to_nat_4; Injection H; Intro H1; Rewrite H1; Rewrite <- plus_Snm_nSm; Reflexivity.
-  Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4.
-  Injection H; Intro H1; Rewrite H1; Reflexivity.
-  Reflexivity.
-Qed.
-
-(**********************************************************************)
-(** Properties of the shifted injection from Peano natural numbers to 
-    binary positive numbers *)
-
-(** Composition of [P_of_succ_nat] and [nat_of_P] is successor on [nat] *)
-
-Theorem bij1 : (m:nat) (convert (anti_convert m)) = (S m).
-Proof.
-Intro m; NewInduction m as [|n H]; [
-  Reflexivity
-| Simpl; Rewrite cvt_add_un; Rewrite H; Auto ].
-Qed.
-
-(** Miscellaneous lemmas on [P_of_succ_nat] *)
-
-Lemma ZL3: (x:nat) (add_un (anti_convert (plus x x))) =  (xO (anti_convert x)).
-Proof.
-Intro x; NewInduction x as [|n H]; [
-  Simpl; Auto with arith
-| Simpl; Rewrite  plus_sym; Simpl; Rewrite  H; Rewrite  ZL1;Auto with arith].
-Qed.
-
-Lemma ZL4: (y:positive) (EX h:nat |(convert y)=(S h)).
-Proof.
-Intro y; NewInduction y as [p H|p H|]; [
-  NewDestruct H as [x H1]; Exists (plus (S x) (S x));
-  Unfold convert ;Simpl; Change (2) with (plus (1) (1)); Rewrite ZL2; Unfold convert in H1;
-  Rewrite H1; Auto with arith
-| NewDestruct H as [x H2]; Exists (plus x (S x)); Unfold convert;
-  Simpl; Change (2) with (plus (1) (1)); Rewrite ZL2;Unfold convert in H2; Rewrite H2; Auto with arith
-| Exists O ;Auto with arith ].
-Qed.
-
-Lemma ZL5: (x:nat) (anti_convert (plus (S x) (S x))) =  (xI (anti_convert x)).
-Proof.
-Intro x; NewInduction x as [|n H];Simpl; [
-  Auto with arith
-| Rewrite <- plus_n_Sm; Simpl; Simpl in H; Rewrite H; Auto with arith].
-Qed.
-
-(** Composition of [nat_of_P] and [P_of_succ_nat] is successor on [positive] *)
-
-Theorem bij2 : (x:positive) (anti_convert (convert x)) = (add_un x).
-Proof.
-Intro x; NewInduction x as [p H|p H|]; [
-  Simpl; Rewrite <- H; Change (2) with (plus (1) (1));
-  Rewrite ZL2; Elim (ZL4 p); 
-  Unfold convert; Intros n H1;Rewrite H1; Rewrite ZL3; Auto with arith
-| Unfold convert ;Simpl; Change (2) with (plus (1) (1));
-  Rewrite ZL2;
-  Rewrite <- (sub_add_one
-               (anti_convert
-                 (plus (positive_to_nat p (S O)) (positive_to_nat p (S O)))));
-  Rewrite <- (sub_add_one (xI p));
-  Simpl;Rewrite <- H;Elim (ZL4 p); Unfold convert ;Intros n H1;Rewrite H1;
-  Rewrite ZL5; Simpl; Trivial with arith
-| Unfold convert; Simpl; Auto with arith ].
-Qed.
-
-(** Composition of [nat_of_P], [P_of_succ_nat] and [Ppred] is identity
-    on [positive] *)
-
-Theorem bij3: (x:positive)(sub_un (anti_convert (convert x))) = x.
-Proof.
-Intros x; Rewrite bij2; Rewrite sub_add_one; Trivial with arith.
-Qed.
-
-(** Extra lemmas on [lt] on Peano natural numbers *)
-
-Lemma ZL7:
-  (m,n:nat) (lt m n) -> (lt (plus m m) (plus n n)).
-Proof.
-Intros m n H; Apply lt_trans with m:=(plus m n); [
-  Apply lt_reg_l with 1:=H
-| Rewrite (plus_sym m n); Apply lt_reg_l with 1:=H ].
-Qed.
-
-Lemma ZL8:
-  (m,n:nat) (lt m n) -> (lt (S (plus m m)) (plus n n)).
-Proof.
-Intros m n H; Apply le_lt_trans with m:=(plus m n); [
-  Change (lt (plus m m) (plus m n)) ; Apply lt_reg_l with 1:=H
-| Rewrite (plus_sym m n); Apply lt_reg_l with 1:=H ].
-Qed.
-
-(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed
-    from [compare] on [positive])
-
-    Part 1: [lt] on [positive] is finer than [lt] on [nat]
-*)
-
-Lemma compare_convert_INFERIEUR : 
-  (x,y:positive) (compare x y EGAL) = INFERIEUR -> 
-    (lt (convert x) (convert y)).
-Proof.
-Intro x; NewInduction x as [p H|p H|];Intro y; NewDestruct y as [q|q|];
-  Intro H2; [
-  Unfold convert ;Simpl; Apply lt_n_S; 
-  Do 2 Rewrite ZL6; Apply ZL7; Apply H; Simpl in H2; Assumption
-| Unfold convert ;Simpl; Do 2 Rewrite ZL6; 
-  Apply ZL8; Apply H;Simpl in H2; Apply ZLSI;Assumption
-| Simpl; Discriminate H2
-| Simpl; Unfold convert ;Simpl;Do 2 Rewrite ZL6; 
-  Elim (ZLII p q H2); [
-    Intros H3;Apply lt_S;Apply ZL7; Apply H;Apply H3
-  | Intros E;Rewrite E;Apply lt_n_Sn]
-| Simpl; Unfold convert ;Simpl;Do 2 Rewrite ZL6; 
-  Apply ZL7;Apply H;Assumption
-| Simpl; Discriminate H2
-| Unfold convert ;Simpl; Apply lt_n_S; Rewrite ZL6;
-  Elim (ZL4 q);Intros h H3; Rewrite H3;Simpl; Apply lt_O_Sn
-| Unfold convert ;Simpl; Rewrite ZL6; Elim (ZL4 q);Intros h H3;
-  Rewrite H3; Simpl; Rewrite <- plus_n_Sm; Apply lt_n_S; Apply lt_O_Sn
-| Simpl; Discriminate H2 ].
-Qed.
-
-(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed
-    from [compare] on [positive])
-
-    Part 1: [gt] on [positive] is finer than [gt] on [nat]
-*)
-
-Lemma compare_convert_SUPERIEUR : 
-  (x,y:positive) (compare x y EGAL)=SUPERIEUR -> (gt (convert x) (convert y)).
-Proof.
-Unfold gt; Intro x; NewInduction x as [p H|p H|];
-  Intro y; NewDestruct y as [q|q|]; Intro H2; [
-  Simpl; Unfold convert ;Simpl;Do 2 Rewrite ZL6; 
-  Apply lt_n_S; Apply ZL7; Apply H;Assumption
-| Simpl; Unfold convert ;Simpl; Do 2 Rewrite ZL6;
-  Elim (ZLSS p q H2); [
-    Intros H3;Apply lt_S;Apply ZL7;Apply H;Assumption
-  | Intros E;Rewrite E;Apply lt_n_Sn]
-| Unfold convert ;Simpl; Rewrite ZL6;Elim (ZL4 p);
-  Intros h H3;Rewrite H3;Simpl; Apply lt_n_S; Apply lt_O_Sn
-| Simpl;Unfold convert ;Simpl;Do 2 Rewrite ZL6; 
-  Apply ZL8; Apply H; Apply ZLIS; Assumption
-| Simpl; Unfold convert ;Simpl;Do 2 Rewrite ZL6; 
-  Apply ZL7;Apply H;Assumption
-| Unfold convert ;Simpl; Rewrite ZL6; Elim (ZL4 p);
-  Intros h H3;Rewrite H3;Simpl; Rewrite <- plus_n_Sm;Apply lt_n_S;
-  Apply lt_O_Sn
-| Simpl; Discriminate H2
-| Simpl; Discriminate H2
-| Simpl; Discriminate H2 ].
-Qed.
-
-(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed
-    from [compare] on [positive])
-
-    Part 2: [lt] on [nat] is finer than [lt] on [positive]
-*)
-
-Lemma convert_compare_INFERIEUR : 
-  (x,y:positive)(lt (convert x) (convert y)) -> (compare x y EGAL) = INFERIEUR.
-Proof.
-Intros x y; Unfold gt; Elim (Dcompare (compare x y EGAL)); [
-  Intros E; Rewrite (compare_convert_EGAL x y E); 
-  Intros H;Absurd (lt (convert y) (convert y)); [ Apply lt_n_n | Assumption ]
-| Intros H;Elim H; [
-    Auto
-  | Intros H1 H2; Absurd (lt (convert x) (convert y)); [
-      Apply lt_not_sym; Change (gt (convert x) (convert y)); 
-      Apply compare_convert_SUPERIEUR; Assumption
-    | Assumption ]]].
-Qed.
-
-(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed
-    from [compare] on [positive])
-
-    Part 2: [gt] on [nat] is finer than [gt] on [positive]
-*)
-
-Lemma convert_compare_SUPERIEUR : 
-  (x,y:positive)(gt (convert x) (convert y)) -> (compare x y EGAL) = SUPERIEUR.
-Proof.
-Intros x y; Unfold gt; Elim (Dcompare (compare x y EGAL)); [
-  Intros E; Rewrite (compare_convert_EGAL x y E); 
-  Intros H;Absurd (lt (convert y) (convert y)); [ Apply lt_n_n | Assumption ]
-| Intros H;Elim H; [
-    Intros H1 H2; Absurd (lt (convert y) (convert x)); [
-      Apply lt_not_sym; Apply compare_convert_INFERIEUR; Assumption
-    | Assumption ]
-  | Auto]].
-Qed.
-
-(**********************************************************************)
-(** Extra properties of the comparison on binary positive numbers *)
-
-Lemma ZC1:
-  (x,y:positive)(compare x y EGAL)=SUPERIEUR -> (compare y x EGAL)=INFERIEUR.
-Proof.
-Intros x y H;Apply convert_compare_INFERIEUR; 
-Change (gt (convert x) (convert y));Apply compare_convert_SUPERIEUR;
-Assumption.
-Qed.
-
-Lemma ZC2:
-  (x,y:positive)(compare x y EGAL)=INFERIEUR -> (compare y x EGAL)=SUPERIEUR.
-Proof.
-Intros x y H;Apply convert_compare_SUPERIEUR;Unfold gt;
-Apply compare_convert_INFERIEUR;Assumption.
-Qed.
-
-Lemma ZC3: (x,y:positive)(compare x y EGAL)=EGAL -> (compare y x EGAL)=EGAL.
-Proof.
-Intros x y H; Rewrite (compare_convert_EGAL x y H);
-Apply convert_compare_EGAL.
-Qed.
-
-Lemma ZC4: (x,y:positive) (compare x y EGAL) = (Op (compare y x EGAL)).
-Proof.
-Intros x y;ElimPcompare y x; 
-Intros E;Rewrite E;Simpl; [Apply ZC3 | Apply ZC2 | Apply ZC1 ]; Assumption.
-Qed.
-
-(**********************************************************************)
-(** Extra properties of the injection from binary positive numbers to Peano 
-    natural numbers *)
-
-(** [nat_of_P] is a morphism for subtraction on positive numbers *)
-
-Theorem true_sub_convert:
-  (x,y:positive) (compare x y EGAL) = SUPERIEUR -> 
-     (convert (true_sub x y)) = (minus (convert x) (convert y)).
-Proof.
-Intros x y H; Apply plus_reg_l with (convert y);
-Rewrite le_plus_minus_r; [
-  Rewrite <- convert_add; Rewrite sub_add; Auto with arith
-| Apply lt_le_weak; Exact (compare_convert_SUPERIEUR x y H)].
-Qed.
-
-(** [nat_of_P] is injective *)
-
-Lemma convert_intro : (x,y:positive)(convert x)=(convert y) -> x=y.
-Proof.
-Intros x y H;Rewrite <- (bij3 x);Rewrite <- (bij3 y); Rewrite H; Trivial with arith.
-Qed.
-
-Lemma ZL16: (p,q:positive)(lt (minus (convert p) (convert q)) (convert p)).
-Proof.
-Intros p q; Elim (ZL4 p);Elim (ZL4 q); Intros h H1 i H2; 
-Rewrite H1;Rewrite H2; Simpl;Unfold lt; Apply le_n_S; Apply le_minus.
-Qed.
-
-Lemma ZL17: (p,q:positive)(lt (convert p) (convert (add p q))).
-Proof.
-Intros p q; Rewrite convert_add;Unfold lt;Elim (ZL4 q); Intros k H;Rewrite H;
-Rewrite plus_sym;Simpl; Apply le_n_S; Apply le_plus_r.
-Qed.
-
-(** Comparison and subtraction *)
-
-Lemma compare_true_sub_right :
-  (p,q,z:positive)
-  (compare q p EGAL)=INFERIEUR->
-  (compare z p EGAL)=SUPERIEUR->
-  (compare z q EGAL)=SUPERIEUR->
-  (compare (true_sub z p) (true_sub z q) EGAL)=INFERIEUR.
-Proof.
-Intros; Apply convert_compare_INFERIEUR; Rewrite true_sub_convert; [
-  Rewrite true_sub_convert; [
-    Apply simpl_lt_plus_l with p:=(convert q); Rewrite le_plus_minus_r; [
-      Rewrite plus_sym; Apply simpl_lt_plus_l with p:=(convert p);
-        Rewrite plus_assoc_l; Rewrite le_plus_minus_r; [
-          Rewrite (plus_sym (convert p)); Apply lt_reg_l;
-          Apply compare_convert_INFERIEUR; Assumption 
-        | Apply lt_le_weak; Apply compare_convert_INFERIEUR;
-          Apply ZC1; Assumption ]
-      | Apply lt_le_weak;Apply compare_convert_INFERIEUR;
-        Apply ZC1; Assumption ]
-    | Assumption ]
-  | Assumption ].
-Qed.
-
-Lemma compare_true_sub_left :
-  (p,q,z:positive)
-  (compare q p EGAL)=INFERIEUR->
-  (compare p z EGAL)=SUPERIEUR->
-  (compare q z EGAL)=SUPERIEUR->
-  (compare (true_sub q z) (true_sub p z) EGAL)=INFERIEUR.
-Proof.
-Intros p q z; Intros; 
-  Apply convert_compare_INFERIEUR; Rewrite true_sub_convert; [
-  Rewrite true_sub_convert; [
-    Unfold gt; Apply simpl_lt_plus_l with p:=(convert z);
-    Rewrite le_plus_minus_r; [
-      Rewrite le_plus_minus_r; [
-        Apply compare_convert_INFERIEUR;Assumption
-      | Apply lt_le_weak; Apply compare_convert_INFERIEUR;Apply ZC1;Assumption]
-    | Apply lt_le_weak; Apply compare_convert_INFERIEUR;Apply ZC1; Assumption]
-  | Assumption]
-| Assumption].
-Qed.
-
-(**********************************************************************)
-(** Properties of multiplication on binary positive numbers *)
-
-(** One is right neutral for multiplication *)
-
-Lemma times_x_1 : (x:positive) (times x xH) = x.
-Proof.
-Intro x;NewInduction x; Simpl.
-  Rewrite IHx; Reflexivity.
-  Rewrite IHx; Reflexivity.
-  Reflexivity.
-Qed.
-
-(** Right reduction properties for multiplication *)
-
-Lemma times_x_double : (x,y:positive) (times x (xO y)) = (xO (times x y)).
-Proof.
-Intros x y; NewInduction x; Simpl.
-  Rewrite IHx; Reflexivity.
-  Rewrite IHx; Reflexivity.
-  Reflexivity.
-Qed.
-
-Lemma times_x_double_plus_one :
- (x,y:positive) (times x (xI y)) = (add x (xO (times x y))).
-Proof.
-Intros x y; NewInduction x; Simpl.
-  Rewrite IHx; Do 2 Rewrite add_assoc; Rewrite add_sym with x:=y; Reflexivity.
-  Rewrite IHx; Reflexivity.
-  Reflexivity.
-Qed.
-
-(** Commutativity of multiplication *)
-
-Theorem times_sym : (x,y:positive) (times x y) = (times y x).
-Proof.
-Intros x y; NewInduction y; Simpl.
-  Rewrite <- IHy; Apply times_x_double_plus_one.
-  Rewrite <- IHy; Apply times_x_double.
-  Apply times_x_1.
-Qed.
-
-(** Distributivity of multiplication over addition *)
-
-Theorem times_add_distr:
-  (x,y,z:positive) (times x (add y z)) = (add (times x y) (times x z)).
-Proof.
-Intros x y z; NewInduction x; Simpl.
-  Rewrite IHx; Rewrite <- add_assoc with y := (xO (times x y));
-    Rewrite -> add_assoc with x := (xO (times x y));
-    Rewrite -> add_sym with x := (xO (times x y));
-    Rewrite <- add_assoc with y := (xO (times x y));
-    Rewrite -> add_assoc with y := z; Reflexivity.
-  Rewrite IHx; Reflexivity.
-  Reflexivity.
-Qed.
-
-Theorem times_add_distr_l:
-  (x,y,z:positive) (times (add x y) z) = (add (times x z) (times y z)).
-Proof.
-Intros x y z; Do 3 Rewrite times_sym with y:=z; Apply times_add_distr.
-Qed.
-
-(** Associativity of multiplication *)
-
-Theorem times_assoc :
-  ((x,y,z:positive) (times x (times y z))= (times (times x y) z)).
-Proof.
-Intro x;NewInduction x as [x|x|]; Simpl; Intros y z.
-  Rewrite IHx; Rewrite times_add_distr_l; Reflexivity.
-  Rewrite IHx; Reflexivity.
-  Reflexivity.
-Qed.
-
-(** Distributivity of multiplication over subtraction *)
-
-Theorem times_true_sub_distr:
-  (x,y,z:positive) (compare y z EGAL) = SUPERIEUR -> 
-      (times x (true_sub y z)) = (true_sub (times x y) (times x z)).
-Proof.
-Intros x y z H; Apply convert_intro;
-Rewrite times_convert; Rewrite true_sub_convert; [
-  Rewrite true_sub_convert; [
-    Do 2 Rewrite times_convert;
-    Do 3 Rewrite (mult_sym (convert x));Apply mult_minus_distr
-  | Apply convert_compare_SUPERIEUR; Do 2 Rewrite times_convert; 
-    Unfold gt; Elim (ZL4 x);Intros h H1;Rewrite H1; Apply lt_mult_left;
-    Exact (compare_convert_SUPERIEUR y z H) ]
-| Assumption ].
-Qed.
-
-(** Parity properties of multiplication *)
-
-Lemma times_discr_xO_xI : 
-  (x,y,z:positive)(times (xI x) z)<>(times (xO y) z).
-Proof.
-Intros x y z; NewInduction z as [|z IHz|]; Try Discriminate.
-Intro H; Apply IHz; Clear IHz.
-Do 2 Rewrite times_x_double in H.
-Injection H; Clear H; Intro H; Exact H.
-Qed.
-
-Lemma times_discr_xO : (x,y:positive)(times (xO x) y)<>y.
-Proof.
-Intros x y; NewInduction y; Try Discriminate.
-Rewrite times_x_double; Injection; Assumption.
-Qed.
-
-(** Simplification properties of multiplication *)
-
-Theorem simpl_times_r : (x,y,z:positive) (times x z)=(times y z) -> x=y.
-Proof.
-Intro x;NewInduction x as [p IHp|p IHp|]; Intro y; NewDestruct y as [q|q|]; Intros z H;
-    Reflexivity Orelse Apply (f_equal positive) Orelse Apply False_ind.
-  Simpl in H; Apply IHp with (xO z); Simpl; Do 2 Rewrite times_x_double;
-    Apply simpl_add_l with 1 := H.
-  Apply times_discr_xO_xI with 1 := H.
-  Simpl in H; Rewrite add_sym in H; Apply add_no_neutral with 1 := H.
-  Symmetry in H; Apply times_discr_xO_xI with 1 := H.
-  Apply IHp with (xO z); Simpl; Do 2 Rewrite times_x_double; Assumption.
-  Apply times_discr_xO with 1:=H.
-  Simpl in H; Symmetry in H; Rewrite add_sym in H; 
-    Apply add_no_neutral with 1 := H.
-  Symmetry in H; Apply times_discr_xO with 1:=H.
-Qed.
-
-Theorem simpl_times_l : (x,y,z:positive) (times z x)=(times z y) -> x=y.
-Proof.
-Intros x y z H; Apply simpl_times_r with z:=z.
-Rewrite times_sym with x:=x; Rewrite times_sym with x:=y; Assumption.
-Qed.
diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v
new file mode 100644
index 000000000..22c6b5cb9
--- /dev/null
+++ b/theories/NArith/Pnat.v
@@ -0,0 +1,472 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+Require BinPos.
+
+(**********************************************************************)
+(** Properties of the injection from binary positive numbers to Peano 
+    natural numbers *)
+
+(** Original development by Pierre Crégut, CNET, Lannion, France *)
+
+Require Le.
+Require Lt.
+Require Gt.
+Require Plus.
+Require Mult.
+Require Minus.
+
+(** [nat_of_P] is a morphism for addition *)
+
+Lemma convert_add_un :
+  (x:positive)(m:nat)
+    (positive_to_nat (add_un x) m) = (plus m (positive_to_nat x m)).
+Proof.
+Intro x; NewInduction x as [p IHp|p IHp|]; Simpl; Auto; Intro m; Rewrite IHp;
+Rewrite plus_assoc_l; Trivial.
+Qed.
+
+Lemma cvt_add_un :
+  (p:positive) (convert (add_un p)) = (S (convert p)).
+Proof.
+  Intro; Change (S (convert p)) with (plus (S O) (convert p));
+  Unfold convert; Apply convert_add_un.
+Qed.
+
+Theorem convert_add_carry :
+  (x,y:positive)(m:nat)
+    (positive_to_nat (add_carry x y) m) =
+    (plus m (positive_to_nat (add x y) m)).
+Proof.
+Intro x; NewInduction x as [p IHp|p IHp|];
+  Intro y; NewDestruct y; Simpl; Auto with arith; Intro m; [
+  Rewrite IHp; Rewrite plus_assoc_l; Trivial with arith
+| Rewrite IHp; Rewrite plus_assoc_l; Trivial with arith
+| Rewrite convert_add_un; Rewrite plus_assoc_l; Trivial with arith
+| Rewrite convert_add_un; Apply plus_assoc_r ].
+Qed.
+
+Theorem cvt_carry :
+  (x,y:positive)(convert (add_carry x y)) = (S (convert (add x y))).
+Proof.
+Intros;Unfold convert; Rewrite convert_add_carry; Simpl; Trivial with arith.
+Qed.
+
+Theorem add_verif :
+  (x,y:positive)(m:nat)
+    (positive_to_nat (add x y) m) = 
+    (plus (positive_to_nat x m) (positive_to_nat y m)).
+Proof.
+Intro x; NewInduction x as [p IHp|p IHp|];
+  Intro y; NewDestruct y;Simpl;Auto with arith; [
+  Intros m;Rewrite convert_add_carry; Rewrite IHp; 
+  Rewrite plus_assoc_r; Rewrite plus_assoc_r; 
+  Rewrite (plus_permute m (positive_to_nat p (plus m m))); Trivial with arith
+| Intros m; Rewrite IHp; Apply plus_assoc_l
+| Intros m; Rewrite convert_add_un; 
+  Rewrite (plus_sym (plus m (positive_to_nat p (plus m m))));
+  Apply plus_assoc_r
+| Intros m; Rewrite IHp; Apply plus_permute
+| Intros m; Rewrite convert_add_un; Apply plus_assoc_r ].
+Qed.
+
+Theorem convert_add:
+  (x,y:positive) (convert (add x y)) = (plus (convert x) (convert y)).
+Proof.
+Intros x y; Exact (add_verif x y (S O)).
+Qed.
+
+(** [Pmult_nat] is a morphism for addition *)
+
+Lemma ZL2:
+  (y:positive)(m:nat)
+    (positive_to_nat y (plus m m)) =
+              (plus (positive_to_nat y m) (positive_to_nat y m)).
+Proof.
+Intro y; NewInduction y as [p H|p H|]; Intro m; [
+  Simpl; Rewrite H; Rewrite plus_assoc_r; 
+  Rewrite (plus_permute m (positive_to_nat p (plus m m)));
+  Rewrite plus_assoc_r; Auto with arith
+| Simpl; Rewrite H; Auto with arith
+| Simpl; Trivial with arith ].
+Qed.
+
+Lemma ZL6:
+  (p:positive) (positive_to_nat p (S (S O))) = (plus (convert p) (convert p)).
+Proof.
+Intro p;Change (2) with (plus (S O) (S O)); Rewrite ZL2; Trivial.
+Qed.
+ 
+(** [nat_of_P] is a morphism for multiplication *)
+
+Theorem times_convert :
+  (x,y:positive) (convert (times x y)) = (mult (convert x) (convert y)).
+Proof.
+Intros x y; NewInduction x as [ x' H | x' H | ]; [
+  Change (times (xI x') y) with (add y (xO (times x' y))); Rewrite convert_add;
+  Unfold 2 3 convert; Simpl; Do 2 Rewrite ZL6; Rewrite H;
+  Rewrite -> mult_plus_distr; Reflexivity
+| Unfold 1 2 convert; Simpl; Do 2 Rewrite ZL6;
+  Rewrite H; Rewrite mult_plus_distr; Reflexivity
+| Simpl; Rewrite <- plus_n_O; Reflexivity ].
+Qed.
+V7only [
+  Comments "Compatibility with the old version of times and times_convert".
+  Syntactic Definition times1 :=
+    [x:positive;_:positive->positive;y:positive](times x y).
+  Syntactic Definition times1_convert :=
+    [x,y:positive;_:positive->positive](times_convert x y).
+].
+
+(** [nat_of_P] maps to the strictly positive subset of [nat] *)
+
+Lemma ZL4: (y:positive) (EX h:nat |(convert y)=(S h)).
+Proof.
+Intro y; NewInduction y as [p H|p H|]; [
+  NewDestruct H as [x H1]; Exists (plus (S x) (S x));
+  Unfold convert ;Simpl; Change (2) with (plus (1) (1)); Rewrite ZL2; Unfold convert in H1;
+  Rewrite H1; Auto with arith
+| NewDestruct H as [x H2]; Exists (plus x (S x)); Unfold convert;
+  Simpl; Change (2) with (plus (1) (1)); Rewrite ZL2;Unfold convert in H2; Rewrite H2; Auto with arith
+| Exists O ;Auto with arith ].
+Qed.
+
+(** Extra lemmas on [lt] on Peano natural numbers *)
+
+Lemma ZL7:
+  (m,n:nat) (lt m n) -> (lt (plus m m) (plus n n)).
+Proof.
+Intros m n H; Apply lt_trans with m:=(plus m n); [
+  Apply lt_reg_l with 1:=H
+| Rewrite (plus_sym m n); Apply lt_reg_l with 1:=H ].
+Qed.
+
+Lemma ZL8:
+  (m,n:nat) (lt m n) -> (lt (S (plus m m)) (plus n n)).
+Proof.
+Intros m n H; Apply le_lt_trans with m:=(plus m n); [
+  Change (lt (plus m m) (plus m n)) ; Apply lt_reg_l with 1:=H
+| Rewrite (plus_sym m n); Apply lt_reg_l with 1:=H ].
+Qed.
+
+(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed
+    from [compare] on [positive])
+
+    Part 1: [lt] on [positive] is finer than [lt] on [nat]
+*)
+
+Lemma compare_convert_INFERIEUR : 
+  (x,y:positive) (compare x y EGAL) = INFERIEUR -> 
+    (lt (convert x) (convert y)).
+Proof.
+Intro x; NewInduction x as [p H|p H|];Intro y; NewDestruct y as [q|q|];
+  Intro H2; [
+  Unfold convert ;Simpl; Apply lt_n_S; 
+  Do 2 Rewrite ZL6; Apply ZL7; Apply H; Simpl in H2; Assumption
+| Unfold convert ;Simpl; Do 2 Rewrite ZL6; 
+  Apply ZL8; Apply H;Simpl in H2; Apply ZLSI;Assumption
+| Simpl; Discriminate H2
+| Simpl; Unfold convert ;Simpl;Do 2 Rewrite ZL6; 
+  Elim (ZLII p q H2); [
+    Intros H3;Apply lt_S;Apply ZL7; Apply H;Apply H3
+  | Intros E;Rewrite E;Apply lt_n_Sn]
+| Simpl; Unfold convert ;Simpl;Do 2 Rewrite ZL6; 
+  Apply ZL7;Apply H;Assumption
+| Simpl; Discriminate H2
+| Unfold convert ;Simpl; Apply lt_n_S; Rewrite ZL6;
+  Elim (ZL4 q);Intros h H3; Rewrite H3;Simpl; Apply lt_O_Sn
+| Unfold convert ;Simpl; Rewrite ZL6; Elim (ZL4 q);Intros h H3;
+  Rewrite H3; Simpl; Rewrite <- plus_n_Sm; Apply lt_n_S; Apply lt_O_Sn
+| Simpl; Discriminate H2 ].
+Qed.
+
+(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed
+    from [compare] on [positive])
+
+    Part 1: [gt] on [positive] is finer than [gt] on [nat]
+*)
+
+Lemma compare_convert_SUPERIEUR : 
+  (x,y:positive) (compare x y EGAL)=SUPERIEUR -> (gt (convert x) (convert y)).
+Proof.
+Unfold gt; Intro x; NewInduction x as [p H|p H|];
+  Intro y; NewDestruct y as [q|q|]; Intro H2; [
+  Simpl; Unfold convert ;Simpl;Do 2 Rewrite ZL6; 
+  Apply lt_n_S; Apply ZL7; Apply H;Assumption
+| Simpl; Unfold convert ;Simpl; Do 2 Rewrite ZL6;
+  Elim (ZLSS p q H2); [
+    Intros H3;Apply lt_S;Apply ZL7;Apply H;Assumption
+  | Intros E;Rewrite E;Apply lt_n_Sn]
+| Unfold convert ;Simpl; Rewrite ZL6;Elim (ZL4 p);
+  Intros h H3;Rewrite H3;Simpl; Apply lt_n_S; Apply lt_O_Sn
+| Simpl;Unfold convert ;Simpl;Do 2 Rewrite ZL6; 
+  Apply ZL8; Apply H; Apply ZLIS; Assumption
+| Simpl; Unfold convert ;Simpl;Do 2 Rewrite ZL6; 
+  Apply ZL7;Apply H;Assumption
+| Unfold convert ;Simpl; Rewrite ZL6; Elim (ZL4 p);
+  Intros h H3;Rewrite H3;Simpl; Rewrite <- plus_n_Sm;Apply lt_n_S;
+  Apply lt_O_Sn
+| Simpl; Discriminate H2
+| Simpl; Discriminate H2
+| Simpl; Discriminate H2 ].
+Qed.
+
+(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed
+    from [compare] on [positive])
+
+    Part 2: [lt] on [nat] is finer than [lt] on [positive]
+*)
+
+Lemma convert_compare_INFERIEUR : 
+  (x,y:positive)(lt (convert x) (convert y)) -> (compare x y EGAL) = INFERIEUR.
+Proof.
+Intros x y; Unfold gt; Elim (Dcompare (compare x y EGAL)); [
+  Intros E; Rewrite (compare_convert_EGAL x y E); 
+  Intros H;Absurd (lt (convert y) (convert y)); [ Apply lt_n_n | Assumption ]
+| Intros H;Elim H; [
+    Auto
+  | Intros H1 H2; Absurd (lt (convert x) (convert y)); [
+      Apply lt_not_sym; Change (gt (convert x) (convert y)); 
+      Apply compare_convert_SUPERIEUR; Assumption
+    | Assumption ]]].
+Qed.
+
+(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed
+    from [compare] on [positive])
+
+    Part 2: [gt] on [nat] is finer than [gt] on [positive]
+*)
+
+Lemma convert_compare_SUPERIEUR : 
+  (x,y:positive)(gt (convert x) (convert y)) -> (compare x y EGAL) = SUPERIEUR.
+Proof.
+Intros x y; Unfold gt; Elim (Dcompare (compare x y EGAL)); [
+  Intros E; Rewrite (compare_convert_EGAL x y E); 
+  Intros H;Absurd (lt (convert y) (convert y)); [ Apply lt_n_n | Assumption ]
+| Intros H;Elim H; [
+    Intros H1 H2; Absurd (lt (convert y) (convert x)); [
+      Apply lt_not_sym; Apply compare_convert_INFERIEUR; Assumption
+    | Assumption ]
+  | Auto]].
+Qed.
+
+(** [nat_of_P] is strictly positive *)
+
+Lemma compare_positive_to_nat_O : 
+	(p:positive)(m:nat)(le m (positive_to_nat p m)).
+NewInduction p; Simpl; Auto with arith.
+Intro m; Apply le_trans with (plus m m);  Auto with arith.
+Qed.
+
+Lemma compare_convert_O : (p:positive)(lt O (convert p)).
+Intro; Unfold convert; Apply lt_le_trans with (S O); Auto with arith.
+Apply compare_positive_to_nat_O.
+Qed.
+
+(** Pmult_nat permutes with multiplication *)
+
+Lemma positive_to_nat_mult : (p:positive) (n,m:nat)
+    (positive_to_nat p (mult m n))=(mult m (positive_to_nat p n)).
+Proof.
+  Induction p. Intros. Simpl. Rewrite mult_plus_distr_r. Rewrite <- (mult_plus_distr_r m n n).
+  Rewrite (H (plus n n) m). Reflexivity.
+  Intros. Simpl. Rewrite <- (mult_plus_distr_r m n n). Apply H.
+  Trivial.
+Qed.
+
+Lemma positive_to_nat_2 : (p:positive)
+    (positive_to_nat p (2))=(mult (2) (positive_to_nat p (1))).
+Proof.
+  Intros. Rewrite <- positive_to_nat_mult. Reflexivity.
+Qed.
+
+Lemma positive_to_nat_4 : (p:positive)
+    (positive_to_nat p (4))=(mult (2) (positive_to_nat p (2))).
+Proof.
+  Intros. Rewrite <- positive_to_nat_mult. Reflexivity.
+Qed.
+
+(** Mapping of xH, xO and xI through [nat_of_P] *)
+
+Lemma convert_xH : (convert xH)=(1).
+Proof.
+  Reflexivity.
+Qed.
+
+Lemma convert_xO : (p:positive) (convert (xO p))=(mult (2) (convert p)).
+Proof.
+  Induction p. Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2.
+  Rewrite positive_to_nat_4. Rewrite H. Simpl. Rewrite <- plus_Snm_nSm. Reflexivity.
+  Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4.
+  Rewrite H. Reflexivity.
+  Reflexivity.
+Qed.
+
+Lemma convert_xI : (p:positive) (convert (xI p))=(S (mult (2) (convert p))).
+Proof.
+  Induction p. Unfold convert. Simpl. Intro p0. Intro. Rewrite positive_to_nat_2.
+  Rewrite positive_to_nat_4; Injection H; Intro H1; Rewrite H1; Rewrite <- plus_Snm_nSm; Reflexivity.
+  Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4.
+  Injection H; Intro H1; Rewrite H1; Reflexivity.
+  Reflexivity.
+Qed.
+
+(**********************************************************************)
+(** Properties of the shifted injection from Peano natural numbers to 
+    binary positive numbers *)
+
+(** Composition of [P_of_succ_nat] and [nat_of_P] is successor on [nat] *)
+
+Theorem bij1 : (m:nat) (convert (anti_convert m)) = (S m).
+Proof.
+Intro m; NewInduction m as [|n H]; [
+  Reflexivity
+| Simpl; Rewrite cvt_add_un; Rewrite H; Auto ].
+Qed.
+
+(** Miscellaneous lemmas on [P_of_succ_nat] *)
+
+Lemma ZL3: (x:nat) (add_un (anti_convert (plus x x))) =  (xO (anti_convert x)).
+Proof.
+Intro x; NewInduction x as [|n H]; [
+  Simpl; Auto with arith
+| Simpl; Rewrite  plus_sym; Simpl; Rewrite  H; Rewrite  ZL1;Auto with arith].
+Qed.
+
+Lemma ZL5: (x:nat) (anti_convert (plus (S x) (S x))) =  (xI (anti_convert x)).
+Proof.
+Intro x; NewInduction x as [|n H];Simpl; [
+  Auto with arith
+| Rewrite <- plus_n_Sm; Simpl; Simpl in H; Rewrite H; Auto with arith].
+Qed.
+
+(** Composition of [nat_of_P] and [P_of_succ_nat] is successor on [positive] *)
+
+Theorem bij2 : (x:positive) (anti_convert (convert x)) = (add_un x).
+Proof.
+Intro x; NewInduction x as [p H|p H|]; [
+  Simpl; Rewrite <- H; Change (2) with (plus (1) (1));
+  Rewrite ZL2; Elim (ZL4 p); 
+  Unfold convert; Intros n H1;Rewrite H1; Rewrite ZL3; Auto with arith
+| Unfold convert ;Simpl; Change (2) with (plus (1) (1));
+  Rewrite ZL2;
+  Rewrite <- (sub_add_one
+               (anti_convert
+                 (plus (positive_to_nat p (S O)) (positive_to_nat p (S O)))));
+  Rewrite <- (sub_add_one (xI p));
+  Simpl;Rewrite <- H;Elim (ZL4 p); Unfold convert ;Intros n H1;Rewrite H1;
+  Rewrite ZL5; Simpl; Trivial with arith
+| Unfold convert; Simpl; Auto with arith ].
+Qed.
+
+(** Composition of [nat_of_P], [P_of_succ_nat] and [Ppred] is identity
+    on [positive] *)
+
+Theorem bij3: (x:positive)(sub_un (anti_convert (convert x))) = x.
+Proof.
+Intros x; Rewrite bij2; Rewrite sub_add_one; Trivial with arith.
+Qed.
+
+(**********************************************************************)
+(** Extra properties of the injection from binary positive numbers to Peano 
+    natural numbers *)
+
+(** [nat_of_P] is a morphism for subtraction on positive numbers *)
+
+Theorem true_sub_convert:
+  (x,y:positive) (compare x y EGAL) = SUPERIEUR -> 
+     (convert (true_sub x y)) = (minus (convert x) (convert y)).
+Proof.
+Intros x y H; Apply plus_reg_l with (convert y);
+Rewrite le_plus_minus_r; [
+  Rewrite <- convert_add; Rewrite sub_add; Auto with arith
+| Apply lt_le_weak; Exact (compare_convert_SUPERIEUR x y H)].
+Qed.
+
+(** [nat_of_P] is injective *)
+
+Lemma convert_intro : (x,y:positive)(convert x)=(convert y) -> x=y.
+Proof.
+Intros x y H;Rewrite <- (bij3 x);Rewrite <- (bij3 y); Rewrite H; Trivial with arith.
+Qed.
+
+Lemma ZL16: (p,q:positive)(lt (minus (convert p) (convert q)) (convert p)).
+Proof.
+Intros p q; Elim (ZL4 p);Elim (ZL4 q); Intros h H1 i H2; 
+Rewrite H1;Rewrite H2; Simpl;Unfold lt; Apply le_n_S; Apply le_minus.
+Qed.
+
+Lemma ZL17: (p,q:positive)(lt (convert p) (convert (add p q))).
+Proof.
+Intros p q; Rewrite convert_add;Unfold lt;Elim (ZL4 q); Intros k H;Rewrite H;
+Rewrite plus_sym;Simpl; Apply le_n_S; Apply le_plus_r.
+Qed.
+
+(** Comparison and subtraction *)
+
+Lemma compare_true_sub_right :
+  (p,q,z:positive)
+  (compare q p EGAL)=INFERIEUR->
+  (compare z p EGAL)=SUPERIEUR->
+  (compare z q EGAL)=SUPERIEUR->
+  (compare (true_sub z p) (true_sub z q) EGAL)=INFERIEUR.
+Proof.
+Intros; Apply convert_compare_INFERIEUR; Rewrite true_sub_convert; [
+  Rewrite true_sub_convert; [
+    Apply simpl_lt_plus_l with p:=(convert q); Rewrite le_plus_minus_r; [
+      Rewrite plus_sym; Apply simpl_lt_plus_l with p:=(convert p);
+        Rewrite plus_assoc_l; Rewrite le_plus_minus_r; [
+          Rewrite (plus_sym (convert p)); Apply lt_reg_l;
+          Apply compare_convert_INFERIEUR; Assumption 
+        | Apply lt_le_weak; Apply compare_convert_INFERIEUR;
+          Apply ZC1; Assumption ]
+      | Apply lt_le_weak;Apply compare_convert_INFERIEUR;
+        Apply ZC1; Assumption ]
+    | Assumption ]
+  | Assumption ].
+Qed.
+
+Lemma compare_true_sub_left :
+  (p,q,z:positive)
+  (compare q p EGAL)=INFERIEUR->
+  (compare p z EGAL)=SUPERIEUR->
+  (compare q z EGAL)=SUPERIEUR->
+  (compare (true_sub q z) (true_sub p z) EGAL)=INFERIEUR.
+Proof.
+Intros p q z; Intros; 
+  Apply convert_compare_INFERIEUR; Rewrite true_sub_convert; [
+  Rewrite true_sub_convert; [
+    Unfold gt; Apply simpl_lt_plus_l with p:=(convert z);
+    Rewrite le_plus_minus_r; [
+      Rewrite le_plus_minus_r; [
+        Apply compare_convert_INFERIEUR;Assumption
+      | Apply lt_le_weak; Apply compare_convert_INFERIEUR;Apply ZC1;Assumption]
+    | Apply lt_le_weak; Apply compare_convert_INFERIEUR;Apply ZC1; Assumption]
+  | Assumption]
+| Assumption].
+Qed.
+
+(** Distributivity of multiplication over subtraction *)
+
+Theorem times_true_sub_distr:
+  (x,y,z:positive) (compare y z EGAL) = SUPERIEUR -> 
+      (times x (true_sub y z)) = (true_sub (times x y) (times x z)).
+Proof.
+Intros x y z H; Apply convert_intro;
+Rewrite times_convert; Rewrite true_sub_convert; [
+  Rewrite true_sub_convert; [
+    Do 2 Rewrite times_convert;
+    Do 3 Rewrite (mult_sym (convert x));Apply mult_minus_distr
+  | Apply convert_compare_SUPERIEUR; Do 2 Rewrite times_convert; 
+    Unfold gt; Elim (ZL4 x);Intros h H1;Rewrite H1; Apply lt_mult_left;
+    Exact (compare_convert_SUPERIEUR y z H) ]
+| Assumption ].
+Qed.
+