Structuration de fast_integer en operations sur positive, proprietes des operations sur positive, operations sur Z, proprietes des operations sur Z; suppression section; true_sub devient definition

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

1 files changed, 1017 insertions, 679 deletions

diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v
index 60fdca1df..26a5a738e 100644
--- a/theories/ZArith/fast_integer.v
+++ b/theories/ZArith/fast_integer.v
@@ -8,15 +8,12 @@
 
 (*i $Id$ i*)
 
+(***********************************************************)
 (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
+(***********************************************************)
 
-Require Le.
-Require Lt.
-Require Plus.
-Require Mult.
-Require Minus.
-
-(** Definition of fast binary integers *)
+(**********************************************************************)
+(** Binary positive numbers *)
 
 Inductive positive : Set :=
   xI : positive -> positive
@@ -31,72 +28,47 @@ Bind Scope positive_scope with positive.
 Arguments Scope xO [ positive_scope ].
 Arguments Scope xI [ positive_scope ].
 
-Inductive Z : Set := 
-  ZERO : Z | POS : positive -> Z | NEG : positive -> Z.
-
-(* Declare Scope positive_scope with Key Z *)
-Delimits Scope Z_scope with Z.
+(** Successor *)
 
-(* Automatically open scope Z_scope for arguments of type Z, POS and NEG *)
-Bind Scope Z_scope with Z.
-Arguments Scope POS [ Z_scope ].
-Arguments Scope NEG [ Z_scope ].
-
-Section fast_integers.
-
-Inductive relation : Set := 
-  EGAL :relation | INFERIEUR : relation | SUPERIEUR : relation.
+Fixpoint add_un [x:positive]:positive :=
+  Cases x of
+    (xI x') => (xO (add_un x'))
+  | (xO x') => (xI x')
+  | xH => (xO xH)
+  end.
 
 (** Addition *)
-Fixpoint add_un [x:positive]:positive :=
-  <positive> Cases x of
-               (xI x') => (xO (add_un x'))
-             | (xO x') => (xI x')
-             | xH => (xO xH)
-             end.
 
-Fixpoint add [x,y:positive]:positive :=
-  <positive>Cases x of
-     (xI x') => <positive>Cases y of
-                    (xI y') => (xO (add_carry x' y'))
-                  | (xO y') => (xI (add x' y'))
-                  | xH      => (xO (add_un x'))
-                  end
-   | (xO x') => <positive>Cases y of
-                    (xI y') => (xI (add x' y'))
-                  | (xO y') => (xO (add x' y'))
-                  | xH      => (xI x')
-                  end
-   | xH      => <positive>Cases y of
-                    (xI y') => (xO (add_un y'))
-                  | (xO y') => (xI y')
-                  | xH      => (xO xH)
-                  end
-   end
-with add_carry [x,y:positive]:positive :=
-  <positive>Cases x of
-     (xI x') => <positive>Cases y of
-            (xI y') => (xI (add_carry x' y'))
-          | (xO y') => (xO (add_carry x' y'))
-          | xH      => (xI (add_un x'))
-          end
-   | (xO x') => <positive>Cases y of
-            (xI y') => (xO (add_carry x' y'))
-          | (xO y') => (xI (add x' y'))
-          | xH      => (xO (add_un x'))
-          end
-   | xH      => <positive>Cases y of
-            (xI y') => (xI (add_un y'))
-          | (xO y') => (xO (add_un y'))
-          | xH      => (xI xH)
-          end
+Fixpoint add [x:positive]:positive -> positive := [y:positive]
+  Cases x y of
+  | (xI x') (xI y') => (xO (add_carry x' y'))
+  | (xI x') (xO y') => (xI (add x' y'))
+  | (xI x') xH      => (xO (add_un x'))
+  | (xO x') (xI y') => (xI (add x' y'))
+  | (xO x') (xO y') => (xO (add x' y'))
+  | (xO x') xH      => (xI x')
+  | xH      _       => (add_un y)
+  end
+with add_carry [x:positive]:positive -> positive := [y:positive]
+  Cases x y of
+  | (xI x') (xI y') => (xI (add_carry x' y'))
+  | (xI x') (xO y') => (xO (add_carry x' y'))
+  | (xI x') xH      => (xI (add_un x'))
+  | (xO x') (xI y') => (xO (add_carry x' y'))
+  | (xO x') (xO y') => (xI (add x' y'))
+  | (xO x') xH      => (xO (add_un x'))
+  | xH      (xI y') => (xI (add_un y'))
+  | xH      (xO y') => (xO (add_un y'))
+  | xH      xH      => (xI xH)
   end.
 
+V7only [Infix LEFTA 4 "+" add : positive_scope.].
 V8Infix "+" add : positive_scope.
 
-(*Open Scope positive_scope.*)
+Open Local Scope positive_scope.
+
+(** From binary positive numbers to Peano natural numbers *)
 
-(** From positive to natural numbers *)
 Fixpoint positive_to_nat [x:positive]:nat -> nat :=
   [pow2:nat]
     <nat> Cases x of
@@ -107,20 +79,600 @@ Fixpoint positive_to_nat [x:positive]:nat -> nat :=
 
 Definition convert := [x:positive] (positive_to_nat x (S O)).
 
-(** From natural numbers to positive *)
+(** From Peano natural numbers to binary positive numbers *)
+
 Fixpoint anti_convert [n:nat]: positive :=
-  <positive> Cases n of
+   Cases n of
                 O => xH
              | (S x') => (add_un (anti_convert x'))
              end.
 
-(* Correctness of addition *)
+(** Subtraction *)
+
+Fixpoint double_moins_un [x:positive]:positive :=
+  Cases x of
+      (xI x') => (xI (xO x'))
+    | (xO x') => (xI (double_moins_un x'))
+    | xH => xH
+    end.
+
+(** Predecessor *)
+
+Definition sub_un := [x:positive]
+   Cases x of
+             (xI x') => (xO x')
+           | (xO x') => (double_moins_un x')
+           | xH => xH
+           end.
+
+(** An auxiliary type for subtraction *)
+
+Inductive positive_mask: Set :=
+   IsNul : positive_mask
+ | IsPos : positive -> positive_mask
+ | IsNeg : positive_mask.
+
+(** Operation x -> 2*x+1 *)
+
+Definition Un_suivi_de := [x:positive_mask]
+  Cases x of IsNul => (IsPos xH) | IsNeg => IsNeg | (IsPos p) => (IsPos (xI p)) end.
+
+(** Operation x -> 2*x *)
+
+Definition Zero_suivi_de := [x:positive_mask]
+  Cases x of IsNul => IsNul | IsNeg => IsNeg | (IsPos p) => (IsPos (xO p)) end.
+
+(** Operation x -> 2*x-2 *)
+
+Definition double_moins_deux :=
+  [x:positive] Cases x of
+           (xI x') => (IsPos (xO (xO x')))
+         | (xO x') => (IsPos (xO (double_moins_un x')))
+         | xH => IsNul
+         end.
+
+(** Subtraction of binary positive numbers into a positive numbers mask *)
+
+Fixpoint sub_pos[x,y:positive]:positive_mask :=
+  Cases x y of
+  | (xI x') (xI y') => (Zero_suivi_de (sub_pos x' y'))
+  | (xI x') (xO y') => (Un_suivi_de (sub_pos x' y'))
+  | (xI x') xH      => (IsPos (xO x'))
+  | (xO x') (xI y') => (Un_suivi_de (sub_neg x' y'))
+  | (xO x') (xO y') => (Zero_suivi_de (sub_pos x' y'))
+  | (xO x') xH      => (IsPos (double_moins_un x'))
+  | xH      xH      => IsNul
+  | xH      _       => IsNeg
+  end
+with sub_neg [x,y:positive]:positive_mask :=
+  Cases x y of
+    (xI x') (xI y') => (Un_suivi_de (sub_neg x' y'))
+  | (xI x') (xO y') => (Zero_suivi_de (sub_pos x' y'))
+  | (xI x') xH      => (IsPos (double_moins_un x'))
+  | (xO x') (xI y') => (Zero_suivi_de (sub_neg x' y'))
+  | (xO x') (xO y') => (Un_suivi_de (sub_neg x' y'))
+  | (xO x') xH      => (double_moins_deux x')
+  | xH      _       => IsNeg
+  end.
+
+(** Subtraction of binary positive numbers x and y, returns 1 if x<=y *)
+
+Definition true_sub := [x,y:positive] 
+  Cases (sub_pos x y) of (IsPos z) => z | _ => xH  end.
+
+(** Multiplication on binary positive numbers *)
+
+Fixpoint times [x:positive] : positive -> positive:=
+  [y:positive]
+  Cases x of
+    (xI x') => (add y (xO (times x' y)))
+  | (xO x') => (xO (times x' y))
+  | xH => y
+  end.
+
+V8Infix "*" times : positive_scope.
+
+(**********************************************************************)
+(** Comparison on binary positive numbers *)
+
+Inductive relation : Set := 
+  EGAL :relation | INFERIEUR : relation | SUPERIEUR : relation.
+
+Definition Op := [r:relation]
+  Cases r of
+    EGAL => EGAL
+  | INFERIEUR => SUPERIEUR
+  | SUPERIEUR => INFERIEUR
+  end.
+
+(** Comparison of binary positive numbers *)
+
+Fixpoint compare [x,y:positive]: relation -> relation :=
+  [r:relation] 
+  Cases x y of
+  | (xI x') (xI y') => (compare x' y' r)
+  | (xI x') (xO y') => (compare x' y' SUPERIEUR)
+  | (xI x')  xH     => SUPERIEUR
+  | (xO x') (xI y') => (compare x' y' INFERIEUR)
+  | (xO x') (xO y') => (compare x' y' r)
+  | (xO x')  xH     => SUPERIEUR
+  | xH      (xI y') => INFERIEUR
+  | xH      (xO y') => INFERIEUR
+  | xH       xH     => r
+  end.
+
+Theorem compare_convert1 : 
+ (x,y:positive) 
+  ~(compare x y SUPERIEUR) = EGAL /\ ~(compare x y INFERIEUR) = EGAL.
+Proof.
+Induction x;Induction y;Split;Simpl;Auto;
+  Discriminate Orelse (Elim (H p0); Auto).
+Qed.
+
+Theorem compare_convert_EGAL : (x,y:positive) (compare x y EGAL) = EGAL -> x=y.
+Proof.
+Induction x;Induction y;Simpl;Auto; [
+  Intros z H1 H2; Rewrite (H z); Trivial
+| Intros z H1 H2; Absurd (compare p z SUPERIEUR)=EGAL ;
+   [ Elim (compare_convert1 p z);Auto | Assumption ]
+| Intros H1;Discriminate H1
+| Intros z H1 H2; Absurd (compare p z INFERIEUR) = EGAL; 
+    [ Elim (compare_convert1 p z);Auto | Assumption ]
+| Intros z H1 H2 ;Rewrite (H z);Auto 
+| Intros H1;Discriminate H1
+| Intros p H H1;Discriminate H1
+| Intros p H H1;Discriminate H1 ].
+Qed.
+
+Lemma ZLSI:
+ (x,y:positive) (compare x y SUPERIEUR) = INFERIEUR -> 
+                (compare x y EGAL) = INFERIEUR.
+Proof.
+Induction x;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.
+Induction x;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.
+(Induction x;Induction y;Simpl;Auto;Try Discriminate);
+ Intros z H1 H2; Elim (H z 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.
+(Induction x;Induction y;Simpl;Auto;Try Discriminate);
+ Intros z H1 H2; Elim (H z H2);Auto; Intros E;Rewrite E;
+ Auto.
+Qed.
+
+Lemma Dcompare : (r:relation) r=EGAL \/ r = INFERIEUR \/ r = SUPERIEUR.
+Proof.
+Induction r; Auto. 
+Qed.
+
+Theorem convert_compare_EGAL: (x:positive)(compare x x EGAL)=EGAL.
+Induction x; Auto.
+Qed.
+
+(**********************************************************************)
+(** Miscellaneous properties of binary positive numbers *)
+
+Lemma ZL11: (x:positive) (x=xH) \/ ~(x=xH).
+Proof.
+Intros x;Case x;Intros; (Left;Reflexivity) Orelse (Right;Discriminate).
+Qed.
+
+(**********************************************************************)
+(** Properties of successor on binary positive numbers *)
+
+(** Specification of [xI] in term of [Psucc] and [xO] *)
+
+Lemma xI_add_un_xO : (p:positive)(xI p) = (add_un (xO p)).
+Proof.
+Reflexivity.
+Qed.
+
+(** Successor and double *)
+
+Lemma is_double_moins_un : (x:positive) (add_un (double_moins_un x)) = (xO x).
+Proof.
+NewInduction x as [x IHx|x|]; Simpl; Try Rewrite IHx; Reflexivity.
+Qed.
+
+Lemma double_moins_un_add_un_xI : 
+ (x:positive)(double_moins_un (add_un x))=(xI x).
+Proof.
+NewInduction x as [x IHx|x|]; Simpl; Try Rewrite IHx; Reflexivity.
+Qed.
+
+Lemma ZL1: (y:positive)(xO (add_un y)) = (add_un (add_un (xO y))).
+Proof.
+Induction y; Simpl; Auto.
+Qed.
+
+(** Successor and predecessor *)
+
+Lemma add_un_not_un : (x:positive) (add_un x) <> xH.
+Proof.
+NewDestruct x as [x|x|]; Discriminate.
+Qed.
+
+Lemma sub_add_one : (x:positive) (sub_un (add_un x)) = x.
+Proof.
+(Induction x; [Idtac | Idtac | Simpl;Auto]);
+(Intros p; Elim p; [Idtac | Idtac | Simpl;Auto]);
+Simpl; Intros q H1 H2; Case H2; Simpl; Trivial.
+Qed.
+
+Lemma add_sub_one : (x:positive) (x=xH) \/ (add_un (sub_un x)) = x.
+Proof.
+Induction x; [
+  Simpl; Auto
+| Simpl; Intros;Right;Apply is_double_moins_un
+| Auto ].
+Qed.
+
+(** Injectivity of successor *)
+
+Lemma add_un_inj : (x,y:positive) (add_un x)=(add_un y) -> x=y.
+Proof.
+NewInduction x; NewDestruct y as [y|y|]; Simpl; 
+  Intro H; Discriminate H Orelse Try (Injection H; Clear H; Intro H).
+Rewrite (IHx y H); Reflexivity.
+Absurd (add_un x)=xH; [ Apply add_un_not_un | Assumption ].
+Apply f_equal with 1:=H; Assumption.
+Absurd (add_un y)=xH; [ Apply add_un_not_un | Symmetry; Assumption ].
+Reflexivity.
+Qed.
+
+(**********************************************************************)
+(** Properties of addition on binary positive numbers *)
+
+(** Specification of [Psucc] in term of [Pplus] *)
+
+Lemma ZL12: (q:positive) (add_un q) = (add q xH).
+Proof.
+NewDestruct q; Reflexivity.
+Qed.
+
+Lemma ZL12bis: (q:positive) (add_un q) = (add xH q).
+Proof.
+Reflexivity.
+Qed.
+
+(** Specification of [Pplus_carry] *)
+
+Theorem ZL13: (x,y:positive)(add_carry x y) = (add_un (add x y)).
+Proof.
+(Induction x;Induction y;Simpl;Auto); Intros q H1;Rewrite H;
+ Auto.
+Qed.
+
+(** Commutativity *)
+
+Theorem add_sym : (x,y:positive) (add x y) = (add y x).
+Proof.
+Induction x;Induction y;Simpl;Auto; Intros q H1; [
+  Clear  H1; Do 2 Rewrite ZL13; Rewrite H;Auto
+| Rewrite H;Auto | Rewrite H;Auto | Rewrite H;Auto ].
+Qed. 
+
+(** Permutation of [Pplus] and [Psucc] *)
+
+Theorem ZL14: (x,y:positive)(add x (add_un y)) = (add_un (add x y)).
+Proof.
+Induction x;Induction y;Simpl;Auto; [
+  Intros q H1; Rewrite ZL13; Rewrite  H; Auto
+| Intros q H1; Rewrite ZL13; Auto
+| Elim p;Simpl;Auto
+| Intros q H1;Rewrite H;Auto
+| Elim p;Simpl;Auto ].
+Qed.
+
+Theorem ZL14bis: (x,y:positive)(add (add_un x) y) = (add_un (add x y)).
+Proof.
+Intros x y; Rewrite add_sym; Rewrite add_sym with x:=x; Apply ZL14.
+Qed.
+
+Theorem ZL15: (q,z:positive) ~z=xH -> (add_carry q (sub_un z)) = (add q z).
+Proof.
+Intros q z H; Elim (add_sub_one z); [
+  Intro;Absurd z=xH;Auto
+| Intros E;Pattern 2 z ;Rewrite <- E; Rewrite ZL14; Rewrite ZL13; Trivial ].
+Qed. 
+
+(** No neutral for addition on strictly positive numbers *)
+
+Lemma add_no_neutral : (x,y:positive) ~(add y x)=x.
+Proof.
+NewInduction x; NewDestruct y as [y|y|]; Simpl; Intro H;
+  Discriminate H Orelse Injection H; Clear H; Intro H; Apply (IHx y H).
+Qed.
+
+Lemma add_carry_not_add_un : (x,y:positive) ~(add_carry y x)=(add_un x).
+Proof.
+Intros x y H; Absurd (add y x)=x; 
+      [ Apply add_no_neutral
+      | Apply add_un_inj; Rewrite <- ZL13; Assumption ].
+Qed.
+
+(** Simplification *)
+
+Lemma add_carry_add :
+  (x,y,z,t:positive) (add_carry x z)=(add_carry y t) -> (add x z)=(add y t).
+Proof.
+Intros x y z t H; Apply add_un_inj; Do 2 Rewrite <- ZL13; Assumption.
+Qed.
+
+Lemma simpl_add_r : (x,y,z:positive) (add x z)=(add y z) -> x=y.
+Proof.
+Intros x y z; Generalize x y; Clear x y.
+NewInduction z as [z|z|].
+  NewDestruct x as [x|x|]; NewDestruct y as [y|y|]; Simpl; Intro H; 
+  Discriminate H Orelse Try (Injection H; Clear H; Intro H).
+    Rewrite IHz with 1:=(add_carry_add ? ? ? ? H); Reflexivity.
+    Absurd (add_carry x z)=(add_un z);
+      [ Apply add_carry_not_add_un | Assumption ].
+    Rewrite IHz with 1:=H; Reflexivity.
+    Symmetry in H; Absurd (add_carry y z)=(add_un z);
+      [ Apply add_carry_not_add_un | Assumption ].
+    Reflexivity.
+  NewDestruct x as [x|x|]; NewDestruct y as [y|y|]; Simpl; Intro H; 
+  Discriminate H Orelse Try (Injection H; Clear H; Intro H).
+    Rewrite IHz with 1:=H; Reflexivity.
+    Absurd (add x z)=z; [ Apply add_no_neutral | Assumption ].
+    Rewrite IHz with 1:=H; Reflexivity.
+    Symmetry in H; Absurd y+z=z; [ Apply add_no_neutral | Assumption ].
+    Reflexivity.
+  Intros H x y; Apply add_un_inj; Do 2 Rewrite ZL12; Assumption.
+Qed.
+
+Lemma simpl_add_carry_r :
+ (x,y,z:positive) (add_carry x z)=(add_carry y z) -> x=y.
+Proof.
+Intros x y z H; Apply simpl_add_r with z:=z; Apply add_carry_add; Assumption.
+Qed.
+
+Lemma simpl_add_l : (x,y,z:positive) (add x y)=(add x z) -> y=z.
+Proof.
+Intros x y z H;Apply simpl_add_r with z:=x; 
+  Rewrite add_sym with x:=z; Rewrite add_sym with x:=y; Assumption.
+Qed.
+
+Lemma simpl_add_carry_l :
+  (x,y,z:positive) (add_carry x y)=(add_carry x z) -> y=z.
+Proof.
+Intros x y z H;Apply simpl_add_r with z:=x; 
+Rewrite add_sym with x:=z; Rewrite add_sym with x:=y; Apply add_carry_add; 
+Assumption.
+Qed.
+
+(** Addition on positive is associative *)
+
+Theorem add_assoc: (x,y,z:positive)(add x (add y z)) = (add (add x y) z).
+Proof.
+Intros x y; Generalize x; Clear x.
+NewInduction y as [y|y|].
+  NewDestruct x as [x|x|]; NewDestruct z as [z|z|]; Simpl; Repeat Rewrite ZL13;
+    Repeat Rewrite ZL14; Repeat Rewrite ZL14bis; Reflexivity Orelse
+    Repeat Apply f_equal with A:=positive; Apply IHy.
+  NewDestruct x as [x|x|]; NewDestruct z as [z|z|]; Simpl; Repeat Rewrite ZL13;
+    Repeat Rewrite ZL14; Repeat Rewrite ZL14bis; Reflexivity Orelse
+    Repeat Apply f_equal with A:=positive; Apply IHy.
+  Intros x z; Rewrite add_sym with x:=xH; Do 2 Rewrite <- ZL12; Rewrite ZL14bis; Rewrite ZL14; Reflexivity.
+Qed.
+
+(** Commutation of addition with the double of a positive number *)
+
+Lemma xO_xI_plus_double_moins_un :
+  (p,q:positive) (xO (add p q)) = (add (xI p) (double_moins_un q)).
+Proof.
+NewDestruct q; Simpl.
+  Rewrite ZL13; Rewrite <- ZL14; Reflexivity.
+  Rewrite ZL13; Rewrite <- ZL14; Rewrite -> is_double_moins_un;
+    Reflexivity.
+  Rewrite -> ZL12; Reflexivity.
+Qed.
+
+Lemma double_moins_un_plus_xO_double_moins_un :
+ (p,q:positive) (double_moins_un (add p q)) = (add (xO p) (double_moins_un q)).
+Proof.
+NewInduction p as [p|p|]; NewDestruct q as [q|q|]; Simpl;
+  Try Rewrite ZL13; Try Rewrite is_double_moins_un; 
+  Try Rewrite double_moins_un_add_un_xI; Try Reflexivity.
+  NewDestruct q; Simpl.
+    Rewrite ZL13; Rewrite <- ZL14; Reflexivity.
+    Rewrite ZL13; Rewrite <- ZL14; Rewrite is_double_moins_un;
+      Reflexivity.
+    Rewrite ZL12; Reflexivity.
+  Rewrite IHp; Reflexivity.
+Qed.
+
+Lemma add_xI_double_moins_un :
+  (p,q:positive)(xO (add p q)) = (add (xI p) (double_moins_un q)).
+Proof.
+Intros; Change (xI p) with (add (xO p) xH).
+Rewrite <- add_assoc; Rewrite <- ZL12bis; Rewrite is_double_moins_un.
+Reflexivity.
+Qed.
+
+Lemma double_moins_un_add :
+  (p,q:positive)(double_moins_un (add p q)) = (add (xO p) (double_moins_un q)).
+Proof.
+NewInduction p as [p|p|]; NewDestruct q as [q|q|]; 
+ Simpl; Try Rewrite ZL13; Try Rewrite double_moins_un_add_un_xI;
+ Try Rewrite is_double_moins_un; Try Rewrite IHp; 
+ Try Rewrite add_xI_double_moins_un; Reflexivity.
+Qed.
+
+(** Misc *)
+
+Lemma add_x_x : (x:positive) (add x x) = (xO x).
+Proof.
+NewInduction x; Simpl; Try Rewrite ZL13; Try Rewrite IHx; Reflexivity.
+Qed.
+
+(**********************************************************************)
+(** Properties of minus on binary positive numbers *)
+
+(* Properties of subtraction *)
+
+Lemma ZS: (p:positive_mask) (Zero_suivi_de p) = IsNul -> p = IsNul.
+Proof.
+NewDestruct p; Simpl; [ Trivial | Discriminate 1 | Discriminate 1 ].
+Qed.
+
+Lemma US: (p:positive_mask) ~(Un_suivi_de p)=IsNul.
+Proof.
+Induction p; Intros; Discriminate.
+Qed.
+
+Lemma USH: (p:positive_mask) (Un_suivi_de p) = (IsPos xH) -> p = IsNul.
+Proof.
+NewDestruct p; Simpl; [ Trivial | Discriminate 1 | Discriminate 1 ].
+Qed.
+
+Lemma ZSH: (p:positive_mask) ~(Zero_suivi_de p)= (IsPos xH).
+Proof.
+Induction p; Intros; Discriminate.
+Qed.
+
+Theorem sub_pos_x_x : (x:positive) (sub_pos x x) = IsNul.
+Proof.
+Induction x; [
+  Simpl; Intros p H;Rewrite H;Simpl; Trivial
+| Intros p H;Simpl;Rewrite H;Auto
+| Auto ].
+Qed.
+
+Theorem ZL10: (x,y:positive)
+ (sub_pos x y) = (IsPos xH) -> (sub_neg x y) = IsNul.
+Proof.
+NewInduction x as [p|p|]; NewDestruct y as [q|q|]; Simpl; Intro H;
+Try Discriminate H; [
+  Absurd (Zero_suivi_de (sub_pos p q))=(IsPos xH); [ Apply ZSH | Assumption ]
+| Assert Heq : (sub_pos p q)=IsNul;
+   [ Apply USH;Assumption | Rewrite Heq; Reflexivity ]
+| Assert Heq : (sub_neg p q)=IsNul;
+   [ Apply USH;Assumption | Rewrite Heq; Reflexivity ]
+| Absurd (Zero_suivi_de (sub_pos p q))=(IsPos xH); [ Apply ZSH | Assumption ]
+| NewDestruct p; Simpl; [ Discriminate H | Discriminate H | Reflexivity ] ].
+Qed.
+
+(* Properties valid only for x>y *)
+
+Theorem sub_pos_SUPERIEUR:
+  (x,y:positive)(compare x y EGAL)=SUPERIEUR -> 
+    (EX h:positive | (sub_pos x y) = (IsPos h) /\ (add y h) = x /\
+                     (h = xH \/ (sub_neg x y) = (IsPos (sub_un h)))).
+Proof.
+NewInduction x as [p|p|];NewDestruct y as [q|q|]; Simpl; Intro H;
+  Try Discriminate H.
+  NewDestruct (IHp q H) as [z [H4 [H6 H7]]]; Exists (xO z); Split.
+    Rewrite H4; Reflexivity.
+    Split.
+      Simpl; Rewrite H6; Reflexivity.
+      Right; Clear H6; NewDestruct (ZL11 z) as [H8|H8]; [
+        Rewrite H8; Rewrite H8 in H4;
+        Rewrite ZL10; [ Reflexivity | Assumption ]
+      | Clear H4; NewDestruct H7 as [H9|H9]; [
+          Absurd z=xH; Assumption
+        | Rewrite H9; Clear H9; NewDestruct z; 
+            [ Reflexivity | Reflexivity | Absurd xH=xH; Trivial ]]].
+  Case ZLSS with 1:=H; [
+    Intros H3;Elim (IHp q H3); Intros z H4; Exists (xI z);
+    Elim H4;Intros H5 H6;Elim H6;Intros H7 H8; Split; [
+      Simpl;Rewrite H5;Auto
+    | Split; [
+        Simpl; Rewrite H7; Trivial
+      | Right;Change (Zero_suivi_de (sub_pos p q))=(IsPos (sub_un (xI z)));
+        Rewrite H5; Auto ]]
+  | Intros H3; Exists xH; Rewrite H3; Split; [
+      Simpl; Rewrite sub_pos_x_x; Auto
+    | Split; Auto ]].
+  Exists (xO p); Auto.
+  NewDestruct (IHp q) as [z [H4 [H6 H7]]].
+    Apply ZLIS; Assumption.
+    NewDestruct (ZL11 z) as [vZ|]; [
+      Exists xH; Split; [
+        Rewrite ZL10; [ Reflexivity | Rewrite vZ in H4;Assumption ]
+      | Split; [
+          Simpl; Rewrite ZL12; Rewrite <- vZ; Rewrite H6; Trivial
+        | Auto ]]
+    | Exists (xI (sub_un z)); NewDestruct H7 as [|H8];[
+        Absurd z=xH;Assumption
+      | Split; [
+          Rewrite H8; Trivial
+        | Split; [ Simpl; Rewrite ZL15; [
+              Rewrite H6;Trivial
+            | Assumption ]
+          | Right; Rewrite H8; Reflexivity]]]].
+  NewDestruct (IHp q H) as [z [H4 [H6 H7]]].
+  Exists (xO z); Split; [
+    Rewrite H4;Auto
+  | Split; [
+      Simpl;Rewrite H6;Reflexivity
+    | Right; Change (Un_suivi_de (sub_neg p q))=(IsPos (double_moins_un z));
+      NewDestruct (ZL11 z) as [H8|H8]; [
+        Rewrite H8; Simpl;
+        Assert H9:(sub_neg p q)=IsNul;[
+          Apply ZL10;Rewrite <- H8;Assumption
+        | Rewrite H9;Reflexivity ]
+      | NewDestruct H7 as [H9|H9]; [
+          Absurd z=xH;Auto
+        | Rewrite H9; NewDestruct z; Simpl; 
+            [ Reflexivity
+            | Reflexivity
+            | Absurd xH=xH; [Assumption | Reflexivity]]]]]].
+  Exists (double_moins_un p); Split; [
+    Reflexivity
+  | Clear IHp; Split; [
+      NewInduction p as [|p0 IHp0|]; [
+        Reflexivity
+      | Simpl; Rewrite IHp0; Reflexivity
+      | Reflexivity ]
+    | NewDestruct p; [Right|Right|Left]; Reflexivity ]].
+Qed.
+
+Theorem sub_add: 
+(x,y:positive) (compare x y EGAL) = SUPERIEUR -> (add y (true_sub x y)) = x.
+Proof.
+Intros x y H;Elim sub_pos_SUPERIEUR with 1:=H;
+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 Plus.
+Require Mult.
+Require Minus.
+
+(** [IPN] 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.
-Induction x; Simpl; Auto with arith; Intros x' H0 m; Rewrite H0;
-Rewrite plus_assoc_l; Trivial with arith.
+Induction x; Simpl; Auto; Intros x' H0 m; Rewrite H0;
+Rewrite plus_assoc_l; Trivial.
 Qed.
 
 Theorem convert_add_carry :
@@ -164,16 +716,54 @@ Proof.
 Intros x y; Exact (add_verif x y (S O)).
 Qed.
 
-(** Correctness of conversion *)
-Theorem bij1 : (m:nat) (convert (anti_convert m)) = (S m).
+(** [IPN_shift] is a morphism for addition wrt the factor *)
+
+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.
-Induction m; [
-  Unfold convert; Simpl; Trivial with arith
-| Unfold convert; Intros n H; Simpl; Rewrite convert_add_un; Rewrite H; Auto with arith].
+Induction y; [
+  Intros p H 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
+| Intros p H m; Simpl; Rewrite H; Auto with arith
+| Intro;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.
+ 
+(** [IPN] is a morphism for 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.
+
+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.
+
+(** IPN is strictly positive *)
 
 Theorem compare_positive_to_nat_O : 
-	(p:positive)(m:nat)(le m  (positive_to_nat p m)).
+	(p:positive)(m:nat)(le m (positive_to_nat p m)).
 Induction p; Simpl; Auto with arith.
 Intros; Apply le_trans with (plus m m);  Auto with arith.
 Qed.
@@ -183,64 +773,60 @@ Intro; Unfold convert; Apply lt_le_trans with (S O); Auto with arith.
 Apply compare_positive_to_nat_O.
 Qed.
 
-Hints Resolve compare_convert_O.
+(** Mapping of 2 and 4 through IPN_shift *)
 
-(** Subtraction *)
-Fixpoint double_moins_un [x:positive]:positive :=
-  <positive>Cases x of
-      (xI x') => (xI (xO x'))
-    | (xO x') => (xI (double_moins_un x'))
-    | xH => xH
-    end.
-
-Definition sub_un := [x:positive]
-  <positive> Cases x of
-             (xI x') => (xO x')
-           | (xO x') => (double_moins_un x')
-           | xH => xH
-           end.
-
-Lemma sub_add_one : (x:positive) (sub_un (add_un x)) = x.
+Lemma positive_to_nat_2 : (p:positive)
+    (positive_to_nat p (2))=(mult (2) (positive_to_nat p (1))).
 Proof.
-(Induction x; [Idtac | Idtac | Simpl;Auto with arith ]);
-(Intros p; Elim p; [Idtac | Idtac | Simpl;Auto with arith]);
-Simpl; Intros q H1 H2; Case H2; Simpl; Trivial with arith.
+  Intros. Rewrite <- positive_to_nat_mult. Reflexivity.
 Qed.
 
-Lemma is_double_moins_un : (x:positive) (add_un (double_moins_un x)) = (xO x).
+Lemma positive_to_nat_4 : (p:positive)
+    (positive_to_nat p (4))=(mult (2) (positive_to_nat p (2))).
 Proof.
-(Induction x;Simpl;Auto with arith); Intros m H;Rewrite H;Trivial with arith.
+  Intros. Rewrite <- positive_to_nat_mult. Reflexivity.
 Qed.
 
-Lemma add_sub_one : (x:positive) (x=xH) \/ (add_un (sub_un x)) = x.
+(** Mapping of xH, xO and xI through IPN *)
+
+Lemma convert_xH : (convert xH)=(1).
 Proof.
-Induction x; [
-  Simpl; Auto with arith
-| Simpl; Intros;Right;Apply is_double_moins_un
-| Auto with arith ].
+  Reflexivity.
 Qed.
 
-Lemma ZL0 : (S (S O))=(plus (S O) (S O)).
-Proof. Auto with arith. 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 ZL1: (y:positive)(xO (add_un y)) = (add_un (add_un (xO y))).
+Lemma convert_xI : (p:positive) (convert (xI p))=(S (mult (2) (convert p))).
 Proof.
-Induction y; Simpl; Auto with arith.
+  Induction p. Unfold convert. Simpl. Intro p0. Intro. Rewrite positive_to_nat_2.
+  Rewrite positive_to_nat_4. Inversion H. Rewrite H1. Rewrite <- plus_Snm_nSm. Reflexivity.
+  Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4.
+  Inversion H. Rewrite H1. Reflexivity.
+  Reflexivity.
 Qed.
 
-Lemma ZL2:
-  (y:positive)(m:nat)
-    (positive_to_nat y (plus m m)) =
-              (plus (positive_to_nat y m) (positive_to_nat y m)).
+(**********************************************************************)
+(** Properties of the shifted injection from Peano natural numbers to 
+    binary positive numbers *)
+
+(** Composition of [INP] and [IPN] is shifted identity on [nat] *)
+
+Theorem bij1 : (m:nat) (convert (anti_convert m)) = (S m).
 Proof.
-Induction y; [
-  Intros p H 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
-| Intros p H m; Simpl; Rewrite H; Auto with arith
-| Intro;Simpl; Trivial with arith ].
+Induction m; [
+  Unfold convert; Simpl; Trivial
+| Unfold convert; Intros n H; Simpl; Rewrite convert_add_un; Rewrite H; Auto ].
 Qed.
 
+(** Miscellaneous lemmas on [INP] *)
+
 Lemma ZL3: (x:nat) (add_un (anti_convert (plus x x))) =  (xO (anti_convert x)).
 Proof.
 Induction x; [
@@ -252,10 +838,10 @@ Lemma ZL4: (y:positive) (EX h:nat |(convert y)=(S h)).
 Proof.
 Induction y; [
   Intros p H;Elim H; Intros x H1; Exists (plus (S x) (S x));
-  Unfold convert ;Simpl; Rewrite ZL0; Rewrite ZL2; Unfold convert in H1;
+  Unfold convert ;Simpl; Change (2) with (plus (1) (1)); Rewrite ZL2; Unfold convert in H1;
   Rewrite H1; Auto with arith
 | Intros p H1;Elim H1;Intros x H2; Exists (plus x (S x)); Unfold convert;
-  Simpl; Rewrite ZL0; Rewrite ZL2;Unfold convert in H2; Rewrite H2; Auto with arith
+  Simpl; Change (2) with (plus (1) (1)); Rewrite ZL2;Unfold convert in H2; Rewrite H2; Auto with arith
 | Exists O ;Auto with arith ].
 Qed.
 
@@ -266,13 +852,16 @@ Induction x;Simpl; [
 | Intros y H; Rewrite <- plus_n_Sm; Simpl; Rewrite H; Auto with arith].
 Qed.
 
-Lemma bij2 : (x:positive) (anti_convert (convert x)) = (add_un x).
+(** Composition of [IPN] and [INP] is shifted identity on [positive] *)
+
+Theorem bij2 : (x:positive) (anti_convert (convert x)) = (add_un x).
 Proof.
 Induction x; [
-  Intros p H; Simpl; Rewrite <- H; Rewrite ZL0;Rewrite ZL2; Elim (ZL4 p); 
+  Intros 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
-
-| Intros p H; Unfold convert ;Simpl; Rewrite ZL0; Rewrite ZL2;
+| Intros p H; 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)))));
@@ -282,55 +871,15 @@ Induction x; [
 | Unfold convert; Simpl; Auto with arith ].
 Qed.
 
-(** Comparison of positive *)
-Fixpoint compare [x,y:positive]: relation -> relation :=
-  [r:relation] <relation> Cases x of
-            (xI x') => <relation>Cases y of
-                          (xI y') => (compare x' y' r)
-                        | (xO y') => (compare x' y' SUPERIEUR)
-                        | xH => SUPERIEUR
-                        end
-          | (xO x') => <relation>Cases y of
-                          (xI y') => (compare x' y' INFERIEUR)
-                        | (xO y') => (compare x' y' r)
-                        | xH => SUPERIEUR
-                        end
-          | xH => <relation>Cases y of
-                     (xI y') => INFERIEUR
-                   | (xO y') => INFERIEUR
-                   | xH => r
-                   end
-  end.
+(** Composition of [IPN], [INP] and [Ppred] is identity on [positive] *)
 
-Theorem compare_convert1 : 
- (x,y:positive) 
-  ~(compare x y SUPERIEUR) = EGAL /\ ~(compare x y INFERIEUR) = EGAL.
+Theorem bij3: (x:positive)(sub_un (anti_convert (convert x))) = x.
 Proof.
-Induction x;Induction y;Split;Simpl;Auto with arith;
-  Discriminate Orelse (Elim (H p0); Auto with arith).
+Intros x; Rewrite bij2; Rewrite sub_add_one; Trivial with arith.
 Qed.
 
-Theorem compare_convert_EGAL : (x,y:positive) (compare x y EGAL) = EGAL -> x=y.
-Proof.
-Induction x;Induction y;Simpl;Auto with arith; [
-  Intros z H1 H2; Rewrite (H z); Trivial with arith
-| Intros z H1 H2; Absurd (compare p z SUPERIEUR)=EGAL ;
-   [ Elim (compare_convert1 p z);Auto with arith | Assumption ]
-| Intros H1;Discriminate H1
-| Intros z H1 H2; Absurd (compare p z INFERIEUR) = EGAL; 
-    [ Elim (compare_convert1 p z);Auto with arith | Assumption ]
-| Intros z H1 H2 ;Rewrite (H z);Auto with arith 
-| Intros H1;Discriminate H1
-| Intros p H H1;Discriminate H1
-| Intros p H H1;Discriminate H1 ].
-Qed.
+(** Extra lemmas on [lt] on Peano natural numbers *)
 
-Lemma ZL6:
-  (p:positive) (positive_to_nat p (S(S O))) = (plus (convert p) (convert p)).
-Proof.
-Intros p;Rewrite ZL0; Rewrite ZL2; Trivial with arith.
-Qed.
- 
 Lemma ZL7:
   (m,n:nat) (lt m n) -> (lt (plus m m) (plus n n)).
 Proof.
@@ -347,39 +896,11 @@ Intros m n H; Apply le_lt_trans with m:=(plus m n); [
 | Rewrite (plus_sym m n); Apply lt_reg_l with 1:=H ].
 Qed.
 
-Lemma ZLSI:
- (x,y:positive) (compare x y SUPERIEUR) = INFERIEUR -> 
-                (compare x y EGAL) = INFERIEUR.
-Proof.
-Induction x;Induction y;Simpl;Auto with arith; 
-  Discriminate Orelse Intros H;Discriminate H.
-Qed.
-
-Lemma ZLIS:
- (x,y:positive) (compare x y INFERIEUR) = SUPERIEUR -> 
-                (compare x y EGAL) = SUPERIEUR.
-Proof.
-Induction x;Induction y;Simpl;Auto with arith; 
-  Discriminate Orelse Intros H;Discriminate H.
-Qed.
+(** [IPN] is a morphism from [positive] to [nat] for [lt] (expressed
+    from [compare] on [positive])
 
-Lemma ZLII:
- (x,y:positive) (compare x y INFERIEUR) = INFERIEUR ->
-                (compare x y EGAL) = INFERIEUR \/ x = y.
-Proof.
-(Induction x;Induction y;Simpl;Auto with arith;Try Discriminate);
- Intros z H1 H2; Elim (H z H2);Auto with arith; Intros E;Rewrite E;
- Auto with arith.
-Qed.
-
-Lemma ZLSS:
- (x,y:positive) (compare x y SUPERIEUR) = SUPERIEUR ->
-                (compare x y EGAL) = SUPERIEUR \/ x = y.
-Proof.
-(Induction x;Induction y;Simpl;Auto with arith;Try Discriminate);
- Intros z H1 H2; Elim (H z H2);Auto with arith; Intros E;Rewrite E;
- Auto with arith.
-Qed.
+    Part 1: [lt] on [positive] is finer than [lt] on [nat]
+*)
 
 Theorem compare_convert_INFERIEUR : 
   (x,y:positive) (compare x y EGAL) = INFERIEUR -> 
@@ -405,6 +926,12 @@ Induction x;Induction y; [
 | Simpl; Intros H;Discriminate H ].
 Qed.
 
+(** [IPN] 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]
+*)
+
 Theorem compare_convert_SUPERIEUR : 
   (x,y:positive) (compare x y EGAL)=SUPERIEUR -> (gt (convert x) (convert y)).
 Proof.
@@ -429,10 +956,11 @@ Unfold gt; Induction x;Induction y; [
 | Simpl;Intros H;Discriminate H ].
 Qed.
 
-Lemma Dcompare : (r:relation) r=EGAL \/ r = INFERIEUR \/ r = SUPERIEUR.
-Proof.
-Induction r; Auto with arith. 
-Qed.
+(** [IPN] 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]
+*)
 
 Theorem convert_compare_INFERIEUR : 
   (x,y:positive)(lt (convert x) (convert y)) -> (compare x y EGAL) = INFERIEUR.
@@ -441,13 +969,19 @@ 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 with arith
+    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.
 
+(** [IPN] 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]
+*)
+
 Theorem convert_compare_SUPERIEUR : 
   (x,y:positive)(gt (convert x) (convert y)) -> (compare x y EGAL) = SUPERIEUR.
 Proof.
@@ -458,240 +992,11 @@ Intros x y; Unfold gt; Elim (Dcompare (compare x y EGAL)); [
     Intros H1 H2; Absurd (lt (convert y) (convert x)); [
       Apply lt_not_sym; Apply compare_convert_INFERIEUR; Assumption
     | Assumption ]
-  | Auto with arith]].
-Qed.
-
-Theorem convert_compare_EGAL: (x:positive)(compare x x EGAL)=EGAL.
-Induction x; Auto with arith.
-Qed.
-
-(** Natural numbers coded with positive *)
-
-Inductive entier: Set := Nul : entier | Pos : positive -> entier.
-
-Definition Un_suivi_de := 
-  [x:entier]<entier> Cases x of Nul => (Pos xH) | (Pos p) => (Pos (xI p)) end.
-
-Definition Zero_suivi_de := 
-  [x:entier]<entier> Cases x of Nul => Nul | (Pos p) => (Pos (xO p)) end.
-
-Definition double_moins_deux :=
-  [x:positive] <entier>Cases x of
-           (xI x') => (Pos (xO (xO x')))
-         | (xO x') => (Pos (xO (double_moins_un x')))
-         | xH => Nul
-         end.
-Lemma ZS: (p:entier) (Zero_suivi_de p) = Nul -> p = Nul.
-Proof.
-Induction p;Simpl; [ Trivial with arith | Intros q H;Discriminate H ].
-Qed.
-
-Lemma US: (p:entier) ~(Un_suivi_de p)=Nul.
-Proof.
-Induction p; Intros; Discriminate.
-Qed.
-
-Lemma USH: (p:entier) (Un_suivi_de p) = (Pos xH) -> p = Nul.
-Proof.
-Induction p;Simpl; [ Trivial with arith | Intros q H;Discriminate H ].
-Qed.
-
-Lemma ZSH: (p:entier) ~(Zero_suivi_de p)= (Pos xH).
-Proof.
-Induction p; Intros; Discriminate.
-Qed.
-
-Fixpoint sub_pos[x,y:positive]:entier :=
-  <entier>Cases x of
-         (xI x') => <entier>Cases y of
-                           (xI y') => (Zero_suivi_de (sub_pos x' y'))
-                         | (xO y') => (Un_suivi_de (sub_pos x' y'))
-                         | xH => (Pos (xO x'))
-                         end
-       | (xO x') => <entier>Cases y of
-                           (xI y') => (Un_suivi_de (sub_neg x' y'))
-                         | (xO y') => (Zero_suivi_de (sub_pos x' y'))
-                         | xH => (Pos (double_moins_un x'))
-                         end
-       | xH => <entier>Cases y of
-                           (xI y') => (Pos (double_moins_un y'))
-                         | (xO y') => (double_moins_deux y')
-                         | xH => Nul
-                         end
-       end
-with sub_neg [x,y:positive]:entier :=
-  <entier>Cases x of
-       (xI x') => <entier>Cases y of
-                            (xI y') => (Un_suivi_de (sub_neg x' y'))
-                          | (xO y') => (Zero_suivi_de (sub_pos x' y'))
-                          | xH => (Pos (double_moins_un x'))
-                          end
-     | (xO x') => <entier>Cases y of
-                            (xI y') => (Zero_suivi_de (sub_neg x' y'))
-                          | (xO y') => (Un_suivi_de (sub_neg x' y'))
-                          | xH => (double_moins_deux x')
-                          end
-     | xH => <entier>Cases y of
-                            (xI y') => (Pos (xO y'))
-                          | (xO y') => (Pos (double_moins_un y'))
-                          | xH => Nul
-                          end
-     end.
-
-Theorem sub_pos_x_x : (x:positive) (sub_pos x x) = Nul.
-Proof.
-Induction x; [
-  Simpl; Intros p H;Rewrite H;Simpl; Trivial with arith
-| Intros p H;Simpl;Rewrite H;Auto with arith
-| Auto with arith ].
-Qed.
-
-Theorem ZL10: (x,y:positive)
- (compare x y EGAL) = SUPERIEUR ->
- (sub_pos x y) = (Pos xH) -> (sub_neg x y) = Nul.
-Proof.
-Induction x;Induction y; [
-  Intros q H1 H2 H3; Absurd (sub_pos (xI p) (xI q))=(Pos xH); 
-    [ Simpl; Apply ZSH | Assumption ]
-| Intros q H1 H2 H3; Simpl in H3; Cut (sub_pos p q)=Nul; [
-     Intros H4;Simpl;Rewrite H4; Simpl; Trivial with arith
-   | Apply USH;Assumption ]
-| Simpl; Intros H1 H2;Discriminate H2
-| Intros q H1 H2;
-  Change (Un_suivi_de (sub_neg p q))=(Pos xH) 
-            -> (Zero_suivi_de (sub_neg p q))=Nul;
-  Intros H3; Rewrite (USH (sub_neg p q) H3); Simpl; Auto with arith
-| Intros q H1 H2 H3; Absurd (sub_pos (xO p) (xO q))=(Pos xH);
-    [ Simpl; Apply ZSH | Assumption ]
-| Intros H1; Elim p; [ 
-    Simpl; Intros q H2 H3;Discriminate H3
-  | Simpl; Intros q H2 H3;Discriminate H3
-  | Simpl; Auto with arith ]
-| Simpl; Intros q H1 H2 H3;Discriminate H2
-| Simpl; Intros q H1 H2 H3;Discriminate H2 
-| Simpl; Intros H;Discriminate H ].
-Qed.
-
-Lemma ZL11: (x:positive) (x=xH) \/ ~(x=xH).
-Proof.
-Intros x;Case x;Intros; (Left;Reflexivity) Orelse (Right;Discriminate).
+  | Auto]].
 Qed.
 
-Lemma ZL12: (q:positive) (add_un q) = (add q xH).
-Proof.
-Induction q; Intros; Simpl; Trivial with arith.
-Qed.
-
-Lemma ZL12bis: (q:positive) (add_un q) = (add xH q).
-Proof.
-Induction q; Intros; Simpl; Trivial with arith.
-Qed.
-
-Theorem ZL13:
-  (x,y:positive)(add_carry x y) = (add_un (add x y)).
-Proof.
-(Induction x;Induction y;Simpl;Auto with arith); Intros q H1;Rewrite H;
- Auto with arith.
-Qed.
-
-Theorem ZL14:
-  (x,y:positive)(add x (add_un y)) = (add_un (add x y)).
-Proof.
-Induction x;Induction y;Simpl;Auto with arith; [
-  Intros q H1; Rewrite ZL13; Rewrite  H; Auto with arith
-| Intros q H1; Rewrite ZL13; Auto with arith
-| Elim p;Simpl;Auto with arith
-| Intros q H1;Rewrite H;Auto with arith
-| Elim p;Simpl;Auto with arith ].
-Qed.
-
-Theorem ZL15:
-  (q,z:positive) ~z=xH -> (add_carry q (sub_un z)) = (add q z).
-Proof.
-Intros q z H; Elim (add_sub_one z); [
-  Intro;Absurd z=xH;Auto with arith
-| Intros E;Pattern 2 z ;Rewrite <- E; Rewrite ZL14; Rewrite ZL13; Trivial with arith ].
-Qed. 
-
-Theorem sub_pos_SUPERIEUR:
-  (x,y:positive)(compare x y EGAL)=SUPERIEUR -> 
-    (EX h:positive | (sub_pos x y) = (Pos h) /\ (add y h) = x /\
-                     (h = xH \/ (sub_neg x y) = (Pos (sub_un h)))).
-Proof.
-Induction x;Induction y; [
-  Intros q H1 H2; Elim (H q H2); Intros z H3;Elim H3;Intros H4 H5; 
-  Elim H5;Intros H6 H7;   Exists (xO z); Split; [
-    Simpl; Rewrite H4; Auto with arith
-  | Split; [
-      Simpl; Rewrite H6; Auto with arith
-    | Right; Simpl; Elim (ZL11 z); [
-        Intros H8; Simpl; Rewrite ZL10; [
-          Rewrite H8; Auto with arith
-        | Exact H2
-        | Rewrite <- H8; Auto with arith ]
-     | Intro H8; Elim H7; [
-         Intro H9; Absurd z=xH; Auto with arith
-       | Intros H9;Simpl;Rewrite H9;Generalize H8 ;Case z;Auto with arith; 
-         Intros H10;Absurd xH=xH;Auto with arith ]]]]
-| Intros q H1 H2; Simpl in H2; Elim ZLSS with 1:=H2; [
-    Intros H3;Elim (H q H3); Intros z H4; Exists (xI z);
-    Elim H4;Intros H5 H6;Elim H6;Intros H7 H8; Split; [
-      Simpl;Rewrite H5;Auto with arith
-    | Split; [
-        Simpl; Rewrite H7; Trivial with arith
-      | Right;Change (Zero_suivi_de (sub_pos p q))=(Pos (sub_un (xI z)));
-        Rewrite H5; Auto with arith ]]
-  | Intros H3; Exists xH; Rewrite H3; Split; [
-      Simpl; Rewrite sub_pos_x_x; Auto with arith
-    | Split; Auto with arith ]]
-| Intros H1; Exists (xO p); Auto with arith
-| Intros q H1 H2; Simpl in H2; Elim (H q); [
-    Intros z H3; Elim H3;Intros H4 H5;Elim H5;Intros H6 H7; 
-    Elim (ZL11 z); [
-      Intros vZ; Exists xH; Split; [
-        Change (Un_suivi_de (sub_neg p q))=(Pos xH); 
-        Rewrite ZL10; [ Auto with arith | Apply ZLIS;Assumption | Rewrite <- vZ;Assumption ]
-      | Split; [
-          Simpl; Rewrite ZL12; Rewrite <- vZ; Rewrite H6; Trivial with arith
-        | Auto with arith ]]
-    | Exists (xI (sub_un z)); Elim H7;[
-        Intros H8; Absurd z=xH;Assumption
-      | Split; [
-          Simpl;Rewrite H8; Trivial with arith
-        | Split; [
-            Change (xO (add_carry q (sub_un z)))=(xO p); Rewrite ZL15; [
-              Rewrite H6;Trivial with arith
-            | Assumption ]
-          | Right; Change (Zero_suivi_de (sub_neg p q)) =
-                           (Pos (sub_un (xI (sub_un z))));
-            Rewrite H8; Auto with arith]]]]
-  | Apply ZLIS; Assumption ]
-| Intros q H1 H2; Simpl in H2; Elim (H q H2); Intros z H3; 
-  Exists (xO z); Elim H3;Intros H4 H5;Elim H5;Intros H6 H7; Split; [
-    Simpl; Rewrite H4;Auto with arith
-  | Split; [
-      Simpl;Rewrite H6;Auto with arith
-    | Right; Change (Un_suivi_de (sub_neg p q))=(Pos (double_moins_un z));
-      Elim (ZL11 z); [
-        Simpl; Intros H8;Rewrite H8; Simpl;
-        Cut (sub_neg p q)=Nul;[
-          Intros H9;Rewrite H9;Auto with arith
-        | Apply ZL10;[Assumption|Rewrite <- H8;Assumption]]
-      | Intros H8;Elim H7; [
-          Intros H9;Absurd z=xH;Auto with arith
-        | Intros H9;Rewrite H9; Generalize H8 ;Elim z; Simpl; Auto with arith;
-          Intros H10;Absurd xH=xH;Auto with arith ]]]]
-| Intros H1; Exists (double_moins_un p); Split; [
-    Auto with arith
-  | Split; [
-      Elim p;Simpl;Auto with arith; Intros q H2; Rewrite ZL12bis; Rewrite H2; Trivial with arith
-    | Change (double_moins_un p)=xH \/ 
-             (double_moins_deux p)=(Pos (sub_un (double_moins_un p))); 
-      Case p;Simpl;Auto with arith ]]
-| Intros p H1 H2;Simpl in H2; Discriminate H2
-| Intros p H1 H2;Simpl in H2;Discriminate H2
-| Intros H1;Simpl in H1;Discriminate H1 ].
-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.
@@ -714,157 +1019,262 @@ Intros x y H; Rewrite (compare_convert_EGAL x y H);
 Apply convert_compare_EGAL.
 Qed.
 
-Definition Op := [r:relation]
- <relation>Cases r of
-             EGAL => EGAL
-           | INFERIEUR => SUPERIEUR
-           | SUPERIEUR => INFERIEUR
-           end.
-
 Lemma ZC4: (x,y:positive) (compare x y EGAL) = (Op (compare y x EGAL)).
 Proof.
 (((Intros x y;Elim (Dcompare (compare y x EGAL));[Idtac | Intros H;Elim H]);
 Intros E;Rewrite E;Simpl); [Apply ZC3 | Apply ZC2 | Apply ZC1 ]); Assumption.
 Qed.
 
-Theorem add_sym : (x,y:positive) (add x y) = (add y x).
-Proof.
-Induction x;Induction y;Simpl;Auto with arith; Intros q H1; [
-  Clear  H1; Do 2 Rewrite ZL13; Rewrite H;Auto with arith
-| Rewrite H;Auto with arith | Rewrite H;Auto with arith | Rewrite H;Auto with arith ].
-Qed. 
+(**********************************************************************)
+(** Extra properties of the injection from binary positive numbers to Peano 
+    natural numbers *)
+
+(** [IPN] is a morphism for subtraction on positive numbers *)
 
-Lemma bij3: (x:positive)(sub_un (anti_convert (convert x))) = x.
+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; Rewrite bij2; Rewrite sub_add_one; Trivial with arith.
+Intros x y H; Apply (simpl_plus_l (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.
 
+(** [IPN] 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 simpl_add_r : (x,y,z:positive) (add x z)=(add y z) -> x=y.
+Lemma ZL16: (p,q:positive)(lt (minus (convert p) (convert q)) (convert p)).
 Proof.
-Intros x y z H;Apply convert_intro;
-Apply (simpl_plus_l (convert z)); Do 2 Rewrite (plus_sym (convert z)); 
-Do 2 Rewrite <- convert_add; Rewrite H; Trivial with arith.
+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 simpl_add_l : (x,y,z:positive) (add x y)=(add x z) -> y=z.
+Lemma ZL17: (p,q:positive)(lt (convert p) (convert (add p q))).
 Proof.
-Intros x y z H;Apply convert_intro;
-Apply (simpl_plus_l (convert x)); Do 2 Rewrite <- convert_add; 
-Rewrite H; Trivial with arith.
+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.
 
-Theorem add_assoc: (x,y,z:positive)(add x (add y z)) = (add (add x y) z).
+(* 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 x y z; Apply convert_intro; Do 4 Rewrite convert_add; 
-Apply plus_assoc_l.
+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.
 
-Local true_sub := [x,y:positive] 
-  <positive> Cases (sub_pos x y) of Nul => xH | (Pos z) => z end.
+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.
-Theorem sub_add: 
-(x,y:positive) (compare x y EGAL) = SUPERIEUR -> (add y (true_sub x y)) = x.
-
-Intros x y H;Elim sub_pos_SUPERIEUR with 1:=H;
-Intros z H1;Elim H1;Intros H2 H3; Elim H3;Intros H4 H5; 
-Unfold true_sub ;Rewrite H2; Exact H4.
+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.
- 
-Theorem true_sub_convert:
-  (x,y:positive) (compare x y EGAL) = SUPERIEUR -> 
-     (convert (true_sub x y)) = (minus (convert x) (convert y)).
+
+(**********************************************************************)
+(** Properties of multiplication on binary positive numbers *)
+
+(** One is right neutral for multiplication *)
+
+Lemma times_x_1 : (x:positive) (times x xH) = x.
 Proof.
-Intros x y H; Apply (simpl_plus_l (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)].
+NewInduction x; Simpl.
+  Rewrite IHx; Reflexivity.
+  Rewrite IHx; Reflexivity.
+  Reflexivity.
 Qed.
 
-(** Misc properties of the injection from positive to nat *)
+(** Right reduction properties for multiplication *)
 
-Lemma convert_xH : (convert xH)=(1).
+Lemma times_x_double : (x,y:positive) (times x (xO y)) = (xO (times x y)).
 Proof.
+Intros; NewInduction x; Simpl.
+  Rewrite IHx; Reflexivity.
+  Rewrite IHx; Reflexivity.
   Reflexivity.
 Qed.
 
-Lemma positive_to_nat_mult : (p:positive) (n,m:nat)
-    (positive_to_nat p (mult m n))=(mult m (positive_to_nat p n)).
+Lemma times_x_double_plus_one :
+ (x,y:positive) (times x (xI y)) = (add x (xO (times x y))).
 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.
+Intros; NewInduction x; Simpl.
+  Rewrite IHx; Do 2 Rewrite add_assoc; Rewrite add_sym with x:=y; Reflexivity.
+  Rewrite IHx; Reflexivity.
+  Reflexivity.
 Qed.
 
-Lemma positive_to_nat_2 : (p:positive)
-    (positive_to_nat p (2))=(mult (2) (positive_to_nat p (1))).
+(** Commutativity of multiplication *)
+
+Theorem times_sym : (x,y:positive) (times x y) = (times y x).
 Proof.
-  Intros. Rewrite <- positive_to_nat_mult. Reflexivity.
+NewInduction y; Simpl.
+  Rewrite <- IHy; Apply times_x_double_plus_one.
+  Rewrite <- IHy; Apply times_x_double.
+  Apply times_x_1.
 Qed.
 
-Lemma positive_to_nat_4 : (p:positive)
-    (positive_to_nat p (4))=(mult (2) (positive_to_nat p (2))).
+(** 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. Rewrite <- positive_to_nat_mult. Reflexivity.
+Intros; 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.
 
-Lemma convert_xO : (p:positive) (convert (xO p))=(mult (2) (convert p)).
+Theorem times_add_distr_l:
+  (x,y,z:positive) (times (add x y) z) = (add (times x z) (times y z)).
 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.
+Intros x y z; Do 3 Rewrite times_sym with y:=z; Apply times_add_distr.
 Qed.
 
-Lemma convert_xI : (p:positive) (convert (xI p))=(S (mult (2) (convert p))).
+(** Associativity of multiplication *)
+
+Theorem times_assoc :
+  ((x,y,z:positive) (times x (times y z))= (times (times x y) z)).
 Proof.
-  Induction p. Unfold convert. Simpl. Intro p0. Intro. Rewrite positive_to_nat_2.
-  Rewrite positive_to_nat_4. Inversion H. Rewrite H1. Rewrite <- plus_Snm_nSm. Reflexivity.
-  Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4.
-  Inversion H. Rewrite H1. Reflexivity.
+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.
+
+(**********************************************************************)
+(** Binary natural numbers *)
+
+Inductive entier: Set := Nul : entier | Pos : positive -> entier.
+
+(**********************************************************************)
+(** Binary integer numbers *)
+
+Inductive Z : Set := 
+  ZERO : Z | POS : positive -> Z | NEG : positive -> Z.
+
+(* Declare Scope Z_scope with Key Z *)
+Delimits Scope Z_scope with Z.
+
+(* Automatically open scope Z_scope for arguments of type Z, POS and NEG *)
+Bind Scope Z_scope with Z.
+Arguments Scope POS [ Z_scope ].
+Arguments Scope NEG [ Z_scope ].
+
 (** Addition on integers *)
+
+Definition Zdouble_plus_one [x:Z] :=
+  Cases x of 
+  | ZERO    => (POS xH)
+  | (POS p) => (POS (xI p))
+  | (NEG p) => (NEG (double_moins_un p))
+  end.
+
+Definition Zdouble_minus_one [x:Z] :=
+  Cases x of 
+  | ZERO    => (NEG xH)
+  | (NEG p) => (NEG (xI p))
+  | (POS p) => (POS (double_moins_un p))
+  end.
+
+Definition Zdouble [x:Z] :=
+  Cases x of
+  | ZERO => ZERO
+  | (POS p) => (POS (xO p))
+  | (NEG p) => (NEG (xO p))
+ end.
+
+Fixpoint Zsub_pos[x,y:positive]:Z :=
+  Cases x y of
+  | (xI x') (xI y') => (Zdouble (Zsub_pos x' y'))
+  | (xI x') (xO y') => (Zdouble_plus_one (Zsub_pos x' y'))
+  | (xI x') xH      => (POS (xO x'))
+  | (xO x') (xI y') => (Zdouble_minus_one (Zsub_pos x' y'))
+  | (xO x') (xO y') => (Zdouble (Zsub_pos x' y'))
+  | (xO x') xH      => (POS (double_moins_un x'))
+  | xH      (xI y') => (NEG (xO y'))
+  | xH      (xO y') => (NEG (double_moins_un y'))
+  | xH      xH      => ZERO
+  end.
+
 Definition Zplus := [x,y:Z]
-  <Z>Cases x of
-      ZERO => y
-    | (POS x') =>
-          <Z>Cases y of
-               ZERO => x
-             | (POS y') => (POS (add x' y'))
-             | (NEG y') =>
-                   <Z>Cases (compare x' y' EGAL) of
-                        EGAL => ZERO
-                      | INFERIEUR => (NEG (true_sub y' x'))
-                      | SUPERIEUR => (POS (true_sub x' y'))
-                      end
-             end
-    | (NEG x') =>
-          <Z>Cases y of
-               ZERO => x
-             | (POS y') =>
-                   <Z>Cases (compare x' y' EGAL) of
-                        EGAL => ZERO
-                      | INFERIEUR => (POS (true_sub y' x'))
-                      | SUPERIEUR => (NEG (true_sub x' y'))
-                      end
-             | (NEG y') => (NEG (add x' y'))
-             end
-    end.
+  Cases x y of
+    ZERO      y       => y
+  | x         ZERO    => x
+  | (POS x') (POS y') => (POS (add x' y'))
+  | (POS x') (NEG y') => 
+      Cases (compare x' y' EGAL) of
+      | EGAL => ZERO
+      | INFERIEUR => (NEG (true_sub y' x'))
+      | SUPERIEUR => (POS (true_sub x' y'))
+      end
+  | (NEG x') (POS y') =>
+      Cases (compare x' y' EGAL) of
+      | EGAL => ZERO
+      | INFERIEUR => (POS (true_sub y' x'))
+      | SUPERIEUR => (NEG (true_sub x' y'))
+      end
+  | (NEG x') (NEG y') => (NEG (add x' y'))
+  end.
 
 V8Infix "+" Zplus : Z_scope.
 
 (** Opposite *)
 
 Definition Zopp := [x:Z]
- <Z>Cases x of
+ Cases x of
       ZERO => ZERO
     | (POS x) => (NEG x)
     | (NEG x) => (POS x)
@@ -872,13 +1282,79 @@ Definition Zopp := [x:Z]
 
 V8Notation "- x" := (Zopp x) : Z_scope.
 
-Theorem Zero_left: (x:Z) (Zplus ZERO x) = x.
+(** Multiplication on integers *)
+
+Definition Zmult := [x,y:Z]
+  Cases x y of
+  | ZERO     _        => ZERO
+  | _        ZERO     => ZERO
+  | (POS x') (POS y') => (POS (times x' y'))
+  | (POS x') (NEG y') => (NEG (times x' y'))
+  | (NEG x') (POS y') => (NEG (times x' y'))
+  | (NEG x') (NEG y') => (POS (times x' y'))
+  end.
+
+V8Infix "*" Zmult : Z_scope.
+
+(** Comparison of integers *)
+
+Definition Zcompare := [x,y:Z]
+  Cases x y of
+  | ZERO     ZERO     => EGAL
+  | ZERO     (POS y') => INFERIEUR
+  | ZERO     (NEG y') => SUPERIEUR
+  | (POS x') ZERO     => SUPERIEUR
+  | (POS x') (POS y') => (compare x' y' EGAL)
+  | (POS x') (NEG y') => SUPERIEUR
+  | (NEG x') ZERO     => INFERIEUR
+  | (NEG x') (POS y') => INFERIEUR
+  | (NEG x') (NEG y') => (Op (compare x' y' EGAL))
+  end.
+
+V8Infix "?=" Zcompare (at level 50, no associativity) : Z_scope.
+
+Open Scope Z_scope.
+
+(**********************************************************************)
+(** Properties of opposite on binary integer numbers *)
+
+Theorem Zopp_NEG : (x:positive) (Zopp (NEG x)) = (POS x).
 Proof.
-Induction x; Auto with arith.
+Reflexivity.
 Qed.
 
+(** [opp] is involutive *)
+
 Theorem Zopp_Zopp: (x:Z) (Zopp (Zopp x)) = x.
 Proof.
+NewDestruct x; Reflexivity.
+Qed.
+
+(** Injectivity of the opposite *)
+
+Theorem Zopp_intro : (x,y:Z) (Zopp x) = (Zopp y) -> x = y.
+Proof.
+Intros x y;Case x;Case y;Simpl;Intros; [
+  Trivial | Discriminate H | Discriminate H | Discriminate H
+| Simplify_eq H; Intro E; Rewrite E; Trivial
+| Discriminate H | Discriminate H | Discriminate H
+| Simplify_eq H; Intro E; Rewrite E; Trivial ].
+Qed.
+
+(**********************************************************************)
+(** Other properties of binary integer numbers *)
+
+Hints Local Resolve compare_convert_O.
+
+Lemma ZL0 : (S (S O))=(plus (S O) (S O)).
+Proof.
+Reflexivity.
+Qed.
+
+(** Addition on integers *)
+
+Theorem Zero_left: (x:Z) (Zplus ZERO x) = x.
+Proof.
 Induction x; Auto with arith.
 Qed.
 
@@ -921,21 +1397,7 @@ Proof.
 Intro; Rewrite Zplus_sym; Apply Zplus_inverse_r.
 Qed.
 
-Theorem Zopp_intro : (x,y:Z) (Zopp x) = (Zopp y) -> x = y.
-Proof.
-Intros x y;Case x;Case y;Simpl;Intros; [
-  Trivial with arith | Discriminate H | Discriminate H | Discriminate H
-| Simplify_eq H; Intro E; Rewrite E; Trivial with arith
-| Discriminate H | Discriminate H | Discriminate H
-| Simplify_eq H; Intro E; Rewrite E; Trivial with arith ].
-Qed.
-
-Theorem Zopp_NEG : (x:positive) (Zopp (NEG x)) = (POS x).
-Proof.
-Induction x; Auto with arith.
-Qed.
-
-Hints Resolve Zero_left Zero_right.
+Hints Local Resolve Zero_left Zero_right.
 
 Theorem weak_assoc :
   (x,y:positive)(z:Z) (Zplus (POS x) (Zplus (POS y) z))=
@@ -1041,7 +1503,7 @@ Intros x y z';Case z'; [
       Rewrite add_sym; Trivial with arith ]]].
 Qed.
 
-Hints Resolve weak_assoc.
+Hints Local Resolve weak_assoc.
 
 Theorem Zplus_assoc :
   (x,y,z:Z) (Zplus x (Zplus y z))= (Zplus (Zplus x y) z).
@@ -1077,65 +1539,6 @@ Proof.
 Intros; Elim H; Elim H0; Auto with arith.
 Qed.
 
-(** Addition on positive numbers *)
-
-Fixpoint times [x:positive] : positive -> positive:=
-  [y:positive]
-  Cases x of
-    (xI x') => (add y (xO (times x' y)))
-  | (xO x') => (xO (times x' y))
-  | xH => y
-  end.
-
-V8Infix "*" times : positive_scope.
-
-(** Correctness of multiplication on positive *)
-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.
-
-Theorem times_assoc :
-  ((x,y,z:positive) (times x (times y z))= (times (times x y) z)).
-Proof.
-Intros x y z;Apply convert_intro; Do 4 Rewrite times_convert;
-Apply mult_assoc_l.
-Qed.
-
-Theorem times_sym : (x,y:positive) (times x y) = (times y x).
-Proof.
-Intros x y; Apply convert_intro; Do 2 Rewrite times_convert; Apply mult_sym.
-Qed.
-
-(** Multiplication on integers *)
-Definition Zmult := [x,y:Z]
-  <Z>Cases x of
-      ZERO => ZERO
-    | (POS x') =>
-          <Z>Cases y of
-               ZERO => ZERO
-             | (POS y') => (POS (times x' y'))
-             | (NEG y') => (NEG (times x' y'))
-             end
-    | (NEG x') =>
-          <Z>Cases y of
-               ZERO => ZERO
-             | (POS y') => (NEG (times x' y'))
-             | (NEG y') => (POS (times x' y'))
-             end
-    end.
-
-V8Infix "*" Zmult : Z_scope.
-
-(*Open Scope Z_scope.*)
-
 Theorem Zmult_sym : (x,y:Z) (Zmult x y) = (Zmult y x).
 Proof.
 Induction x; Induction y; Simpl; Auto with arith; Intro q; Rewrite (times_sym p q); Auto with arith.
@@ -1154,29 +1557,6 @@ Proof.
 Induction x; Simpl; Unfold times; Auto with arith.
 Qed.
 
-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;Apply convert_intro;Rewrite times_convert;
-Do 2 Rewrite convert_add; Do 2 Rewrite times_convert;
-Do 3 Rewrite (mult_sym (convert x)); Apply mult_plus_distr.
-Qed.
-
-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.
-
 Theorem Zero_mult_left: (x:Z) (Zmult ZERO x) = ZERO.
 Proof.
 Induction x; Auto with arith.
@@ -1187,7 +1567,7 @@ Proof.
 Induction x; Auto with arith.
 Qed.
 
-Hints Resolve Zero_mult_left Zero_mult_right.
+Hints Local Resolve Zero_mult_left Zero_mult_right.
 
 (* Multiplication and Opposite *)
 Theorem Zopp_Zmult:
@@ -1238,35 +1618,13 @@ Intros x y z; Case x; [
   Apply weak_Zmult_plus_distr_r ].
 Qed.
 
-(** Comparison on integers *)
-Definition Zcompare := [x,y:Z]
-  <relation>Cases x of
-      ZERO => <relation>Cases y of
-                ZERO => EGAL
-              | (POS y') => INFERIEUR
-              | (NEG y') => SUPERIEUR
-              end
-   | (POS x') => <relation>Cases y of
-                ZERO => SUPERIEUR
-              | (POS y') => (compare x' y' EGAL)
-              | (NEG y') => SUPERIEUR
-              end
-   | (NEG x') => <relation>Cases y of
-               ZERO => INFERIEUR
-             | (POS y') => INFERIEUR
-             | (NEG y') => (Op (compare x' y' EGAL))
-             end
-  end.
-
-V8Infix "?=" Zcompare (at level 50, no associativity) : Z_scope.
-
 Theorem Zcompare_EGAL : (x,y:Z) (Zcompare x y) = EGAL <-> x = y.
 Proof.
 Intros x y;Split; [
   Case x;Case y;Simpl;Auto with arith; Try (Intros;Discriminate H); [
     Intros x' y' H; Rewrite (compare_convert_EGAL y' x' H); Trivial with arith
   | Intros x' y' H; Rewrite (compare_convert_EGAL y' x'); [
-      Trivial with arith
+      Trivial
     | Generalize H; Case (compare y' x' EGAL);
       Trivial with arith Orelse (Intros C;Discriminate C)]]
 | Intros E;Rewrite E; Case y; [
@@ -1293,18 +1651,6 @@ Intros x y;Split; [
        Trivial with arith Orelse (Intros H2;Discriminate H2)]))].
 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.
-
 Theorem Zcompare_Zopp :
   (x,y:Z) (Zcompare x y) = (Zcompare (Zopp y) (Zopp x)).
 Proof.
@@ -1312,20 +1658,21 @@ Proof.
 Intros;Rewrite <- ZC4;Trivial with arith.
 Qed.
 
-Hints Resolve convert_compare_EGAL.
+Hints Local Resolve convert_compare_EGAL.
 
 Theorem weaken_Zcompare_Zplus_compatible : 
   ((x,y:Z) (z:positive) 
     (Zcompare (Zplus (POS z) x) (Zplus (POS z) y)) = (Zcompare x y)) ->
    (x,y,z:Z) (Zcompare (Zplus z x) (Zplus z y)) = (Zcompare x y).
 Proof.
-(Intros H x y z;Case x;Case y;Case z;Auto with arith;
-Try (Intros; Rewrite Zcompare_Zopp; Do 2 Rewrite Zopp_Zplus;
-     Rewrite Zopp_NEG; Rewrite H; Simpl; Auto with arith));
-Try (Intros; Simpl; Rewrite <- ZC4; Auto with arith).
+Intro H; NewDestruct z; [
+  Reflexivity
+| Apply H
+| Rewrite (Zcompare_Zopp x y); Rewrite Zcompare_Zopp; 
+  Do 2 Rewrite Zopp_Zplus; Rewrite Zopp_NEG; Apply H ].
 Qed.
 
-Hints Resolve ZC4.
+Hints Local Resolve ZC4.
 
 Theorem weak_Zcompare_Zplus_compatible : 
   (x,y:Z) (z:positive) 
@@ -1530,8 +1877,6 @@ Intros x y;Case x;Case y; [
   Simpl; Rewrite (ZC1 q p H); Trivial with arith].
 Qed.
 
-End fast_integers.
-
 V7only [
   Comments "Compatibility with the old version of times and times_convert".
   Syntactic Definition times1 :=
@@ -1539,10 +1884,3 @@ V7only [
   Syntactic Definition times1_convert :=
     [x,y:positive;_:positive->positive](times_convert x y).
 ].
-
-V8Infix "+" add   : positive_scope.
-V8Infix "*" times : positive_scope.
-V8Infix "+" Zplus : Z_scope.
-V8Infix "*" Zmult : Z_scope.
-V8Notation "- x" := (Zopp x) : Z_scope.
-V8Infix "?=" Zcompare (at level 50, no associativity) : Z_scope.