Documentation/Structuration

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

5 files changed, 1673 insertions, 1214 deletions

diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 753a33e47c..a9c7ebfee5 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -20,53 +20,8 @@ Open Local Scope Z_scope.
 
 Set Implicit Arguments.
 
-Lemma Zmult_zero : (x,y:Z)`x*y=0` -> `x=0` \/ `y=0`.
-NewDestruct x; NewDestruct y; Auto.
-Simpl; Intros; Discriminate H.
-Simpl; Intros; Discriminate H.
-Simpl; Intros; Discriminate H.
-Simpl; Intros; Discriminate H.
-Qed.
-
-Lemma Zeq_Zminus : (x,y:Z)x=y -> `x-y = 0`.
-Intros; Omega.
-Qed.
+Implicit Variable Type x,y,z:Z.
 
-Lemma Zminus_Zeq : (x,y:Z)`x-y=0` -> x=y.
-Intros; Omega.
-Qed.
-
-Lemma Zmult_Zminus_distr_l : (x,y,z:Z)`(x-y)*z = x*z - y*z`.
-Intros; Unfold Zminus.
-Rewrite <- Zopp_Zmult.
-Apply Zmult_plus_distr_l.
-Qed.
-
-Lemma  Zmult_Zminus_distr_r : (x,y,z:Z)`z*(x-y) = z*x - z*y`.
-Intros; Rewrite (Zmult_sym z `x-y`).
-Rewrite (Zmult_sym  z x).
-Rewrite (Zmult_sym z y).
-Apply Zmult_Zminus_distr_l.
-Qed.
-
-Lemma Zmult_reg_left : (x,y,z:Z)`z<>0` -> `z*x=z*y` -> x=y.
-Intros.
-Generalize (Zeq_Zminus H0).
-Intro.
-Apply Zminus_Zeq.
-Rewrite <- Zmult_Zminus_distr_r in H1.
-Elim (Zmult_zero H1).
-Omega.
-Trivial.
-Qed.
-
-Lemma Zmult_reg_right : (x,y,z:Z)`z<>0` -> `x*z=y*z` -> x=y.
-Intros x y z Hz.
-Rewrite (Zmult_sym x z).
-Rewrite (Zmult_sym y z).
-Intro; Apply Zmult_reg_left with z; Assumption.
-Qed.
-    
 Lemma Zgt0_le_pred : (y:Z) `y > 0` -> `0 <= (Zpred y)`.
 Intro; Unfold Zpred; Omega.
 Qed.
@@ -175,6 +130,8 @@ Left ; Split with (NEG p); Reflexivity.
 Right ; Split with `-1`; Reflexivity.
 Qed.
 
+
+(**********************************************************************)
 (** The biggest power of 2 that is stricly less than [a]
 
     Easy to compute: replace all "1" of the binary representation by
@@ -217,6 +174,7 @@ Simpl; Omega.
 Qed.
 
 
+(**********************************************************************)
 (** Two more induction principles over [Z]. *)
 
 Theorem Z_lt_abs_rec : (P: Z -> Set)
@@ -284,10 +242,12 @@ Ring.
 Omega.
 Save.
 
+(**********************************************************************)
 (** A list length in Z, tail recursive.  *)
+
 Require PolyList.
 
-Fixpoint Zlength_aux [acc: Z; A: Set; l:(list A)] : Z := Cases l of 
+Fixpoint Zlength_aux [acc: Z; A:Set; l:(list A)] : Z := Cases l of 
     nil => acc
   | (cons _ l) => (Zlength_aux (Zs acc) A l)
 end. 
@@ -295,35 +255,46 @@ end.
 Definition Zlength := (Zlength_aux 0).
 Implicits Zlength [1].
 
-Lemma Zlength_correct : (A:Set)(l:(list A))(Zlength l)=(inject_nat (length l)).
+Section Zlength_properties.
+
+Variable A:Set.
+
+Implicit Variable Type l:(list A).
+
+Lemma Zlength_correct : (l:(list A))(Zlength l)=(inject_nat (length l)).
 Proof.
-Assert (A:Set)(l:(list A))(acc:Z)(Zlength_aux acc A l)=acc+(inject_nat (length l)). 
+Assert (l:(list A))(acc:Z)(Zlength_aux acc A l)=acc+(inject_nat (length l)). 
 Induction l.
 Simpl; Auto with zarith.
 Intros; Simpl (length (cons a l0)); Rewrite inj_S.
 Simpl; Rewrite H; Auto with zarith.
 Unfold Zlength; Intros; Rewrite H; Auto.
 Qed.
-Implicits Zlength_correct [1].
 
-Lemma Zlength_nil : (A:Set)(Zlength 1!A (nil A))=0.
+Lemma Zlength_nil : (Zlength 1!A (nil A))=0.
 Proof.
 Auto.
 Qed.
 
-Lemma Zlength_cons : (A:Set)(x:A)(l:(list A))(Zlength (cons x l))=(Zs (Zlength l)).
+Lemma Zlength_cons : (x:A)(l:(list A))(Zlength (cons x l))=(Zs (Zlength l)).
 Proof.
 Intros; Do 2 Rewrite Zlength_correct.
 Simpl (length (cons x l)); Rewrite inj_S; Auto.
 Qed.
-Implicits Zlength_cons [1].
 
-Lemma Zlength_nil_inv : (A:Set)(l:(list A))(Zlength l)=0 -> l=(nil ?).
+Lemma Zlength_nil_inv : (l:(list A))(Zlength l)=0 -> l=(nil ?).
 Proof.
-Intros A l; Rewrite Zlength_correct.
+Intro l; Rewrite Zlength_correct.
 Case l; Auto.
 Intros x l'; Simpl (length (cons x l')).
 Rewrite inj_S.
 Intros; ElimType False; Generalize (ZERO_le_inj (length l')); Omega.
 Qed.
+
+End Zlength_properties.
+
+Implicits Zlength_correct [1].
+Implicits Zlength_cons [1].
 Implicits Zlength_nil_inv [1].
+
+(**********************************************************************)
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index a4cf3a9b34..7e153c8dd1 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -16,58 +16,8 @@ Require Bool.
 V7only [Import Z_scope.].
 Open Local Scope Z_scope.
 
-(** Overview of the sections of this file:
-    - logic: Logic complements.
-    - numbers: a few very simple lemmas for manipulating the
-      constructors [POS], [NEG], [ZERO] and [xI], [xO], [xH]
-    - registers: defining arrays of bits and their relation with integers.
-    - iter: the n-th iterate of a function is defined for [n:nat] and 
-      [n:positive].
-      The two notions are identified and an invariant conservation theorem
-      is proved.
-    - recursors: Here a nat-like recursor is built.
-    - arith: lemmas about [< <= ?= + *]
-*)
-
-Section logic.
-
-Lemma rename : (A:Set)(P:A->Prop)(x:A) ((y:A)(x=y)->(P y)) -> (P x).
-Auto with arith. 
-Qed.
-
-End logic.
-
-Section numbers.
-
-Definition entier_of_Z :=
-  [z:Z]Cases z of ZERO => Nul | (POS p) => (Pos p) | (NEG p) => (Pos p) end.
-Definition Z_of_entier :=
-  [x:entier]Cases x of Nul => ZERO | (Pos p) => (POS p) end.
- 
-(* Coercion Z_of_entier : entier >-> Z. *)
-
-Lemma POS_xI : (p:positive) (POS (xI p))=`2*(POS p) + 1`.
-Intro; Apply refl_equal.
-Qed.
-Lemma POS_xO : (p:positive) (POS (xO p))=`2*(POS p)`.
-Intro; Apply refl_equal.
-Qed.
-Lemma NEG_xI : (p:positive) (NEG (xI p))=`2*(NEG p) - 1`.
-Intro; Apply refl_equal.
-Qed.
-Lemma NEG_xO : (p:positive) (NEG (xO p))=`2*(NEG p)`.
-Intro; Apply refl_equal.
-Qed.
-
-Lemma POS_add : (p,p':positive)`(POS (add p p'))=(POS p)+(POS p')`.
-Induction p; Induction p'; Simpl; Auto with arith.
-Qed.
-
-Lemma NEG_add : (p,p':positive)`(NEG (add p p'))=(NEG p)+(NEG p')`.
-Induction p; Induction p'; Simpl; Auto with arith.
-Qed.
-
-(** Boolean comparisons *)
+(**********************************************************************)
+(** Boolean comparisons of binary integers *)
 
 Definition Zle_bool := 
   [x,y:Z]Cases `x ?= y` of SUPERIEUR => false | _ => true end.
@@ -106,9 +56,94 @@ Intros x y; Unfold Zgt_bool Zgt Zle.
 Case (Zcompare x y); Auto; Discriminate.
 Qed.
 
-End numbers.
+(** Lemmas on [Zle_bool] used in contrib/graphs *)
+
+Lemma Zle_bool_imp_le : (x,y:Z) (Zle_bool x y)=true -> (Zle x y).
+Proof.
+  Unfold Zle_bool Zle. Intros x y. Unfold not. 
+  Case (Zcompare x y); Intros; Discriminate.
+Qed.
+
+Lemma Zle_imp_le_bool : (x,y:Z) (Zle x y) -> (Zle_bool x y)=true.
+Proof.
+  Unfold Zle Zle_bool. Intros x y. Case (Zcompare x y); Trivial. Intro. Elim (H (refl_equal ? ?)).
+Qed.
+
+Lemma Zle_bool_refl : (x:Z) (Zle_bool x x)=true.
+Proof.
+  Intro. Apply Zle_imp_le_bool. Apply Zle_refl. Reflexivity.
+Qed.
+
+Lemma Zle_bool_antisym : (x,y:Z) (Zle_bool x y)=true -> (Zle_bool y x)=true -> x=y.
+Proof.
+  Intros. Apply Zle_antisym. Apply Zle_bool_imp_le. Assumption.
+  Apply Zle_bool_imp_le. Assumption.
+Qed.
+
+Lemma Zle_bool_trans : (x,y,z:Z) (Zle_bool x y)=true -> (Zle_bool y z)=true -> (Zle_bool x z)=true.
+Proof.
+  Intros. Apply Zle_imp_le_bool. Apply Zle_trans with m:=y. Apply Zle_bool_imp_le. Assumption.
+  Apply Zle_bool_imp_le. Assumption.
+Qed.
+
+Definition Zle_bool_total : (x,y:Z) {(Zle_bool x y)=true}+{(Zle_bool y x)=true}.
+Proof.
+  Intros. Unfold Zle_bool. Cut (Zcompare x y)=SUPERIEUR<->(Zcompare y x)=INFERIEUR.
+  Case (Zcompare x y). Left . Reflexivity.
+  Left . Reflexivity.
+  Right . Rewrite (proj1 ? ? H (refl_equal ? ?)). Reflexivity.
+  Apply Zcompare_ANTISYM.
+Defined.
+
+Lemma Zle_bool_plus_mono : (x,y,z,t:Z) (Zle_bool x y)=true -> (Zle_bool z t)=true ->
+                                (Zle_bool (Zplus x z) (Zplus y t))=true.
+Proof.
+  Intros. Apply Zle_imp_le_bool. Apply Zle_plus_plus. Apply Zle_bool_imp_le. Assumption.
+  Apply Zle_bool_imp_le. Assumption.
+Qed.
+
+Lemma Zone_pos : (Zle_bool `1` `0`)=false.
+Proof.
+  Reflexivity.
+Qed.
+
+Lemma Zone_min_pos : (x:Z) (Zle_bool x `0`)=false -> (Zle_bool `1` x)=true.
+Proof.
+  Intros. Apply Zle_imp_le_bool. Change (Zle (Zs ZERO) x). Apply Zgt_le_S. Generalize H.
+  Unfold Zle_bool Zgt. Case (Zcompare x ZERO). Intro H0. Discriminate H0.
+  Intro H0. Discriminate H0.
+  Reflexivity.
+Qed.
+
+
+ Lemma Zle_is_le_bool : (x,y:Z) (Zle x y) <-> (Zle_bool x y)=true.
+  Proof.
+    Intros. Split. Intro. Apply Zle_imp_le_bool. Assumption.
+    Intro. Apply Zle_bool_imp_le. Assumption.
+  Qed.
+
+  Lemma Zge_is_le_bool : (x,y:Z) (Zge x y) <-> (Zle_bool y x)=true.
+  Proof.
+    Intros. Split. Intro. Apply Zle_imp_le_bool. Apply Zge_le. Assumption.
+    Intro. Apply Zle_ge. Apply Zle_bool_imp_le. Assumption.
+  Qed.
+
+  Lemma Zlt_is_le_bool : (x,y:Z) (Zlt x y) <-> (Zle_bool x `y-1`)=true.
+  Proof.
+    Intros. Split. Intro. Apply Zle_imp_le_bool. Apply Zlt_n_Sm_le. Rewrite (Zs_pred y) in H.
+    Assumption.
+    Intro. Rewrite (Zs_pred y). Apply Zle_lt_n_Sm. Apply Zle_bool_imp_le. Assumption.
+  Qed.
+
+  Lemma Zgt_is_le_bool : (x,y:Z) (Zgt x y) <-> (Zle_bool y `x-1`)=true.
+  Proof.
+    Intros. Apply iff_trans with `y < x`. Split. Exact (Zgt_lt x y).
+    Exact (Zlt_gt y x).
+    Exact (Zlt_is_le_bool y x).
+  Qed.
 
-Section iterate.
+(**********************************************************************)
+(** Iterators *)
 
 (** [n]th iteration of the function [f] *)
 Fixpoint iter_nat[n:nat]  : (A:Set)(f:A->A)A->A :=
@@ -188,33 +223,8 @@ Theorem iter_pos_invariant :
 Intros; Rewrite iter_convert; Apply iter_nat_invariant; Trivial with arith.
 Qed.
 
-End iterate.
-
-
-Section arith.
-
-Lemma POS_gt_ZERO : (p:positive) `(POS p) > 0`.
-Unfold Zgt; Trivial.
-Qed.
-
-(* weaker but useful (in [Zpower] for instance) *)
-Lemma ZERO_le_POS : (p:positive) `0 <= (POS p)`.
-Intro; Unfold Zle; Unfold Zcompare; Discriminate.
-Qed.
-
-Lemma Zlt_ZERO_pred_le_ZERO : (x:Z) `0 < x` -> `0 <= (Zpred x)`.
-Intros.
-Rewrite (Zs_pred x) in H.
-Apply Zgt_S_le.
-Apply Zlt_gt.
-Assumption.
-Qed.
-
-Lemma NEG_lt_ZERO : (p:positive)`(NEG p) < 0`.
-Unfold Zlt; Trivial.
-Qed.
-
 
+(**********************************************************************)
 (** [Zeven], [Zodd], [Zdiv2] and their related properties *)
 
 Definition Zeven := 
@@ -254,10 +264,6 @@ Proof.
     (Right; Compute; Exact I) Orelse (Left; Compute; Exact I)
   | Intro p; Case p; Intros; 
     (Right; Compute; Exact I) Orelse (Left; Compute; Exact I) ].
-  (*i was 
-  Realizer Zeven_bool.
-  Repeat Program; Compute; Trivial.
-  i*)
 Defined.
 
 Definition Zeven_dec : (z:Z) { (Zeven z) }+{ ~(Zeven z) }.
@@ -268,10 +274,6 @@ Proof.
     (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) 
   | Intro p; Case p; Intros; 
     (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ].
-  (*i was 
-  Realizer Zeven_bool.
-  Repeat Program; Compute; Trivial.
-  i*)
 Defined.
 
 Definition Zodd_dec : (z:Z) { (Zodd z) }+{ ~(Zodd z) }.
@@ -282,10 +284,6 @@ Proof.
     (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) 
   | Intro p; Case p; Intros; 
     (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ].
-  (*i was 
-  Realizer Zodd_bool.
-  Repeat Program; Compute; Trivial.
-  i*)
 Defined.
 
 Lemma Zeven_not_Zodd : (z:Z)(Zeven z) -> ~(Zodd z).
@@ -324,14 +322,10 @@ Qed.
 
 Hints Unfold Zeven Zodd : zarith.
 
-(** [Zdiv2] is defined on all [Z], but notice that for odd negative integers
-    it is not the euclidean quotient: in that case we have [n = 2*(n/2)-1] *)
-
-Definition Zdiv2_pos :=
-  [z:positive]Cases z of xH => xH
-                       | (xO p) => p
-		       | (xI p) => p
-		      end.
+(**********************************************************************)
+(** [Zdiv2] is defined on all [Z], but notice that for odd negative
+    integers it is not the euclidean quotient: in that case we have [n =
+    2*(n/2)-1] *)
 
 Definition Zdiv2 :=
   [z:Z]Cases z of ZERO => ZERO
@@ -399,249 +393,3 @@ Rewrite Zplus_assoc; Assumption.
 Right; Reflexivity.
 Qed.
 
-(* Very simple *)
-Lemma Zminus_Zplus_compatible :
-  (x,y,n:Z) `(x+n) - (y+n) = x - y`.
-Intros.
-Unfold Zminus.
-Rewrite -> Zopp_Zplus.
-Rewrite -> (Zplus_sym (Zopp y) (Zopp n)).
-Rewrite -> Zplus_assoc.
-Rewrite <- (Zplus_assoc x n (Zopp n)).
-Rewrite -> (Zplus_inverse_r n).
-Rewrite <- Zplus_n_O.
-Reflexivity.
-Qed.
-
-(** Decompose an egality between two [?=] relations into 3 implications *)
-Theorem Zcompare_egal_dec :
-   (x1,y1,x2,y2:Z)
-    (`x1 < y1`->`x2 < y2`)
-     ->(`x1 ?= y1`=EGAL -> `x2 ?= y2`=EGAL)
-        ->(`x1 > y1`->`x2 > y2`)->`x1 ?= y1`=`x2 ?= y2`.
-Intros x1 y1 x2 y2.
-Unfold Zgt; Unfold Zlt;
-Case `x1 ?= y1`; Case `x2 ?= y2`; Auto with arith; Symmetry; Auto with arith.
-Qed.
-
-Theorem Zcompare_elim :
-  (c1,c2,c3:Prop)(x,y:Z)
-    ((x=y) -> c1) ->(`x < y` -> c2) ->(`x > y`-> c3)
-       -> Cases `x ?= y`of EGAL => c1 | INFERIEUR => c2 | SUPERIEUR => c3 end.
-
-Intros.
-Apply rename with x:=`x ?= y`; Intro r; Elim r;
-[ Intro; Apply H; Apply (let (h1, h2)=(Zcompare_EGAL x y) in h1); Assumption
-| Unfold Zlt in H0; Assumption
-| Unfold Zgt in H1; Assumption ].
-Qed.
-
-Lemma Zcompare_x_x : (x:Z) `x ?= x` = EGAL.
-Intro; Apply let (h1,h2) = (Zcompare_EGAL x x) in h2.
-Apply refl_equal.
-Qed.
-
-Lemma Zlt_not_eq : (x,y:Z)`x < y` -> ~x=y.
-Proof.
-Intros.
-Unfold Zlt in H.
-Unfold not.
-Intro.
-Generalize (proj2 ? ? (Zcompare_EGAL x y) H0).
-Intro.
-Rewrite H1 in H.
-Discriminate H.
-Qed.
-
-Lemma Zcompare_eq_case : 
-  (c1,c2,c3:Prop)(x,y:Z) c1 -> x=y ->
-  Cases `x ?= y` of EGAL => c1 | INFERIEUR => c2 | SUPERIEUR => c3 end.
-Intros.
-Rewrite -> (Case (Zcompare_EGAL x y) of [h1,h2: ?]h2 end H0).
-Assumption.
-Qed.
-
-(** Four very basic lemmas about [Zle], [Zlt], [Zge], [Zgt] *)
-Lemma Zle_Zcompare :
-  (x,y:Z)`x <= y` ->
-  Cases `x ?= y` of EGAL => True | INFERIEUR => True | SUPERIEUR => False end.
-Intros x y; Unfold Zle; Elim `x ?=y`; Auto with arith.
-Qed.
-
-Lemma Zlt_Zcompare :
-  (x,y:Z)`x < y`  ->
-  Cases `x ?= y` of EGAL => False | INFERIEUR => True | SUPERIEUR => False end.
-Intros x y; Unfold Zlt; Elim `x ?=y`; Intros; Discriminate Orelse Trivial with arith.
-Qed.
-
-Lemma Zge_Zcompare :
-  (x,y:Z)` x >= y`->
-  Cases `x ?= y` of EGAL => True | INFERIEUR => False | SUPERIEUR => True end.
-Intros x y; Unfold Zge; Elim `x ?=y`; Auto with arith. 
-Qed.
-
-Lemma Zgt_Zcompare :
-  (x,y:Z)`x > y` ->
-  Cases `x ?= y` of EGAL => False | INFERIEUR => False | SUPERIEUR => True end.
-Intros x y; Unfold Zgt; Elim `x ?= y`; Intros; Discriminate Orelse Trivial with arith.
-Qed.
-
-(** Lemmas about [Zmin] *)
-
-Lemma Zmin_plus : (x,y,n:Z) `(Zmin (x+n)(y+n))=(Zmin x y)+n`.
-Intros; Unfold Zmin.
-Rewrite (Zplus_sym x n);
-Rewrite (Zplus_sym y n);
-Rewrite (Zcompare_Zplus_compatible x y n).
-Case `x ?= y`; Apply Zplus_sym.
-Qed.
-
-(** Lemmas about [absolu] *)
-
-Lemma absolu_lt : (x,y:Z) `0 <= x < y` -> (lt (absolu x) (absolu y)).
-Proof.
-Intros x y. Case x; Simpl. Case y; Simpl.
-
-Intro. Absurd `0 < 0`. Compute. Intro H0. Discriminate H0. Intuition.
-Intros. Elim (ZL4 p). Intros. Rewrite H0. Auto with arith.
-Intros. Elim (ZL4 p). Intros. Rewrite H0. Auto with arith.
-
-Case y; Simpl.
-Intros. Absurd `(POS p) < 0`. Compute. Intro H0. Discriminate H0. Intuition.
-Intros. Change (gt (convert p) (convert p0)).
-Apply compare_convert_SUPERIEUR.
-Elim H; Auto with arith. Intro. Exact (ZC2 p0 p).
-
-Intros. Absurd `(POS p0) < (NEG p)`.
-Compute. Intro H0. Discriminate H0. Intuition.
-
-Intros. Absurd `0 <= (NEG p)`. Compute. Auto with arith. Intuition.
-Qed.
-
-(** Lemmas on [Zle_bool] used in contrib/graphs *)
-
-Lemma Zle_bool_imp_le : (x,y:Z) (Zle_bool x y)=true -> (Zle x y).
-Proof.
-  Unfold Zle_bool Zle. Intros x y. Unfold not. 
-  Case (Zcompare x y); Intros; Discriminate.
-Qed.
-
-Lemma Zle_imp_le_bool : (x,y:Z) (Zle x y) -> (Zle_bool x y)=true.
-Proof.
-  Unfold Zle Zle_bool. Intros x y. Case (Zcompare x y); Trivial. Intro. Elim (H (refl_equal ? ?)).
-Qed.
-
-Lemma Zle_bool_refl : (x:Z) (Zle_bool x x)=true.
-Proof.
-  Intro. Apply Zle_imp_le_bool. Apply Zle_refl. Reflexivity.
-Qed.
-
-Lemma Zle_bool_antisym : (x,y:Z) (Zle_bool x y)=true -> (Zle_bool y x)=true -> x=y.
-Proof.
-  Intros. Apply Zle_antisym. Apply Zle_bool_imp_le. Assumption.
-  Apply Zle_bool_imp_le. Assumption.
-Qed.
-
-Lemma Zle_bool_trans : (x,y,z:Z) (Zle_bool x y)=true -> (Zle_bool y z)=true -> (Zle_bool x z)=true.
-Proof.
-  Intros. Apply Zle_imp_le_bool. Apply Zle_trans with m:=y. Apply Zle_bool_imp_le. Assumption.
-  Apply Zle_bool_imp_le. Assumption.
-Qed.
-
-Definition Zle_bool_total : (x,y:Z) {(Zle_bool x y)=true}+{(Zle_bool y x)=true}.
-Proof.
-  Intros. Unfold Zle_bool. Cut (Zcompare x y)=SUPERIEUR<->(Zcompare y x)=INFERIEUR.
-  Case (Zcompare x y). Left . Reflexivity.
-  Left . Reflexivity.
-  Right . Rewrite (proj1 ? ? H (refl_equal ? ?)). Reflexivity.
-  Apply Zcompare_ANTISYM.
-Defined.
-
-Lemma Zle_bool_plus_mono : (x,y,z,t:Z) (Zle_bool x y)=true -> (Zle_bool z t)=true ->
-                                (Zle_bool (Zplus x z) (Zplus y t))=true.
-Proof.
-  Intros. Apply Zle_imp_le_bool. Apply Zle_plus_plus. Apply Zle_bool_imp_le. Assumption.
-  Apply Zle_bool_imp_le. Assumption.
-Qed.
-
-Lemma Zone_pos : (Zle_bool `1` `0`)=false.
-Proof.
-  Reflexivity.
-Qed.
-
-Lemma Zone_min_pos : (x:Z) (Zle_bool x `0`)=false -> (Zle_bool `1` x)=true.
-Proof.
-  Intros. Apply Zle_imp_le_bool. Change (Zle (Zs ZERO) x). Apply Zgt_le_S. Generalize H.
-  Unfold Zle_bool Zgt. Case (Zcompare x ZERO). Intro H0. Discriminate H0.
-  Intro H0. Discriminate H0.
-  Reflexivity.
-Qed.
-
-
- Lemma Zle_is_le_bool : (x,y:Z) (Zle x y) <-> (Zle_bool x y)=true.
-  Proof.
-    Intros. Split. Intro. Apply Zle_imp_le_bool. Assumption.
-    Intro. Apply Zle_bool_imp_le. Assumption.
-  Qed.
-
-  Lemma Zge_is_le_bool : (x,y:Z) (Zge x y) <-> (Zle_bool y x)=true.
-  Proof.
-    Intros. Split. Intro. Apply Zle_imp_le_bool. Apply Zge_le. Assumption.
-    Intro. Apply Zle_ge. Apply Zle_bool_imp_le. Assumption.
-  Qed.
-
-  Lemma Zlt_is_le_bool : (x,y:Z) (Zlt x y) <-> (Zle_bool x `y-1`)=true.
-  Proof.
-    Intros. Split. Intro. Apply Zle_imp_le_bool. Apply Zlt_n_Sm_le. Rewrite (Zs_pred y) in H.
-    Assumption.
-    Intro. Rewrite (Zs_pred y). Apply Zle_lt_n_Sm. Apply Zle_bool_imp_le. Assumption.
-  Qed.
-
-  Lemma Zgt_is_le_bool : (x,y:Z) (Zgt x y) <-> (Zle_bool y `x-1`)=true.
-  Proof.
-    Intros. Apply iff_trans with `y < x`. Split. Exact (Zgt_lt x y).
-    Exact (Zlt_gt y x).
-    Exact (Zlt_is_le_bool y x).
-  Qed.
-
-End arith.
-
-(** Equivalence between inequalities used in contrib/graph *)
-
-
-  Lemma Zle_plus_swap : (x,y,z:Z) `x+z<=y` <-> `x<=y-z`.
-  Proof.
-    Intros. Split. Intro. Rewrite <- (Zero_right x). Rewrite <- (Zplus_inverse_r z).
-    Rewrite Zplus_assoc_l. Exact (Zle_reg_r ? ? ? H).
-    Intro. Rewrite <- (Zero_right y). Rewrite <- (Zplus_inverse_l z). Rewrite Zplus_assoc_l.
-    Apply Zle_reg_r. Assumption.
-  Qed.
-
-  Lemma Zge_iff_le : (x,y:Z) `x>=y` <-> `y<=x`.
-  Proof.
-    Intros. Split. Intro. Apply Zge_le. Assumption.
-    Intro. Apply Zle_ge. Assumption.
-  Qed.
-
-  Lemma Zlt_plus_swap : (x,y,z:Z) `x+z<y` <-> `x<y-z`.
-  Proof.
-    Intros. Split. Intro. Unfold Zminus. Rewrite Zplus_sym. Rewrite <- (Zero_left x).
-    Rewrite <- (Zplus_inverse_l z). Rewrite Zplus_assoc_r. Apply Zlt_reg_l. Rewrite Zplus_sym.
-    Assumption.
-    Intro. Rewrite Zplus_sym. Rewrite <- (Zero_left y). Rewrite <- (Zplus_inverse_r z).
-    Rewrite Zplus_assoc_r. Apply Zlt_reg_l. Rewrite Zplus_sym. Assumption.
-  Qed.
-
-  Lemma Zgt_iff_lt : (x,y:Z) `x>y` <-> `y<x`.
-  Proof.
-    Intros. Split. Intro. Apply Zgt_lt. Assumption.
-    Intro. Apply Zlt_gt. Assumption.
-  Qed.
-
-  Lemma Zeq_plus_swap : (x,y,z:Z) `x+z=y` <-> `x=y-z`.
-  Proof.
-    Intros. Split. Intro. Rewrite <- H. Unfold Zminus. Rewrite Zplus_assoc_r.
-    Rewrite Zplus_inverse_r. Apply sym_eq. Apply Zero_right.
-    Intro. Rewrite H. Unfold Zminus. Rewrite Zplus_assoc_r. Rewrite Zplus_inverse_l.
-    Apply Zero_right.
-  Qed.
diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index b376e31beb..aa34a201e3 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -17,12 +17,10 @@ Require Decidable.
 Require Peano_dec.
 Require Export Compare_dec.
 
+Open Local Scope Z_scope.
 
 Definition neq := [x,y:nat] ~(x=y).
 Definition Zne := [x,y:Z] ~(x=y).
-Theorem add_un_Zs : (x:positive) (POS (add_un x)) = (Zs (POS x)).
-Intro; Rewrite -> ZL12; Unfold Zs; Simpl; Trivial with arith.
-Qed.
 
 Theorem inj_S : (y:nat) (inject_nat (S y)) = (Zs (inject_nat y)).
 Induction y; [
@@ -32,11 +30,6 @@ Induction y; [
   Rewrite add_un_Zs; Trivial with arith].
 Qed.
  
-Theorem Zplus_S_n: (x,y:Z) (Zplus (Zs x) y) = (Zs (Zplus x y)).
-Intros x y; Unfold Zs; Rewrite (Zplus_sym (Zplus x y)); Rewrite Zplus_assoc;
-Rewrite (Zplus_sym (POS xH)); Trivial with arith.
-Qed.
-
 Theorem inj_plus : 
   (x,y:nat) (inject_nat (plus x y)) = (Zplus (inject_nat x) (inject_nat y)).
 
@@ -254,29 +247,16 @@ Intros x y H; Apply Zsimpl_gt_plus_r with (Zopp y).
 Rewrite Zplus_inverse_r; Trivial.
 Qed.
 
-Theorem Zopp_one : (x:Z)(Zopp x)=(Zmult x (NEG xH)).
-Induction x; Intros; Rewrite Zmult_sym; Auto with arith.
-Qed.
-
-Theorem Zopp_Zmult_r : (x,y:Z)(Zopp (Zmult x y)) = (Zmult x (Zopp y)).
-Intros x y; Rewrite Zmult_sym; Rewrite <- Zopp_Zmult; Apply Zmult_sym.
-Qed.
-
-Theorem Zmult_Zopp_left :  (x,y:Z)(Zmult (Zopp x) y) = (Zmult x (Zopp y)).
-Intros; Rewrite Zopp_Zmult; Rewrite Zopp_Zmult_r; Trivial with arith.
-Qed.
-
-Theorem Zopp_Zmult_l : (x,y:Z)(Zopp (Zmult x y)) = (Zmult (Zopp x) y).
-Intros x y; Symmetry; Apply Zopp_Zmult.
-Qed.
+(**********************************************************************)
+(** Omega lemmas *)
 
 Theorem Zred_factor0 : (x:Z) x = (Zmult x (POS xH)).
-Intro x; Rewrite (Zmult_n_1 x); Trivial with arith.
+Intro x; Rewrite (Zmult_n_1 x); Reflexivity.
 Qed.
 
 Theorem Zred_factor1 : (x:Z) (Zplus x x) = (Zmult x (POS (xO xH))).
-Intros x; Pattern 1 2 x ; Rewrite <- (Zmult_n_1 x);
-Rewrite <- Zmult_plus_distr_r; Auto with arith.
+Proof.
+Exact Zplus_Zmult_2.
 Qed.
 
 Theorem Zred_factor2 :
@@ -307,73 +287,6 @@ Theorem Zred_factor6 : (x:Z) x = (Zplus x ZERO).
 Intro; Rewrite Zero_right; Trivial with arith.
 Qed.
 
-Theorem Zcompare_Zplus_compatible2 :
-  (r:relation)(x,y,z,t:Z)
-    (Zcompare x y) = r -> (Zcompare z t) = r ->
-    (Zcompare (Zplus x z) (Zplus y t)) = r.
-
-Intros r x y z t; Case r; [
-  Intros H1 H2; Elim (Zcompare_EGAL x y); Elim (Zcompare_EGAL z t);
-  Intros H3 H4 H5 H6; Rewrite H3; [ 
-    Rewrite H5; [ Elim (Zcompare_EGAL (Zplus y t) (Zplus y t)); Auto with arith | Auto with arith ]
-  | Auto with arith ]
-| Intros H1 H2; Elim (Zcompare_ANTISYM (Zplus y t) (Zplus x z));
-  Intros H3 H4; Apply H3;
-  Apply Zcompare_trans_SUPERIEUR with y:=(Zplus y z) ; [
-    Rewrite Zcompare_Zplus_compatible;
-    Elim (Zcompare_ANTISYM t z); Auto with arith
-  | Do 2 Rewrite <- (Zplus_sym z); 
-    Rewrite Zcompare_Zplus_compatible;
-    Elim (Zcompare_ANTISYM y x); Auto with arith]
-| Intros H1 H2;
-  Apply Zcompare_trans_SUPERIEUR with y:=(Zplus x t) ; [
-    Rewrite Zcompare_Zplus_compatible; Assumption
-  | Do 2 Rewrite <- (Zplus_sym t);
-    Rewrite Zcompare_Zplus_compatible; Assumption]].
-Qed.
-
-Theorem Zcompare_Zmult_compatible : 
-   (x:positive)(y,z:Z)
-      (Zcompare (Zmult (POS x) y) (Zmult (POS x) z)) = (Zcompare y z).
-
-Induction x; [
-  Intros p H y z;
-  Cut (POS (xI p))=(Zplus (Zplus (POS p) (POS p)) (POS xH)); [
-    Intros E; Rewrite E; Do 4 Rewrite Zmult_plus_distr_l; 
-    Do 2 Rewrite Zmult_one;
-    Apply Zcompare_Zplus_compatible2; [
-      Apply Zcompare_Zplus_compatible2; Apply H
-    | Trivial with arith]
-  | Simpl; Rewrite (add_x_x p); Trivial with arith]
-| Intros p H y z; Cut (POS (xO p))=(Zplus (POS p) (POS p)); [
-    Intros E; Rewrite E; Do 2 Rewrite Zmult_plus_distr_l;
-      Apply Zcompare_Zplus_compatible2; Apply H
-    | Simpl; Rewrite (add_x_x p); Trivial with arith]
-  | Intros y z; Do 2 Rewrite Zmult_one; Trivial with arith].
-Qed.
-
-Theorem Zmult_eq:
-  (x,y:Z) ~(x=ZERO) -> (Zmult y x) = ZERO -> y = ZERO.
-
-Intros x y; Case x; [
-  Intro; Absurd ZERO=ZERO; Auto with arith
-| Intros p H1 H2; Elim (Zcompare_EGAL y ZERO);
-  Intros H3 H4; Apply H3; Rewrite <- (Zcompare_Zmult_compatible p);
-  Rewrite -> Zero_mult_right; Rewrite -> Zmult_sym;
-  Elim (Zcompare_EGAL (Zmult y (POS p)) ZERO); Auto with arith
-| Intros p H1 H2; Apply Zopp_intro; Simpl;
-  Elim (Zcompare_EGAL (Zopp y) ZERO); Intros H3 H4; Apply H3;
-  Rewrite <- (Zcompare_Zmult_compatible p);
-  Rewrite -> Zero_mult_right; Rewrite -> Zmult_sym;
-  Rewrite -> Zmult_Zopp_left; Simpl;
-  Elim (Zcompare_EGAL (Zmult y (NEG p)) ZERO); Auto with arith].
-Qed.
-
-Theorem Z_eq_mult:
-  (x,y:Z)  y = ZERO -> (Zmult y x) = ZERO.
-Intros x y H; Rewrite H; Auto with arith.
-Qed.
-
 Theorem Zmult_le:
   (x,y:Z) (Zgt x ZERO) -> (Zle ZERO (Zmult y x)) -> (Zle ZERO y).
 
diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v
index 43be524191..59ee28cd5b 100644
--- a/theories/ZArith/fast_integer.v
+++ b/theories/ZArith/fast_integer.v
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 (***********************************************************)
-(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 (***********************************************************)
 
 (**********************************************************************)
@@ -162,6 +162,8 @@ with sub_neg [x,y:positive]:positive_mask :=
 Definition true_sub := [x,y:positive] 
   Cases (sub_pos x y) of (IsPos z) => z | _ => xH  end.
 
+V8Infix "-" true_sub : positive_scope.
+
 (** Multiplication on binary positive numbers *)
 
 Fixpoint times [x:positive] : positive -> positive:=
@@ -174,6 +176,16 @@ Fixpoint times [x:positive] : positive -> positive:=
 
 V8Infix "*" times : positive_scope.
 
+(** Division by 2 rounded below but for 1 *)
+
+Definition Zdiv2_pos :=
+  [z:positive]Cases z of xH => xH
+                       | (xO p) => p
+		       | (xI p) => p
+		      end.
+
+V8Infix "/" Zdiv2_pos : positive_scope.
+
 (**********************************************************************)
 (** Comparison on binary positive numbers *)
 
@@ -253,6 +265,10 @@ 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.
 Induction x; Auto.
 Qed.
@@ -270,7 +286,7 @@ Qed.
 
 (** Specification of [xI] in term of [Psucc] and [xO] *)
 
-Lemma xI_add_un_xO : (p:positive)(xI p) = (add_un (xO p)).
+Lemma xI_add_un_xO : (x:positive)(xI x) = (add_un (xO x)).
 Proof.
 Reflexivity.
 Qed.
@@ -467,31 +483,6 @@ 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.
-  NewDestruct q; Simpl; Try Rewrite is_double_moins_un; Reflexivity.
-Qed.
-
 Lemma add_xI_double_moins_un :
   (p,q:positive)(xO (add p q)) = (add (xI p) (double_moins_un q)).
 Proof.
@@ -500,8 +491,10 @@ 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)).
+(* xO_xI_plus_double_moins_un = add_xI_double_moins_un *)
+
+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 IHp|p IHp|]; NewDestruct q as [q|q|];
  Simpl; Try Rewrite ZL13; Try Rewrite double_moins_un_add_un_xI;
@@ -509,6 +502,8 @@ NewInduction p as [p IHp|p IHp|]; NewDestruct q as [q|q|];
  Rewrite <- is_double_moins_un; Rewrite ZL12bis; Reflexivity. 
 Qed.
 
+(* double_moins_un_add = double_moins_un_plus_xO_double_moins_un *)
+
 (** Misc *)
 
 Lemma add_x_x : (x:positive) (add x x) = (xO x).
@@ -517,6 +512,75 @@ NewInduction x; Simpl; Try Rewrite ZL13; Try Rewrite IHx; Reflexivity.
 Qed.
 
 (**********************************************************************)
+(** Peano induction on binary positive positive numbers *)
+
+Fixpoint add_iter [x:positive] : positive -> positive := 
+  [y]Cases x of 
+  | xH => (add_un y)
+  | (xO x) => (add_iter x (add_iter x y))
+  | (xI x) => (add_iter x (add_iter x (add_un y)))
+  end.
+
+Lemma add_iter_add : (x,y:positive)(add_iter x y)=(add x y).
+Proof.
+NewInduction x as [p IHp|p IHp|]; NewDestruct y; Simpl;
+  Reflexivity Orelse Do 2 Rewrite IHp; Rewrite add_assoc; Rewrite add_x_x;
+  Try Reflexivity.
+Rewrite ZL13; Rewrite <- ZL14; Reflexivity.
+Rewrite ZL12; Reflexivity.
+Qed.
+
+Lemma add_iter_xO : (x:positive)(add_iter x x)=(xO x).
+Proof.
+Intro; Rewrite <- add_x_x; Apply add_iter_add.
+Qed.
+
+Lemma add_iter_xI : (x:positive)(add_un (add_iter x x))=(xI x).
+Proof.
+Intro; Rewrite xI_add_un_xO; Rewrite <- add_x_x; 
+  Apply (f_equal positive); Apply add_iter_add.
+Qed.
+
+Lemma iterate_add : (P:(positive->Type))
+  ((n:positive)(P n) ->(P (add_un n)))->(p,n:positive)(P n) ->
+  (P (add_iter p n)).
+Proof.
+Intros P H; NewInduction p; Simpl; Intros.
+Apply IHp; Apply IHp; Apply H; Assumption.
+Apply IHp; Apply IHp; Assumption.
+Apply H; Assumption.
+Defined.
+
+(** Peano induction *)
+
+Theorem Pind : (P:(positive->Prop))
+  (P xH) ->((n:positive)(P n) ->(P (add_un n))) ->(n:positive)(P n).
+Proof.
+Intros P H1 Hsucc; NewInduction n.
+Rewrite <- add_iter_xI; Apply Hsucc; Apply iterate_add; Assumption.
+Rewrite <- add_iter_xO; Apply iterate_add; Assumption.
+Assumption.
+Qed.
+
+(** Peano recursion *)
+
+Definition Prec : (A:Set)A->(positive->A->A)->positive->A :=
+  [A;a;f]Fix Prec { Prec [p:positive] : A :=
+  Cases p of
+  | xH => a
+  | (xO p) => (iterate_add [_]A f p p (Prec p))
+  | (xI p) => (f (add_iter p p) (iterate_add [_]A f p p (Prec p)))
+  end}.
+
+(** Test *)
+
+Check
+ let fact = (Prec positive xH [p;r](times (add_un p) r)) in
+ let seven = (xI (xI xH)) in
+ let five_thousand_forty= (xO(xO(xO(xO(xI(xI(xO(xI(xI(xI(xO(xO xH))))))))))))
+ in ((refl_equal ? ?) :: (fact seven) = five_thousand_forty).
+
+(**********************************************************************)
 (** Properties of minus on binary positive numbers *)
 
 (* Properties of subtraction *)
@@ -656,6 +720,7 @@ Qed.
 
 Require Le.
 Require Lt.
+Require Gt.
 Require Plus.
 Require Mult.
 Require Minus.
@@ -754,6 +819,13 @@ Intros x y; NewInduction x as [ x' H | x' H | ]; [
   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).
+].
 
 (** IPN is strictly positive *)
 
@@ -1016,8 +1088,8 @@ Qed.
 
 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.
+Intros x y;ElimPcompare y x; 
+Intros E;Rewrite E;Simpl; [Apply ZC3 | Apply ZC2 | Apply ZC1 ]; Assumption.
 Qed.
 
 (**********************************************************************)
@@ -1231,75 +1303,6 @@ Rewrite times_sym with x:=x; Rewrite times_sym with x:=y; Assumption.
 Qed.
 
 (**********************************************************************)
-(** Peano induction on binary positive positive numbers *)
-
-Fixpoint add_iter [x:positive] : positive -> positive := 
-  [y]Cases x of 
-  | xH => (add_un y)
-  | (xO x) => (add_iter x (add_iter x y))
-  | (xI x) => (add_iter x (add_iter x (add_un y)))
-  end.
-
-Lemma add_iter_add : (p,q:positive)(add_iter p q)=(add p q).
-Proof.
-NewInduction p as [p IHp|p IHp|]; NewDestruct q; Simpl;
-  Reflexivity Orelse Do 2 Rewrite IHp; Rewrite add_assoc; Rewrite add_x_x;
-  Try Reflexivity.
-Rewrite ZL13; Rewrite <- ZL14; Reflexivity.
-Rewrite ZL12; Reflexivity.
-Qed.
-
-Lemma add_iter_xO : (p:positive)(add_iter p p)=(xO p).
-Proof.
-Intro; Rewrite <- add_x_x; Apply add_iter_add.
-Qed.
-
-Lemma add_iter_xI : (p:positive)(add_un (add_iter p p))=(xI p).
-Proof.
-Intro; Rewrite xI_add_un_xO; Rewrite <- add_x_x; 
-  Apply (f_equal positive); Apply add_iter_add.
-Qed.
-
-Lemma iterate_add : (P:(positive->Type))
-  ((n:positive)(P n) ->(P (add_un n)))->(p,n:positive)(P n) ->
-  (P (add_iter p n)).
-Proof.
-Intros P H; NewInduction p; Simpl; Intros.
-Apply IHp; Apply IHp; Apply H; Assumption.
-Apply IHp; Apply IHp; Assumption.
-Apply H; Assumption.
-Defined.
-
-(** Peano induction *)
-
-Theorem Pind : (P:(positive->Prop))
-  (P xH) ->((n:positive)(P n) ->(P (add_un n))) ->(n:positive)(P n).
-Proof.
-Intros P H1 Hsucc; NewInduction n.
-Rewrite <- add_iter_xI; Apply Hsucc; Apply iterate_add; Assumption.
-Rewrite <- add_iter_xO; Apply iterate_add; Assumption.
-Assumption.
-Qed.
-
-(** Peano recursion *)
-
-Definition Prec : (A:Set)A->(positive->A->A)->positive->A :=
-  [A;a;f]Fix Prec { Prec [p:positive] : A :=
-  Cases p of
-  | xH => a
-  | (xO p) => (iterate_add [_]A f p p (Prec p))
-  | (xI p) => (f (add_iter p p) (iterate_add [_]A f p p (Prec p)))
-  end}.
-
-(** Test *)
-
-Check
- let fact = (Prec positive xH [p;r](times (add_un p) r)) in
- let seven = (xI (xI xH)) in
- let five_thousand_forty= (xO(xO(xO(xO(xI(xI(xO(xI(xI(xI(xO(xO xH))))))))))))
- in ((refl_equal ? ?) :: (fact seven) = five_thousand_forty).
-
-(**********************************************************************)
 (** Binary natural numbers *)
 
 Inductive entier: Set := Nul : entier | Pos : positive -> entier.
@@ -1337,6 +1340,28 @@ Definition Nmult := [n,m]
   | (Pos p) (Pos q) => (Pos (times p q))
   end.
 
+(** Order *)
+
+Definition Ncompare := [n,m]
+  Cases n m of
+  | Nul      Nul      => EGAL
+  | Nul      (Pos m') => INFERIEUR
+  | (Pos n') Nul      => SUPERIEUR
+  | (Pos n') (Pos m') => (compare n' m' EGAL)
+  end.
+
+(** Peano induction on binary natural numbers *)
+
+Theorem Nind : (P:(entier ->Prop))
+  (P Nul) ->((n:entier)(P n) ->(P (Nsucc n))) ->(n:entier)(P n).
+Proof.
+NewDestruct n.
+  Assumption.
+  Apply Pind with P := [p](P (Pos p)).
+Exact (H0 Nul H).
+Intro p'; Exact (H0 (Pos p')).
+Qed.
+
 (** Properties of addition *)
 
 Theorem Nplus_0_l : (n:entier)(Nplus Nul n)=n.
@@ -1366,6 +1391,32 @@ NewDestruct p; Try Reflexivity.
 Simpl; Rewrite add_assoc; Reflexivity.
 Qed.
 
+Theorem Nplus_succ : (n,m:entier)(Nplus (Nsucc n) m)=(Nsucc (Nplus n m)).
+Proof.
+NewDestruct n; NewDestruct m.
+  Simpl; Reflexivity.
+  Unfold Nsucc Nplus; Rewrite <- ZL12bis; Reflexivity.
+  Simpl; Reflexivity.
+  Simpl; Rewrite ZL14bis; Reflexivity.
+Qed.
+
+Theorem Nsucc_inj : (n,m:entier)(Nsucc n)=(Nsucc m)->n=m.
+Proof.
+NewDestruct n; NewDestruct m; Simpl; Intro H; 
+  Reflexivity Orelse Injection H; Clear H; Intro H.
+  Symmetry in H; Contradiction add_un_not_un with p.
+  Contradiction add_un_not_un with p.
+  Rewrite add_un_inj with 1:=H; Reflexivity.
+Qed.
+
+Theorem Nplus_reg_l : (n,m,p:entier)(Nplus n m)=(Nplus n p)->m=p.
+Proof.
+Intro n; Pattern n; Apply Nind; Clear n; Simpl.
+  Trivial.
+  Intros n IHn m p H0; Do 2 Rewrite Nplus_succ in H0.
+  Apply IHn; Apply Nsucc_inj; Assumption.
+Qed.
+
 (** Properties of multiplication *)
 
 Theorem Nmult_1_l : (n:entier)(Nmult (Pos xH) n)=n.
@@ -1413,16 +1464,18 @@ Left; NewDestruct n; NewDestruct m; Reflexivity Orelse Try Discriminate H.
 Injection H; Clear H; Intro H; Rewrite simpl_times_r with 1:=H; Reflexivity.
 Qed. 
 
-(** Peano induction on binary natural numbers *)
+Theorem Nmult_0_l : (n:entier) (Nmult Nul n) = Nul.
+Proof.
+Reflexivity.
+Qed.
 
-Theorem Nind : (P:(entier ->Prop))
-  (P Nul) ->((n:entier)(P n) ->(P (Nsucc n))) ->(n:entier)(P n).
+(** Properties of comparison *)
+
+Theorem Ncompare_Eq_eq : (n,m:entier) (Ncompare n m) = EGAL -> n = m.
 Proof.
-NewDestruct n.
-  Assumption.
-  Apply Pind with P := [p](P (Pos p)).
-Exact (H0 Nul H).
-Intro p'; Exact (H0 (Pos p')).
+NewDestruct n as [|n]; NewDestruct m as [|m]; Simpl; Intro H;
+  Reflexivity Orelse Try Discriminate H.
+  Rewrite (compare_convert_EGAL n m H); Reflexivity.
 Qed.
 
 (**********************************************************************)
@@ -1436,10 +1489,10 @@ 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 ].
+Arguments Scope POS [ positive_scope ].
+Arguments Scope NEG [ positive_scope ].
 
-(** Addition on integers *)
+(** Subtraction of positive into Z *)
 
 Definition Zdouble_plus_one [x:Z] :=
   Cases x of 
@@ -1475,6 +1528,8 @@ Fixpoint Zsub_pos[x,y:positive]:Z :=
   | xH      xH      => ZERO
   end.
 
+(** Addition on integers *)
+
 Definition Zplus := [x,y:Z]
   Cases x y of
     ZERO      y       => y
@@ -1508,6 +1563,20 @@ Definition Zopp := [x:Z]
 
 V8Notation "- x" := (Zopp x) : Z_scope.
 
+(** Successor on integers *)
+
+Definition Zs := [x:Z](Zplus x (POS xH)).
+
+(** Predecessor on integers *)
+
+Definition Zpred := [x:Z](Zplus x (NEG xH)).
+
+(** Subtraction on integers *)
+
+Definition Zminus := [m,n:Z](Zplus m (Zopp n)).
+
+V8Infix "-" Zminus : Z_scope.
+
 (** Multiplication on integers *)
 
 Definition Zmult := [x,y:Z]
@@ -1539,9 +1608,65 @@ Definition Zcompare := [x,y:Z]
 
 V8Infix "?=" Zcompare (at level 70, no associativity) : Z_scope.
 
+Tactic Definition ElimCompare com1 com2:=
+  Case (Dcompare (Zcompare com1 com2)); [ Idtac | 
+     Let x = FreshId "H" In Intro x; Case x; Clear x ].
+
+(** Sign function *)
+
+Definition Zsgn [z:Z] : Z :=
+  Cases z of 
+     ZERO   => ZERO
+  | (POS p) => (POS xH)
+  | (NEG p) => (NEG xH)
+  end.
+
+(* Easier to handle variants of successor and addition *)
+
+Definition Zs' [x:Z] :=
+  Cases x of
+  | ZERO => (POS xH)
+  | (POS x') => (POS (add_un x'))
+  | (NEG x') => (Zsub_pos xH x')
+  end.
+
+Definition Zpred' [x:Z] :=
+  Cases x of
+  | ZERO => (NEG xH)
+  | (POS x') => (Zsub_pos x' xH)
+  | (NEG x') => (NEG (add_un x'))
+  end.
+
+Definition Zplus' := [x,y:Z]
+  Cases x y of
+    ZERO      y       => y
+  | x         ZERO    => x
+  | (POS x') (POS y') => (POS (add x' y'))
+  | (POS x') (NEG y') => (Zsub_pos x' y')
+  | (NEG x') (POS y') => (Zsub_pos y' x')
+  | (NEG x') (NEG y') => (NEG (add x' y'))
+  end.
+
 Open Local Scope Z_scope.
 
 (**********************************************************************)
+(** Inductive specification of Z *)
+
+Theorem Zind : (P:(Z ->Prop))
+  (P ZERO) -> ((x:Z)(P x) ->(P (Zs' x))) -> ((x:Z)(P x) ->(P (Zpred' x))) ->
+     (z:Z)(P z).
+Proof.
+Intros P H0 Hs Hp; NewDestruct z.
+  Assumption.
+  Apply Pind with P:=[p](P (POS p)).
+    Change (P (Zs' ZERO)); Apply Hs; Apply H0.
+    Intro n; Exact (Hs (POS n)).
+ Apply Pind with P:=[p](P (NEG p)).
+    Change (P (Zpred' ZERO)); Apply Hp; Apply H0.
+    Intro n; Exact (Hp (NEG n)).
+Qed.
+
+(**********************************************************************)
 (** Properties of opposite on binary integer numbers *)
 
 Theorem Zopp_NEG : (x:positive) (Zopp (NEG x)) = (POS x).
@@ -1568,6 +1693,215 @@ Intros x y;Case x;Case y;Simpl;Intros; [
 Qed.
 
 (**********************************************************************)
+(** Properties of the double of an integer *)
+
+Lemma Zopp_Zdouble : (x:Z) (Zopp (Zdouble x))=(Zdouble (Zopp x)).
+Proof.
+NewDestruct x as [|p|p]; Reflexivity.
+Qed.
+
+Lemma Zopp_Zdouble_plus_one :
+  (x:Z) (Zopp (Zdouble_plus_one x))=(Zdouble_minus_one (Zopp x)).
+Proof.
+NewDestruct x as [|p|p]; Reflexivity.
+Qed.
+
+Lemma Zopp_Zdouble_minus_one :
+  (x:Z) (Zopp (Zdouble_minus_one x))=(Zdouble_plus_one (Zopp x)).
+Proof.
+NewDestruct x as [|p|p]; Reflexivity.
+Qed.
+
+Lemma Zdouble_minus_one_spec :
+  (x:Z)(Zdouble_minus_one x) = (Zplus (Zdouble x) (NEG xH)).
+Proof.
+NewDestruct x as [|p|p]; Reflexivity Orelse Exact (POS_Zdouble_minus_one p).
+Qed.
+
+Lemma Zdouble_minus_one_add_un_xI :
+ (x:positive) (Zdouble_minus_one (POS (add_un x))) = (POS (xI x)).
+Proof.
+NewDestruct x; Simpl; Try Rewrite double_moins_un_add_un_xI; Reflexivity.
+Qed.
+
+(** Permutations *)
+
+Lemma Zdouble_plus_one_Zdouble :
+  (x:Z)(Zdouble_plus_one (Zdouble x))=(Zdouble_minus_one (Zdouble_plus_one x)).
+Proof.
+NewDestruct x; Reflexivity.
+Qed.
+
+Lemma Zdouble_plus_one_Zdouble_minus_one :
+ (x:Z)(Zdouble_plus_one (Zdouble_minus_one x))=(Zdouble_minus_one (Zdouble x)).
+Proof.
+NewDestruct x; Reflexivity.
+Qed.
+
+Lemma Zdouble_plus_one_spec :
+  (x:Z)(Zdouble_plus_one x)=(Zplus (Zdouble x) (POS xH)).
+Proof.
+  NewDestruct x; Reflexivity.
+Qed.
+
+Lemma Zdouble_plus_one_Zdouble_minus_one_one :
+  (x:Z)(Zdouble_plus_one x)=(Zdouble_minus_one (Zs' x)).
+Proof.
+NewDestruct x; Simpl.
+  Reflexivity.
+  Rewrite -> double_moins_un_add_un_xI; Reflexivity.
+  NewDestruct p; Reflexivity.
+Qed.
+
+Lemma Zdouble_one_one_Zdouble_plus_one:
+  (x:Z)(Zdouble (Zs' x)) = (Zs' (Zdouble_plus_one x)).
+Proof.
+NewDestruct x as [|p|p]; Try Reflexivity.
+  NewDestruct p; Reflexivity.
+Qed.
+
+(**********************************************************************)
+(** Properties of the subtraction from positive to integers *)
+
+Infix Local 4 "--" Zsub_pos : Z_scope.
+
+Lemma Zsub_pos_x_x : (x:positive) x--x = ZERO.
+Proof.
+NewInduction x as [p IHp|p IHp|]; Simpl; Try Rewrite IHp; Reflexivity.
+Qed.
+
+Lemma Zopp_Zsub_pos : (x,y:positive) (Zopp (x--y)) = y--x.
+Proof.
+NewInduction x as [p IHp|p IHp|]; NewDestruct y as [q|q|]; Simpl; 
+  Try Rewrite <- IHp; Try Reflexivity.
+  Apply Zopp_Zdouble.
+  Apply Zopp_Zdouble_plus_one.
+  Apply Zopp_Zdouble_minus_one.
+  Apply Zopp_Zdouble.
+Qed.
+
+Lemma Zsub_pos_add_un_permute : 
+  (x,y:positive)(add_un x)--y = (Zs' (x--y)).
+Proof.
+NewInduction x as [x IHx|x|]; NewDestruct y as [y|y|]; Simpl.
+  (* xI/xI *)
+  Rewrite IHx; Simpl.
+  NewDestruct (Zsub_pos x y); Simpl; Try Reflexivity.
+    NewDestruct p; Simpl; Try Reflexivity.
+      Rewrite double_moins_un_add_un_xI; Reflexivity.
+    NewDestruct p; Reflexivity.
+  (* xI/xO *)
+  Rewrite IHx; Simpl.
+  NewDestruct (Zsub_pos x y); Simpl; Try Reflexivity.
+    NewDestruct p; Reflexivity.
+  Rewrite double_moins_un_add_un_xI; Reflexivity.
+  (* xO/xI *)
+  NewDestruct (Zsub_pos x y); Simpl; Try Reflexivity.
+  NewDestruct p; Simpl; Try Rewrite is_double_moins_un; Reflexivity.
+  (* xO/xO *)
+  NewDestruct (Zsub_pos x y); Simpl; Reflexivity.
+  (* xO/xH *)
+  NewDestruct x; Simpl; Try Reflexivity.
+  Rewrite is_double_moins_un; Reflexivity.
+  (* xH/xI *)
+  NewDestruct y; Reflexivity.
+  (* xH/xO *)
+  NewDestruct y; Reflexivity.
+  (* xH/xH *)
+  Reflexivity.
+Qed.
+
+Lemma Zsub_pos_add_un_permute_Zopp :
+  (x,y:positive) x--(add_un y) = (Zopp (Zs' (Zopp (x--y)))).
+Proof.
+Intros.
+Rewrite Zopp_Zsub_pos; Rewrite <- Zopp_Zsub_pos; 
+Rewrite Zsub_pos_add_un_permute; Reflexivity.
+Qed.
+
+Lemma Zsub_pos_double_moins_un_xO_add_un :
+ (x,y:positive)(Zsub_pos (double_moins_un x) y) = (Zsub_pos (xO x) (add_un y)).
+Proof.
+NewInduction x as [p IHp|p|]; NewDestruct y as [q|q|]; Simpl;
+  Try Rewrite -> IHp; Try Reflexivity.
+  Rewrite Zsub_pos_add_un_permute_Zopp;
+      Change (xI p) with (add_un (xO p));
+      Rewrite Zsub_pos_add_un_permute;
+      NewDestruct (Zsub_pos (xO p) q).
+    Reflexivity.
+    NewDestruct p0; Simpl; Try Rewrite double_moins_un_add_un_xI; Reflexivity.
+    NewDestruct p0; Simpl; Try Rewrite is_double_moins_un; Try Reflexivity.
+  NewDestruct q; Simpl.
+    Rewrite Zdouble_plus_one_Zdouble_minus_one; Reflexivity.
+    Rewrite Zdouble_plus_one_Zdouble; Reflexivity.
+    Reflexivity.
+  Rewrite Zsub_pos_add_un_permute_Zopp; Simpl; 
+      NewDestruct (Zsub_pos (xO p) q); Simpl.
+    Reflexivity.
+    NewDestruct p0; Reflexivity.
+    Rewrite double_moins_un_add_un_xI; Reflexivity.
+  Rewrite Zsub_pos_add_un_permute_Zopp; Simpl;
+    NewDestruct q; Simpl; Try Rewrite is_double_moins_un; Reflexivity.
+  NewDestruct q; Reflexivity.
+Qed.
+
+Lemma Zdouble_minus_one_Zsub_pos :
+  (x,y:positive)(Zdouble_minus_one (Zsub_pos x y))
+     = (Zsub_pos (double_moins_un x) (xO y)).
+Proof.
+Intros; Rewrite Zsub_pos_double_moins_un_xO_add_un; Reflexivity.
+Qed.
+
+Lemma Zdouble_plus_one_Zsub_pos :
+  (x,y:positive)(Zdouble_plus_one (x--y)) = (xO x)--(double_moins_un y).
+Proof.
+Intros; Rewrite <- Zopp_Zsub_pos with y := (xO x);
+Rewrite <- Zdouble_minus_one_Zsub_pos;
+Rewrite <- Zopp_Zsub_pos with y := y;
+Rewrite <- Zopp_Zdouble_plus_one;
+Rewrite Zopp_Zopp;
+Reflexivity.
+Qed.
+
+Lemma Zsub_pos_xI_double_moins_un :
+  (x,y:positive)
+  (Zdouble (Zs' (Zsub_pos x y))) = (Zsub_pos (xI x) (double_moins_un y)).
+Proof.
+Intros; Change (xI x) with (add_un (xO x));
+Rewrite -> Zsub_pos_add_un_permute; Rewrite <- Zdouble_plus_one_Zsub_pos.
+Apply Zdouble_one_one_Zdouble_plus_one.
+Qed.
+
+Lemma Zpred'_Zs' : (x:Z)(Zpred' (Zs' x))=x.
+Proof.
+NewDestruct x; Simpl.
+  Reflexivity.
+NewDestruct p; Simpl; Try Rewrite double_moins_un_add_un_xI; Reflexivity.
+NewDestruct p; Simpl; Try Rewrite is_double_moins_un; Reflexivity.
+Qed.
+
+Lemma add_un_discr : (x:positive)(add_un x)<>x.
+Proof.
+NewDestruct x; Discriminate.
+Qed.
+
+Lemma double_moins_un_xO_discr : (x:positive)(double_moins_un x)<>(xO x).
+Proof.
+NewDestruct x; Discriminate.
+Qed.
+
+Lemma Z0_Zs'_discr : (x:Z)(Zs' x)<>x.
+Proof.
+NewDestruct x; Simpl.
+  Discriminate.
+  Injection; Apply add_un_discr.
+  NewDestruct p; Simpl.
+    Discriminate.
+    Injection; Apply double_moins_un_xO_discr.
+    Discriminate.
+Qed.
+
+(**********************************************************************)
 (** Other properties of binary integer numbers *)
 
 Hints Local Resolve compare_convert_O.
@@ -1577,47 +1911,55 @@ Proof.
 Reflexivity.
 Qed.
 
-(** Addition on integers *)
+(**********************************************************************)
+(** Properties of the addition on integers *)
+
+(** zero is left neutral for addition *)
 
 Theorem Zero_left: (x:Z) (Zplus ZERO x) = x.
 Proof.
-Induction x; Auto with arith.
+NewDestruct x; Reflexivity.
 Qed.
 
-(** Addition and opposite *)
+(** zero is right neutral for addition *)
+
 Theorem Zero_right: (x:Z) (Zplus x ZERO) = x.
 Proof.
-Induction x; Auto with arith.
+NewDestruct x; Reflexivity.
 Qed.
 
+(** opposite is right inverse for addition *)
+
 Theorem Zplus_inverse_r: (x:Z) (Zplus x (Zopp x)) = ZERO.
 Proof.
-Induction x; [
-  Simpl;Auto with arith
-| Simpl; Intros p;Rewrite (convert_compare_EGAL p); Auto with arith
-| Simpl; Intros p;Rewrite (convert_compare_EGAL p); Auto with arith ].
+NewDestruct x as [|p|p]; Simpl; [
+  Reflexivity
+| Rewrite (convert_compare_EGAL p); Reflexivity
+| Rewrite (convert_compare_EGAL p); Reflexivity ].
 Qed.
 
+(** opposite distributes over addition *)
+
 Theorem Zopp_Zplus: 
   (x,y:Z) (Zopp (Zplus x y)) = (Zplus (Zopp x) (Zopp y)).
 Proof.
-(Intros x y;Case x;Case y;Auto with arith);
-Intros p q;Simpl;Case (compare q p EGAL);Auto with arith.
+NewDestruct x as [|p|p]; NewDestruct y as [|q|q]; Simpl;
+  Reflexivity Orelse NewDestruct  (compare p q EGAL); Reflexivity.
 Qed.
 
+(** addition is commutative *)
+
 Theorem Zplus_sym: (x,y:Z) (Zplus x y) = (Zplus y x).
 Proof.
-Induction x;Induction y;Simpl;Auto with arith; [
-  Intros q;Rewrite add_sym;Auto with arith
-| Intros q; Rewrite (ZC4 q p);
-  (Elim (Dcompare (compare p q EGAL));[Idtac|Intros H;Elim H]);
-  Intros E;Rewrite E;Auto with arith
-| Intros q; Rewrite (ZC4 q p);
-  (Elim (Dcompare (compare p q EGAL));[Idtac|Intros H;Elim H]);
-  Intros E;Rewrite E;Auto with arith
-| Intros q;Rewrite add_sym;Auto with arith ].
+NewInduction x as [|p|p];NewDestruct y as [|q|q];Simpl;Try Reflexivity.
+  Rewrite add_sym; Reflexivity.
+  Rewrite ZC4; NewDestruct (compare q p EGAL); Reflexivity.
+  Rewrite ZC4; NewDestruct (compare q p EGAL); Reflexivity.
+  Rewrite add_sym; Reflexivity.
 Qed.
 
+(** opposite is left inverse for addition *)
+
 Theorem Zplus_inverse_l: (x:Z) (Zplus (Zopp x) x) = ZERO.
 Proof.
 Intro; Rewrite Zplus_sym; Apply Zplus_inverse_r.
@@ -1625,6 +1967,8 @@ Qed.
 
 Hints Local Resolve Zero_left Zero_right.
 
+(** addition is associative *)
+
 Theorem weak_assoc :
   (x,y:positive)(z:Z) (Zplus (POS x) (Zplus (POS y) z))=
                        (Zplus (Zplus (POS x) (POS y)) z).
@@ -1632,40 +1976,38 @@ Proof.
 Intros x y z';Case z'; [
   Auto with arith
 | Intros z;Simpl; Rewrite add_assoc;Auto with arith
-| Intros z; Simpl;
-  (Elim (Dcompare (compare y z EGAL));[Idtac|Intros H;Elim H;Clear  H]);
+| Intros z; Simpl; ElimPcompare y z;
   Intros E0;Rewrite E0;
-  (Elim (Dcompare (compare (add x y) z EGAL));[Idtac|Intros H;Elim H;
-    Clear H]);Intros E1;Rewrite E1; [
-    Absurd (compare (add x y) z EGAL)=EGAL; [    (* Cas 1 *)
+  ElimPcompare '(add x y) 'z;Intros E1;Rewrite E1; [
+    Absurd (compare (add x y) z EGAL)=EGAL; [    (* Case 1 *)
       Rewrite convert_compare_SUPERIEUR; [
         Discriminate
       | Rewrite convert_add; Rewrite (compare_convert_EGAL y z E0);
         Elim (ZL4 x);Intros k E2;Rewrite E2; Simpl; Unfold gt lt; Apply le_n_S;
         Apply le_plus_r ]
     | Assumption ]
-  | Absurd (compare (add x y) z EGAL)=INFERIEUR; [ (* Cas 2 *)
+  | Absurd (compare (add x y) z EGAL)=INFERIEUR; [ (* Case 2 *)
       Rewrite convert_compare_SUPERIEUR; [
         Discriminate
       | Rewrite convert_add; Rewrite (compare_convert_EGAL y z E0);
         Elim (ZL4 x);Intros k E2;Rewrite E2; Simpl; Unfold gt lt; Apply le_n_S;
         Apply le_plus_r]
     | Assumption ]
-  | Rewrite (compare_convert_EGAL y z E0); (* Cas 3 *)
+  | Rewrite (compare_convert_EGAL y z E0); (* Case 3 *)
     Elim (sub_pos_SUPERIEUR (add x z) z);[
       Intros t H; Elim H;Intros H1 H2;Elim H2;Intros H3 H4;
       Unfold true_sub; Rewrite H1; Cut x=t; [
         Intros E;Rewrite E;Auto with arith
       | Apply simpl_add_r with z:=z; Rewrite <- H3; Rewrite add_sym; Trivial with arith ]
     | Pattern 1 z; Rewrite <- (compare_convert_EGAL y z E0); Assumption ]
-  | Elim (sub_pos_SUPERIEUR z y); [ (* Cas 4 *)
+  | Elim (sub_pos_SUPERIEUR z y); [ (* Case 4 *)
       Intros k H;Elim H;Intros H1 H2;Elim H2;Intros H3 H4; Unfold 1 true_sub;
       Rewrite H1; Cut x=k; [
         Intros E;Rewrite E; Rewrite (convert_compare_EGAL k); Trivial with arith
       | Apply simpl_add_r with z:=y; Rewrite (add_sym k y); Rewrite H3;
         Apply compare_convert_EGAL; Assumption ]
     | Apply ZC2;Assumption]
-  | Elim (sub_pos_SUPERIEUR z y); [ (* Cas 5 *)
+  | Elim (sub_pos_SUPERIEUR z y); [ (* Case 5 *)
       Intros k H;Elim H;Intros H1 H2;Elim H2;Intros H3 H4;
       Unfold 1 3 5 true_sub; Rewrite H1;
       Cut (compare x k EGAL)=INFERIEUR; [
@@ -1685,7 +2027,7 @@ Intros x y z';Case z'; [
         Do 2 Rewrite <- convert_add; Apply compare_convert_INFERIEUR;
         Rewrite H3; Rewrite add_sym; Assumption ]
     | Apply ZC2; Assumption ]
-  | Elim (sub_pos_SUPERIEUR z y); [ (* Cas 6 *)
+  | Elim (sub_pos_SUPERIEUR z y); [ (* Case 6 *)
       Intros k H;Elim H;Intros H1 H2;Elim H2;Intros H3 H4;
       Elim (sub_pos_SUPERIEUR (add x y) z); [
         Intros i H5;Elim H5;Intros H6 H7;Elim H7;Intros H8 H9;
@@ -1705,21 +2047,21 @@ Intros x y z';Case z'; [
           Rewrite H3; Rewrite add_sym; Apply ZC1; Assumption ]
       | Assumption ]
     | Apply ZC2;Assumption ]
-  | Absurd (compare (add x y) z EGAL)=EGAL; [ (* Cas 7 *)
+  | Absurd (compare (add x y) z EGAL)=EGAL; [ (* Case 7 *)
       Rewrite convert_compare_SUPERIEUR; [
         Discriminate
       | Rewrite convert_add; Unfold gt;Apply lt_le_trans with m:=(convert y);[
           Apply compare_convert_INFERIEUR; Apply ZC1; Assumption
         | Apply le_plus_r]]
     | Assumption ]
-  | Absurd (compare (add x y) z EGAL)=INFERIEUR; [ (* Cas 8 *)
+  | Absurd (compare (add x y) z EGAL)=INFERIEUR; [ (* Case 8 *)
       Rewrite convert_compare_SUPERIEUR; [
         Discriminate
       | Unfold gt; Apply lt_le_trans with m:=(convert y);[
           Exact (compare_convert_SUPERIEUR y z E0)
         | Rewrite convert_add; Apply le_plus_r]]
     | Assumption ]
-  | Elim sub_pos_SUPERIEUR with 1:=E0;Intros k H1; (* Cas 9 *)
+  | Elim sub_pos_SUPERIEUR with 1:=E0;Intros k H1; (* Case 9 *)
     Elim sub_pos_SUPERIEUR with 1:=E1; Intros i H2;Elim H1;Intros H3 H4;
     Elim H4;Intros H5 H6; Elim H2;Intros H7 H8;Elim H8;Intros H9 H10; 
     Unfold true_sub ;Rewrite H3;Rewrite H7; Cut (add x k)=i; [
@@ -1731,13 +2073,11 @@ Qed.
 
 Hints Local Resolve weak_assoc.
 
-Theorem Zplus_assoc :
+Theorem Zplus_assoc_l :
   (x,y,z:Z) (Zplus x (Zplus y z))= (Zplus (Zplus x y) z).
 Proof.
 Intros x y z;Case x;Case y;Case z;Auto with arith; Intros; [
-(*i  Apply weak_assoc
-| Apply weak_assoc 
-| i*) Rewrite (Zplus_sym (NEG p0)); Rewrite weak_assoc;
+  Rewrite (Zplus_sym (NEG p0)); Rewrite weak_assoc;
   Rewrite (Zplus_sym (Zplus (POS p1) (NEG p0))); Rewrite weak_assoc;
   Rewrite (Zplus_sym (POS p1)); Trivial with arith
 | Apply Zopp_intro; Do 4 Rewrite Zopp_Zplus; 
@@ -1760,54 +2100,320 @@ Intros x y z;Case x;Case y;Case z;Auto with arith; Intros; [
 .
 Qed.
 
-Lemma Zplus_simpl : (n,m,p,q:Z) n=m -> p=q -> (Zplus n p)=(Zplus m q).
+V7only [Notation Zplus_assoc := Zplus_assoc_l.].
+
+Lemma Zplus_assoc_r : (n,m,p:Z)(Zplus (Zplus n m) p) =(Zplus n (Zplus m p)).
 Proof.
-Intros; Elim H; Elim H0; Auto with arith.
+Intros; Symmetry; Apply Zplus_assoc.
 Qed.
 
-Theorem Zmult_sym : (x,y:Z) (Zmult x y) = (Zmult y x).
+(** Associativity mixed with commutativity *)
+
+Lemma Zplus_permute : (n,m,p:Z) (Zplus n (Zplus m p))=(Zplus m (Zplus n p)).
 Proof.
-Induction x; Induction y; Simpl; Auto with arith; Intro q; Rewrite (times_sym p q); Auto with arith.
+Intros n m p;
+Rewrite Zplus_sym;Rewrite <- Zplus_assoc; Rewrite (Zplus_sym p n); Trivial with arith.
 Qed.
 
-Theorem Zmult_assoc :
-  (x,y,z:Z) (Zmult x (Zmult y z))= (Zmult (Zmult x y) z).
+(** addition simplifies *)
+
+Lemma Zsimpl_plus_l : (n,m,p:Z)(Zplus n m)=(Zplus n p)->m=p.
+Intros n m p H; Cut (Zplus (Zopp n) (Zplus n m))=(Zplus (Zopp n) (Zplus n p));[
+  Do 2 Rewrite -> Zplus_assoc; Rewrite -> (Zplus_sym (Zopp n) n);
+  Rewrite -> Zplus_inverse_r;Simpl; Trivial with arith
+| Rewrite -> H; Trivial with arith ].
+Qed.
+
+(** addition and successor permutes *)
+
+Lemma Zplus_S_n: (x,y:Z) (Zplus (Zs x) y) = (Zs (Zplus x y)).
 Proof.
-Induction x; Induction y; Induction z; Simpl; Auto with arith; Intro p1; 
-Rewrite times_assoc; Auto with arith.
+Intros x y; Unfold Zs; Rewrite (Zplus_sym (Zplus x y)); Rewrite Zplus_assoc;
+Rewrite (Zplus_sym (POS xH)); Trivial with arith.
 Qed.
 
-Theorem Zmult_one:
-  (x:Z) (Zmult (POS xH) x) = x.
+Lemma Zplus_n_Sm : (n,m:Z) (Zs (Zplus n m))=(Zplus n (Zs m)).
 Proof.
-Induction x; Simpl; Unfold times; Auto with arith.
+Intros n m; Unfold Zs; Rewrite Zplus_assoc; Trivial with arith.
 Qed.
 
+Lemma Zplus_Snm_nSm : (n,m:Z)(Zplus (Zs n) m)=(Zplus n (Zs m)).
+Proof.
+Unfold Zs ;Intros n m; Rewrite <- Zplus_assoc; Rewrite (Zplus_sym (POS xH));
+Trivial with arith.
+Qed.
+
+(** Misc properties, usually redundant or non natural *)
+
+Lemma Zplus_n_O : (n:Z) n=(Zplus n ZERO).
+Proof.
+Symmetry; Apply Zero_right.
+Qed.
+
+Lemma Zplus_unit_left : (n,m:Z) (Zplus n ZERO)=m -> n=m.
+Proof.
+Intros n m; Rewrite Zero_right; Intro; Assumption.
+Qed.
+
+Lemma Zplus_unit_right : (n,m:Z) n=(Zplus m ZERO) -> n=m.
+Proof.
+Intros n m; Rewrite Zero_right; Intro; Assumption.
+Qed.
+
+Lemma Zplus_simpl : (x,y,z,t:Z) x=y -> z=t -> (Zplus x z)=(Zplus y t).
+Proof.
+Intros; Rewrite H; Rewrite H0; Reflexivity.
+Qed.
+
+Lemma Zplus_Zopp_expand : (x,y,z:Z)
+  (Zplus x (Zopp y))=(Zplus (Zplus x (Zopp z)) (Zplus z (Zopp y))).
+Proof.
+Intros x y z.
+Rewrite <- (Zplus_assoc x).
+Rewrite (Zplus_assoc (Zopp z)).
+Rewrite Zplus_inverse_l.
+Reflexivity.
+Qed.
+
+(**********************************************************************)
+(** Properties of successor and predecessor on binary integer numbers *)
+
+Theorem Zn_Sn : (x:Z) ~ x=(Zs x).
+Proof.
+Intros n;Cut ~ZERO=(POS xH);[
+  Unfold not ;Intros H1 H2;Apply H1;Apply (Zsimpl_plus_l n);Rewrite Zero_right;
+  Exact H2
+| Discriminate ].
+Qed.
+
+Theorem add_un_Zs : (x:positive) (POS (add_un x)) = (Zs (POS x)).
+Proof.
+Intro; Rewrite -> ZL12; Unfold Zs; Simpl; Trivial with arith.
+Qed.
+
+(** successor and predecessor are inverse functions *)
+
+Lemma Zs_pred : (n:Z) n=(Zs (Zpred n)).
+Proof.
+Intros n; Unfold Zs Zpred ;Rewrite <- Zplus_assoc; Simpl; Rewrite Zero_right;
+Trivial with arith.
+Qed. 
+
+Hints Immediate Zs_pred : zarith.
+ 
+Theorem Zpred_Sn : (x:Z) x=(Zpred (Zs x)).
+Proof.
+Intros m; Unfold Zpred Zs; Rewrite <- Zplus_assoc; Simpl; 
+Rewrite Zplus_sym; Auto with arith.
+Qed.
+
+Theorem Zeq_add_S : (x,y:Z) (Zs x)=(Zs y) -> x=y.
+Proof.
+Intros n m H.
+Change (Zplus (Zplus (NEG xH) (POS xH)) n)=
+       (Zplus (Zplus (NEG xH) (POS xH)) m);
+Do 2 Rewrite <- Zplus_assoc; Do 2 Rewrite (Zplus_sym (POS xH));
+Unfold Zs in H;Rewrite H; Trivial with arith.
+Qed.
+ 
+(** Misc properties, usually redundant or non natural *)
+
+Theorem Zeq_S : (x,y:Z) x=y -> (Zs x)=(Zs y).
+Proof.
+Intros n m H; Rewrite H; Reflexivity.
+Qed.
+
+Theorem Znot_eq_S : (x,y:Z) ~(x=y) -> ~((Zs x)=(Zs y)).
+Proof.
+Unfold not ;Intros n m H1 H2;Apply H1;Apply Zeq_add_S; Assumption.
+Qed.
+
+(**********************************************************************)
+(** Properties of subtraction on binary integer numbers *)
+
+Lemma Zminus_n_O : (x:Z) x=(Zminus x ZERO).
+Proof.
+Intro; Unfold Zminus; Simpl;Rewrite Zero_right; Trivial with arith.
+Qed.
+
+Lemma Zminus_n_n : (n:Z)(ZERO=(Zminus n n)).
+Proof.
+Intro; Unfold Zminus; Rewrite Zplus_inverse_r; Trivial with arith.
+Qed.
+
+Lemma Zplus_minus : (x,y,z:Z)(x=(Zplus y z))->(z=(Zminus x y)).
+Proof.
+Intros n m p H;Unfold Zminus;Apply (Zsimpl_plus_l m); 
+Rewrite (Zplus_sym m (Zplus n (Zopp m))); Rewrite <- Zplus_assoc;
+Rewrite Zplus_inverse_l; Rewrite Zero_right; Rewrite H; Trivial with arith.
+Qed.
+
+Lemma Zminus_plus : (x,y:Z)(Zminus (Zplus x y) x)=y.
+Proof.
+Intros n m;Unfold Zminus ;Rewrite -> (Zplus_sym n m);Rewrite <- Zplus_assoc;
+Rewrite -> Zplus_inverse_r; Apply Zero_right.
+Qed.
+
+Lemma Zle_plus_minus : (x,y:Z) (Zplus x (Zminus y x))=y.
+Proof.
+Unfold Zminus; Intros n m; Rewrite Zplus_permute; Rewrite Zplus_inverse_r;
+Apply Zero_right.
+Qed.
+
+Lemma Zminus_Sn_m : (x,y:Z)((Zs (Zminus x y))=(Zminus (Zs x) y)).
+Proof.
+Intros n m;Unfold Zminus Zs; Rewrite (Zplus_sym n (Zopp m));
+Rewrite <- Zplus_assoc;Apply Zplus_sym.
+Qed.
+
+Lemma Zminus_plus_simpl : 
+  (x,y,z:Z)((Zminus x y)=(Zminus (Zplus z x) (Zplus z y))).
+Proof.
+Intros n m p;Unfold Zminus; Rewrite Zopp_Zplus; Rewrite Zplus_assoc;
+Rewrite (Zplus_sym p); Rewrite <- (Zplus_assoc n p); Rewrite Zplus_inverse_r;
+Rewrite Zero_right; Trivial with arith.
+Qed.
+
+Lemma Zminus_Zplus_compatible :
+  (x,y,z:Z) (Zminus (Zplus x z) (Zplus y z)) = (Zminus x y).
+Intros x y n.
+Unfold Zminus.
+Rewrite -> Zopp_Zplus.
+Rewrite -> (Zplus_sym (Zopp y) (Zopp n)).
+Rewrite -> Zplus_assoc.
+Rewrite <- (Zplus_assoc x n (Zopp n)).
+Rewrite -> (Zplus_inverse_r n).
+Rewrite <- Zplus_n_O.
+Reflexivity.
+Qed.
+
+(** Misc redundant properties *)
+
+V7only [Set Implicit Arguments.].
+
+Lemma Zeq_Zminus : (x,y:Z)x=y -> (Zminus x y)=ZERO.
+Proof.
+Intros x y H; Rewrite H; Symmetry; Apply Zminus_n_n.
+Qed.
+
+Lemma Zminus_Zeq : (x,y:Z)(Zminus x y)=ZERO -> x=y.
+Proof.
+Intros x y H; Rewrite <- (Zle_plus_minus y x); Rewrite H; Apply Zero_right.
+Qed.
+
+V7only [Unset Implicit Arguments.].
+
+(**********************************************************************)
+(** Properties of multiplication on binary integer numbers *)
+
+(** One is neutral for multiplication *)
+
+Lemma Zmult_1_n : (x:Z)(Zmult (POS xH) x)=x.
+Proof.
+NewDestruct x; Reflexivity.
+Qed.
+V7only [Notation Zmult_one := Zmult_1_n.].
+
+Lemma Zmult_n_1 : (x:Z)(Zmult x (POS xH))=x.
+Proof.
+NewDestruct x; Simpl; Try Rewrite times_x_1; Reflexivity.
+Qed.
+
+(** Zero is absorbant for multiplication *)
+
 Theorem Zero_mult_left: (x:Z) (Zmult ZERO x) = ZERO.
 Proof.
-Induction x; Auto with arith.
+NewDestruct x; Reflexivity.
 Qed.
 
 Theorem Zero_mult_right: (x:Z) (Zmult x ZERO) = ZERO.
 Proof.
-Induction x; Auto with arith.
+NewDestruct x; Reflexivity.
 Qed.
 
 Hints Local Resolve Zero_mult_left Zero_mult_right.
 
-(* Multiplication and Opposite *)
-Theorem Zopp_Zmult:
-  (x,y:Z) (Zmult (Zopp x) y) = (Zopp (Zmult x y)).
+(** Commutativity of multiplication *)
+
+Theorem Zmult_sym : (x,y:Z) (Zmult x y) = (Zmult y x).
+Proof.
+NewDestruct x as [|p|p]; NewDestruct y as [|q|q]; Simpl; 
+  Try Rewrite (times_sym p q); Reflexivity.
+Qed.
+
+(** Associativity of multiplication *)
+
+Theorem Zmult_assoc_l :
+  (x,y,z:Z) (Zmult x (Zmult y z))= (Zmult (Zmult x y) z).
+Proof.
+NewDestruct x; NewDestruct y; NewDestruct z; Simpl; 
+  Try Rewrite times_assoc; Reflexivity.
+Qed.
+V7only [Notation Zmult_assoc := Zmult_assoc_l.].
+
+Lemma Zmult_assoc_r : (x,y,z:Z)((Zmult (Zmult x y) z) = (Zmult x (Zmult y z))).
+Proof.
+Intros n m p; Rewrite Zmult_assoc; Trivial with arith.
+Qed.
+
+(** Associativity mixed with commutativity *)
+
+Theorem Zmult_permute : (x,y,z:Z)(Zmult x (Zmult y z)) = (Zmult y (Zmult x z)).
+Proof.
+Intros; Rewrite -> (Zmult_assoc y x z); Rewrite -> (Zmult_sym y x).
+Apply Zmult_assoc.
+Qed.
+
+(** Z is integral *)
+
+Theorem Zmult_eq: (x,y:Z) ~(x=ZERO) -> (Zmult y x) = ZERO -> y = ZERO.
+Proof.
+Intros x y; NewDestruct x as [|p|p].
+  Intro H; Absurd ZERO=ZERO; Trivial.
+  Intros _ H; NewDestruct y as [|q|q]; Reflexivity Orelse Discriminate.
+  Intros _ H; NewDestruct y as [|q|q]; Reflexivity Orelse Discriminate.
+Qed.
+
+V7only [Set Implicit Arguments.].
+
+Lemma Zmult_zero : (x,y:Z)(Zmult x y)=ZERO -> x=ZERO \/ y=ZERO.
 Proof.
-Intros x y; Case x; Case y; Simpl; Auto with arith.
+NewDestruct x; NewDestruct y; Auto; Simpl; Intro H; Discriminate H.
 Qed.
 
-Theorem Zmult_Zopp_Zopp:
-  (x,y:Z) (Zmult (Zopp x) (Zopp y)) = (Zmult x y).
+V7only [Unset Implicit Arguments.].
+
+(** Multiplication and Opposite *)
+
+Theorem Zopp_Zmult: (x,y:Z) (Zmult (Zopp x) y) = (Zopp (Zmult x y)).
 Proof.
 NewDestruct x; NewDestruct y; Reflexivity.
 Qed.
 
+Theorem Zopp_Zmult_r : (x,y:Z)(Zopp (Zmult x y)) = (Zmult x (Zopp y)).
+Intros x y; Rewrite Zmult_sym; Rewrite <- Zopp_Zmult; Apply Zmult_sym.
+Qed.
+
+Theorem Zopp_Zmult_l : (x,y:Z)(Zopp (Zmult x y)) = (Zmult (Zopp x) y).
+Proof.
+Intros x y; Symmetry; Apply Zopp_Zmult.
+Qed.
+
+Theorem Zmult_Zopp_left :  (x,y:Z)(Zmult (Zopp x) y) = (Zmult x (Zopp y)).
+Intros; Rewrite Zopp_Zmult; Rewrite Zopp_Zmult_r; Trivial with arith.
+Qed.
+
+Theorem Zmult_Zopp_Zopp: (x,y:Z) (Zmult (Zopp x) (Zopp y)) = (Zmult x y).
+Proof.
+NewDestruct x; NewDestruct y; Reflexivity.
+Qed.
+
+Theorem Zopp_one : (x:Z)(Zopp x)=(Zmult x (NEG xH)).
+Induction x; Intros; Rewrite Zmult_sym; Auto with arith.
+Qed.
+
+(** Distributivity of multiplication over addition *)
+
 Theorem weak_Zmult_plus_distr_r:
   (x:positive)(y,z:Z)
    (Zmult (POS x) (Zplus y z)) = (Zplus (Zmult (POS x) y) (Zmult (POS x) z)).
@@ -1815,8 +2421,7 @@ Proof.
 Intros x y' z';Case y';Case z';Auto with arith;Intros y z;
   (Simpl; Rewrite times_add_distr; Trivial with arith)
 Orelse
-  (Simpl; (Elim (Dcompare (compare z y EGAL));[Idtac|Intros H;Elim H;
-   Clear  H]);Intros E0;Rewrite E0; [
+  (Simpl; ElimPcompare z y; Intros E0;Rewrite E0; [
     Rewrite (compare_convert_EGAL z y E0);
     Rewrite (convert_compare_EGAL (times x y)); Trivial with arith
   | Cut (compare (times x z) (times x y) EGAL)=INFERIEUR; [
@@ -1844,19 +2449,113 @@ Intros x y z; Case x; [
   Apply weak_Zmult_plus_distr_r ].
 Qed.
 
+Lemma Zmult_plus_distr_l : 
+  (n,m,p:Z)((Zmult (Zplus n m) p)=(Zplus (Zmult n p) (Zmult m p))).
+Proof.
+Intros n m p;Rewrite Zmult_sym;Rewrite Zmult_plus_distr_r; 
+Do 2 Rewrite -> (Zmult_sym p); Trivial with arith.
+Qed.
+
+(** Distributivity of multiplication over subtraction *)
+
+Lemma Zmult_Zminus_distr_l :
+  (x,y,z:Z)((Zmult (Zminus x y) z)=(Zminus (Zmult x z) (Zmult y z))).
+Proof.
+Intros; Unfold Zminus.
+Rewrite <- Zopp_Zmult.
+Apply Zmult_plus_distr_l.
+Qed.
+
+V7only [Notation Zmult_minus_distr := Zmult_Zminus_distr_l.].
+ 
+Lemma  Zmult_Zminus_distr_r :
+  (x,y,z:Z)(Zmult z (Zminus x y)) = (Zminus (Zmult z x) (Zmult z y)).
+Proof.
+Intros; Rewrite (Zmult_sym z (Zminus x y)).
+Rewrite (Zmult_sym  z x).
+Rewrite (Zmult_sym z y).
+Apply Zmult_Zminus_distr_l.
+Qed.
+
+(** Simplification of multiplication for non-zero integers *)
+
+Lemma Zmult_reg_left : (x,y,z:Z) z<>ZERO -> (Zmult z x)=(Zmult z y) -> x=y.
+Proof.
+Intros.
+Generalize (Zeq_Zminus H0).
+Intro.
+Apply Zminus_Zeq.
+Rewrite <- Zmult_Zminus_distr_r in H1.
+Clear H0; NewDestruct (Zmult_zero H1).
+Contradiction.
+Trivial.
+Qed.
+
+Lemma Zmult_reg_right : (x,y,z:Z) z<>ZERO -> (Zmult x z)=(Zmult y z) -> x=y.
+Proof.
+Intros x y z Hz.
+Rewrite (Zmult_sym x z).
+Rewrite (Zmult_sym y z).
+Intro; Apply Zmult_reg_left with z; Assumption.
+Qed.
+    
+(** Addition and multiplication by 2 *)
+
+Theorem Zplus_Zmult_2 : (x:Z) (Zplus x x) = (Zmult x (POS (xO xH))).
+Proof.
+Intros x; Pattern 1 2 x ; Rewrite <- (Zmult_n_1 x);
+Rewrite <- Zmult_plus_distr_r; Reflexivity.
+Qed.
+
+(** Multiplication and successor *)
+
+Lemma Zmult_n_Sm : (n,m:Z) (Zplus (Zmult n m) n)=(Zmult n (Zs m)).
+Proof.
+Intros n m;Unfold Zs; Rewrite Zmult_plus_distr_r;
+Rewrite (Zmult_sym n (POS xH));Rewrite Zmult_one; Trivial with arith.
+Qed.
+
+Lemma Zmult_Sm_n : (n,m:Z) (Zplus (Zmult n m) m)=(Zmult (Zs n) m).
+Proof.
+Intros n m; Unfold Zs; Rewrite Zmult_plus_distr_l; Rewrite Zmult_1_n;
+Trivial with arith.
+Qed.
+
+(** Misc redundant properties *)
+
+Lemma Zmult_n_O : (n:Z) ZERO=(Zmult n ZERO).
+Proof.
+Intro;Rewrite Zmult_sym;Simpl; Trivial with arith.
+Qed.
+
+Theorem Z_eq_mult:
+  (x,y:Z)  y = ZERO -> (Zmult y x) = ZERO.
+Intros x y H; Rewrite H; Auto with arith.
+Qed.
+
+(**********************************************************************)
+(* Comparison on integers *)
+
+Lemma Zcompare_x_x : (x:Z) (Zcompare x x) = EGAL.
+Proof.
+NewDestruct x as [|p|p]; Simpl; [ Reflexivity | Apply convert_compare_EGAL
+  | Rewrite convert_compare_EGAL; Reflexivity ].
+Qed.
+
+Theorem Zcompare_EGAL_eq : (x,y:Z) (Zcompare x y) = EGAL -> x = y.
+Proof.
+NewDestruct x as [|x'|x'];NewDestruct y as [|y'|y'];Simpl;Intro H; Reflexivity Orelse Try Discriminate H; [
+    Rewrite (compare_convert_EGAL x' y' H); Reflexivity
+  | Rewrite (compare_convert_EGAL x' y'); [
+      Reflexivity
+    | NewDestruct (compare x' y' EGAL);
+      Reflexivity Orelse Discriminate]].
+Qed.
+
 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
-    | Generalize H; Case (compare y' x' EGAL);
-      Trivial with arith Orelse (Intros C;Discriminate C)]]
-| Intros E;Rewrite E; Case y; [
-    Trivial with arith
-  | Simpl;Exact convert_compare_EGAL
-  | Simpl; Intros p;Rewrite convert_compare_EGAL;Auto with arith ]].
+Intros x y;Split; Intro E; [ Apply Zcompare_EGAL_eq; Assumption
+  | Rewrite E; Apply Zcompare_x_x ].
 Qed.
 
 Theorem Zcompare_ANTISYM : 
@@ -1877,6 +2576,26 @@ Intros x y;Split; [
        Trivial with arith Orelse (Intros H2;Discriminate H2)]))].
 Qed.
 
+(** Transitivity of comparison *)
+
+Theorem Zcompare_trans_SUPERIEUR : 
+  (x,y,z:Z) (Zcompare x y) = SUPERIEUR ->  
+            (Zcompare y z) = SUPERIEUR ->
+            (Zcompare x z) = SUPERIEUR.
+Proof.
+Intros x y z;Case x;Case y;Case z; Simpl;
+Try (Intros; Discriminate H Orelse Discriminate H0);
+Auto with arith; [
+  Intros p q r H H0;Apply convert_compare_SUPERIEUR; Unfold gt;
+  Apply lt_trans with m:=(convert q);
+  Apply compare_convert_INFERIEUR;Apply ZC1;Assumption
+| Intros p q r; Do 3 Rewrite <- ZC4; Intros H H0;
+  Apply convert_compare_SUPERIEUR;Unfold gt;Apply lt_trans with m:=(convert q);
+  Apply compare_convert_INFERIEUR;Apply ZC1;Assumption ].
+Qed.
+
+(** Comparison and opposite *)
+
 Theorem Zcompare_Zopp :
   (x,y:Z) (Zcompare x y) = (Zcompare (Zopp y) (Zopp x)).
 Proof.
@@ -1886,6 +2605,28 @@ Qed.
 
 Hints Local Resolve convert_compare_EGAL.
 
+(** Comparison first-order specification *)
+
+Lemma SUPERIEUR_POS :
+  (x,y:Z) (Zcompare x y) = SUPERIEUR ->
+  (EX h:positive |(Zplus x (Zopp y)) = (POS h)).
+Proof.
+Intros x y;Case x;Case y; [
+  Simpl; Intros H; Discriminate H
+| Simpl; Intros p H; Discriminate H
+| Intros p H; Exists p; Simpl; Auto with arith
+| Intros p H; Exists p; Simpl; Auto with arith
+| Intros q p H; Exists (true_sub p q); Unfold Zplus Zopp;
+  Unfold Zcompare in H; Rewrite H; Trivial with arith
+| Intros q p H; Exists (add p q); Simpl; Trivial with arith
+| Simpl; Intros p H; Discriminate H
+| Simpl; Intros q p H; Discriminate H
+| Unfold Zcompare; Intros q p; Rewrite <- ZC4; Intros H; Exists (true_sub q p);
+  Simpl; Rewrite (ZC1 q p H); Trivial with arith].
+Qed.
+
+(** Comparison and addition *)
+
 Theorem weaken_Zcompare_Zplus_compatible : 
   ((x,y:Z) (z:positive) 
     (Zcompare (Zplus (POS z) x) (Zplus (POS z) y)) = (Zcompare x y)) ->
@@ -1906,15 +2647,14 @@ Theorem weak_Zcompare_Zplus_compatible :
 Proof.
 Intros x y z;Case x;Case y;Simpl;Auto with arith; [
   Intros p;Apply convert_compare_INFERIEUR; Apply ZL17
-| Intros p;(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H;
-  Clear H]);Intros E;Rewrite E;Auto with arith;
+| Intros p;ElimPcompare z p;Intros E;Rewrite E;Auto with arith;
   Apply convert_compare_SUPERIEUR; Rewrite true_sub_convert; [ Unfold gt ;
   Apply ZL16 | Assumption ]
-| Intros p;(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H;
-  Clear H]);Intros E;Auto with arith; Apply convert_compare_SUPERIEUR;
+| Intros p;ElimPcompare z p;
+  Intros E;Auto with arith; Apply convert_compare_SUPERIEUR;
   Unfold gt;Apply ZL17
 | Intros p q;
-  (Elim (Dcompare (compare q p EGAL));[Idtac|Intros H;Elim H;Clear  H]);
+  ElimPcompare q p;
   Intros E;Rewrite E;[
     Rewrite (compare_convert_EGAL q p E); Apply convert_compare_EGAL
   | Apply convert_compare_INFERIEUR;Do 2 Rewrite convert_add;Apply lt_reg_l;
@@ -1922,27 +2662,22 @@ Intros x y z;Case x;Case y;Simpl;Auto with arith; [
   | Apply convert_compare_SUPERIEUR;Unfold gt ;Do 2 Rewrite convert_add;
     Apply lt_reg_l;Exact (compare_convert_SUPERIEUR q p E) ]
 | Intros p q; 
-  (Elim (Dcompare (compare z p EGAL));[Idtac|Intros H;Elim H;Clear  H]);
+  ElimPcompare z p;
   Intros E;Rewrite E;Auto with arith;
   Apply convert_compare_SUPERIEUR; Rewrite true_sub_convert; [
     Unfold gt; Apply lt_trans with m:=(convert z); [Apply ZL16 | Apply ZL17]
   | Assumption ]
-| Intros p;(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H;
-  Clear H]);Intros E;Rewrite E;Auto with arith; Simpl;
+| Intros p;ElimPcompare z p;Intros E;Rewrite E;Auto with arith; Simpl;
   Apply convert_compare_INFERIEUR;Rewrite true_sub_convert;[Apply ZL16|
   Assumption]
 | Intros p q;
-  (Elim (Dcompare (compare z q EGAL));[Idtac|Intros H;Elim H;Clear  H]);
+  ElimPcompare z q;
   Intros E;Rewrite E;Auto with arith; Simpl;Apply convert_compare_INFERIEUR;
   Rewrite true_sub_convert;[
     Apply lt_trans with m:=(convert z) ;[Apply ZL16|Apply ZL17]
   | Assumption]
-| Intros p q;
-  (Elim (Dcompare (compare z q EGAL));[Idtac|Intros H;Elim H;Clear  H]);
-  Intros E0;Rewrite E0;
-  (Elim (Dcompare (compare z p EGAL));[Idtac|Intros H;Elim H;Clear  H]);
-  Intros E1;Rewrite E1;
-  (Elim (Dcompare (compare q p EGAL));[Idtac|Intros H;Elim H;Clear  H]);
+| Intros p q; ElimPcompare z q; Intros E0;Rewrite E0;
+  ElimPcompare z p; Intros E1;Rewrite E1; ElimPcompare q p;
   Intros E2;Rewrite E2;Auto with arith; [
     Absurd (compare q p EGAL)=INFERIEUR; [
       Rewrite <- (compare_convert_EGAL z q E0);
@@ -2069,44 +2804,150 @@ Proof.
 Exact (weaken_Zcompare_Zplus_compatible weak_Zcompare_Zplus_compatible).
 Qed.
 
-Theorem Zcompare_trans_SUPERIEUR : 
-  (x,y,z:Z) (Zcompare x y) = SUPERIEUR ->  
-            (Zcompare y z) = SUPERIEUR ->
-            (Zcompare x z) = SUPERIEUR.
-Proof.
-Intros x y z;Case x;Case y;Case z; Simpl;
-Try (Intros; Discriminate H Orelse Discriminate H0);
-Auto with arith; [
-  Intros p q r H H0;Apply convert_compare_SUPERIEUR; Unfold gt;
-  Apply lt_trans with m:=(convert q);
-  Apply compare_convert_INFERIEUR;Apply ZC1;Assumption
-| Intros p q r; Do 3 Rewrite <- ZC4; Intros H H0;
-  Apply convert_compare_SUPERIEUR;Unfold gt;Apply lt_trans with m:=(convert q);
-  Apply compare_convert_INFERIEUR;Apply ZC1;Assumption ].
+Theorem Zcompare_Zplus_compatible2 :
+  (r:relation)(x,y,z,t:Z)
+    (Zcompare x y) = r -> (Zcompare z t) = r ->
+    (Zcompare (Zplus x z) (Zplus y t)) = r.
+Proof.
+Intros r x y z t; Case r; [
+  Intros H1 H2; Elim (Zcompare_EGAL x y); Elim (Zcompare_EGAL z t);
+  Intros H3 H4 H5 H6; Rewrite H3; [ 
+    Rewrite H5; [ Elim (Zcompare_EGAL (Zplus y t) (Zplus y t)); Auto with arith | Auto with arith ]
+  | Auto with arith ]
+| Intros H1 H2; Elim (Zcompare_ANTISYM (Zplus y t) (Zplus x z));
+  Intros H3 H4; Apply H3;
+  Apply Zcompare_trans_SUPERIEUR with y:=(Zplus y z) ; [
+    Rewrite Zcompare_Zplus_compatible;
+    Elim (Zcompare_ANTISYM t z); Auto with arith
+  | Do 2 Rewrite <- (Zplus_sym z); 
+    Rewrite Zcompare_Zplus_compatible;
+    Elim (Zcompare_ANTISYM y x); Auto with arith]
+| Intros H1 H2;
+  Apply Zcompare_trans_SUPERIEUR with y:=(Zplus x t) ; [
+    Rewrite Zcompare_Zplus_compatible; Assumption
+  | Do 2 Rewrite <- (Zplus_sym t);
+    Rewrite Zcompare_Zplus_compatible; Assumption]].
+Qed.
+
+Lemma Zcompare_Zs_SUPERIEUR : (x:Z)(Zcompare (Zs x) x)=SUPERIEUR.
+Proof.
+Intro x; Unfold Zs; Pattern 2 x; Rewrite <- (Zero_right x); 
+Rewrite Zcompare_Zplus_compatible;Reflexivity.
+Qed.
+
+Theorem Zcompare_et_un: 
+  (x,y:Z) (Zcompare x y)=SUPERIEUR <-> 
+    ~(Zcompare x (Zplus y (POS xH)))=INFERIEUR.
+Proof.
+Intros x y; Split; [
+  Intro H; (ElimCompare 'x '(Zplus y (POS xH)));[
+    Intro H1; Rewrite H1; Discriminate
+  | Intros H1; Elim SUPERIEUR_POS with 1:=H; Intros h H2; 
+    Absurd (gt (convert h) O) /\ (lt (convert h) (S O)); [
+      Unfold not ;Intros H3;Elim H3;Intros H4 H5; Absurd (gt (convert h) O); [
+        Unfold gt ;Apply le_not_lt; Apply le_S_n; Exact H5
+      | Assumption]
+    | Split; [
+        Elim (ZL4 h); Intros i H3;Rewrite H3; Apply gt_Sn_O
+      | Change (lt (convert h) (convert xH)); 
+        Apply compare_convert_INFERIEUR;
+        Change (Zcompare (POS h) (POS xH))=INFERIEUR;
+        Rewrite <- H2; Rewrite <- [m,n:Z](Zcompare_Zplus_compatible m n y);
+        Rewrite (Zplus_sym x);Rewrite Zplus_assoc; Rewrite Zplus_inverse_r;
+        Simpl; Exact H1 ]]
+  | Intros H1;Rewrite -> H1;Discriminate ]
+| Intros H; (ElimCompare 'x '(Zplus y (POS xH))); [
+    Intros H1;Elim (Zcompare_EGAL x (Zplus y (POS xH))); Intros H2 H3;
+    Rewrite  (H2 H1); Exact (Zcompare_Zs_SUPERIEUR y)
+  | Intros H1;Absurd (Zcompare x (Zplus y (POS xH)))=INFERIEUR;Assumption
+  | Intros H1; Apply Zcompare_trans_SUPERIEUR with y:=(Zs y); 
+      [ Exact H1 | Exact (Zcompare_Zs_SUPERIEUR y)]]].
 Qed.
 
-Lemma SUPERIEUR_POS :
-  (x,y:Z) (Zcompare x y) = SUPERIEUR ->
-  (EX h:positive |(Zplus x (Zopp y)) = (POS h)).
+(** Successor and comparison *)
+
+Theorem Zcompare_n_S : (x,y:Z)(Zcompare (Zs x) (Zs y)) = (Zcompare x y).
 Proof.
-Intros x y;Case x;Case y; [
-  Simpl; Intros H; Discriminate H
-| Simpl; Intros p H; Discriminate H
-| Intros p H; Exists p; Simpl; Auto with arith
-| Intros p H; Exists p; Simpl; Auto with arith
-| Intros q p H; Exists (true_sub p q); Unfold Zplus Zopp;
-  Unfold Zcompare in H; Rewrite H; Trivial with arith
-| Intros q p H; Exists (add p q); Simpl; Trivial with arith
-| Simpl; Intros p H; Discriminate H
-| Simpl; Intros q p H; Discriminate H
-| Unfold Zcompare; Intros q p; Rewrite <- ZC4; Intros H; Exists (true_sub q p);
-  Simpl; Rewrite (ZC1 q p H); Trivial with arith].
+Intros n m;Unfold Zs ;Do 2 Rewrite -> [t:Z](Zplus_sym t (POS xH));
+Rewrite -> Zcompare_Zplus_compatible;Auto with arith.
 Qed.
+ 
+(** Multiplication and comparison *)
 
-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).
-].
+Theorem Zcompare_Zmult_compatible : 
+   (x:positive)(y,z:Z)
+      (Zcompare (Zmult (POS x) y) (Zmult (POS x) z)) = (Zcompare y z).
+
+Induction x; [
+  Intros p H y z;
+  Cut (POS (xI p))=(Zplus (Zplus (POS p) (POS p)) (POS xH)); [
+    Intros E; Rewrite E; Do 4 Rewrite Zmult_plus_distr_l; 
+    Do 2 Rewrite Zmult_one;
+    Apply Zcompare_Zplus_compatible2; [
+      Apply Zcompare_Zplus_compatible2; Apply H
+    | Trivial with arith]
+  | Simpl; Rewrite (add_x_x p); Trivial with arith]
+| Intros p H y z; Cut (POS (xO p))=(Zplus (POS p) (POS p)); [
+    Intros E; Rewrite E; Do 2 Rewrite Zmult_plus_distr_l;
+      Apply Zcompare_Zplus_compatible2; Apply H
+    | Simpl; Rewrite (add_x_x p); Trivial with arith]
+  | Intros y z; Do 2 Rewrite Zmult_one; Trivial with arith].
+Qed.
+
+(**********************************************************************)
+(** Relating binary positive numbers and binary integers *)
+
+Lemma POS_xI : (p:positive) (POS (xI p))=(Zplus (Zmult (POS (xO xH)) (POS p)) (POS xH)).
+Intro; Apply refl_equal.
+Qed.
+Lemma POS_xO : (p:positive) (POS (xO p))=(Zmult (POS (xO xH)) (POS p)).
+Intro; Apply refl_equal.
+Qed.
+Lemma NEG_xI : (p:positive) (NEG (xI p))=(Zminus (Zmult (POS (xO xH)) (NEG p)) (POS xH)).
+Intro; Apply refl_equal.
+Qed.
+Lemma NEG_xO : (p:positive) (NEG (xO p))=(Zmult (POS (xO xH)) (NEG p)).
+Reflexivity.
+Qed.
+
+Lemma POS_add : (p,p':positive)(POS (add p p'))=(Zplus (POS p) (POS p')).
+NewDestruct p; NewDestruct p'; Reflexivity.
+Qed.
+
+Lemma NEG_add : (p,p':positive)(NEG (add p p'))=(Zplus (NEG p) (NEG p')).
+NewDestruct p; NewDestruct p'; Reflexivity.
+Qed.
+
+(**********************************************************************)
+(** Order relations *)
+
+Definition Zlt := [x,y:Z](Zcompare x y) = INFERIEUR.
+Definition Zgt := [x,y:Z](Zcompare x y) = SUPERIEUR.
+Definition Zle := [x,y:Z]~(Zcompare x y) = SUPERIEUR.
+Definition Zge := [x,y:Z]~(Zcompare x y) = INFERIEUR.
+
+V8Infix "<=" Zle : Z_scope.
+V8Infix "<"  Zlt : Z_scope.
+V8Infix ">=" Zge : Z_scope.
+V8Infix ">"  Zgt : Z_scope.
+
+V8Notation "x <= y <= z" := (Zle x y)/\(Zle y z) :Z_scope.
+V8Notation "x <= y < z"  := (Zle x y)/\(Zlt y z) :Z_scope.
+V8Notation  "x < y < z"  := (Zlt x y)/\(Zlt y z) :Z_scope.
+V8Notation  "x < y <= z" := (Zlt x y)/\(Zle y z) :Z_scope.
+
+(**********************************************************************)
+(** From [nat] to [Z] *)
+
+Definition inject_nat := 
+  [x:nat]Cases x of
+           O => ZERO
+         | (S y) => (POS (anti_convert y))
+         end.
+
+Definition entier_of_Z :=
+  [z:Z]Cases z of ZERO => Nul | (POS p) => (Pos p) | (NEG p) => (Pos p) end.
+
+Definition Z_of_entier :=
+  [x:entier]Cases x of Nul => ZERO | (Pos p) => (POS p) end.
+ 
diff --git a/theories/ZArith/zarith_aux.v b/theories/ZArith/zarith_aux.v
index 3da7f4eb8a..01c3467814 100644
--- a/theories/ZArith/zarith_aux.v
+++ b/theories/ZArith/zarith_aux.v
@@ -7,264 +7,276 @@
 (***********************************************************************)
 (*i $Id$ i*)
 
-(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
 
+Require fast_integer.
 Require Arith.
-Require Export fast_integer.
 
 V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Tactic Definition ElimCompare com1 com2:=
-  Elim (Dcompare (Zcompare com1 com2)); [
-         Idtac 
-       | Intro hidden_auxiliary; Elim hidden_auxiliary; 
-         Clear hidden_auxiliary ] .
-
-(** Order relations *)
-Definition Zlt := [x,y:Z](Zcompare x y) = INFERIEUR.
-Definition Zgt := [x,y:Z](Zcompare x y) = SUPERIEUR.
-Definition Zle := [x,y:Z]~(Zcompare x y) = SUPERIEUR.
-Definition Zge := [x,y:Z]~(Zcompare x y) = INFERIEUR.
-
-V8Infix "<=" Zle : Z_scope.
-V8Infix "<"  Zlt : Z_scope.
-V8Infix ">=" Zge : Z_scope.
-V8Infix ">"  Zgt : Z_scope.
-
-V8Notation "x <= y <= z" := (Zle x y)/\(Zle y z) :Z_scope.
-V8Notation "x <= y < z"  := (Zle x y)/\(Zlt y z) :Z_scope.
-V8Notation  "x < y < z"  := (Zlt x y)/\(Zlt y z) :Z_scope.
-V8Notation  "x < y <= z" := (Zlt x y)/\(Zle y z) :Z_scope.
-
-(** Sign function *)
-Definition Zsgn [z:Z] : Z :=
-  Cases z of 
-     ZERO   => ZERO
-  | (POS p) => (POS xH)
-  | (NEG p) => (NEG xH)
-  end.
+Open Local Scope Z_scope.
 
-(** Absolu function *)
-Definition absolu [x:Z] : nat :=
-  Cases x of
-     ZERO   => O
-  | (POS p) => (convert p)
-  | (NEG p) => (convert p)
-  end.
+(**********************************************************************)
+(** Properties of the order relations on binary integers *)
 
-Definition Zabs [z:Z] : Z :=
-  Cases z of 
-     ZERO   => ZERO
-  | (POS p) => (POS p)
-  | (NEG p) => (POS p)
-  end.
+(** Trichotomy *)
 
-(** Properties of absolu function *)
+Theorem Ztrichotomy_inf : (m,n:Z) {Zlt m n} + {m=n} + {Zgt m n}.
+Proof.
+Unfold Zgt Zlt; Intros m n; Assert H:=(refl_equal ? (Zcompare m n)).
+  LetTac x := (Zcompare m n) in 2 H Goal.
+  NewDestruct x; 
+    [Left; Right;Rewrite Zcompare_EGAL_eq with 1:=H 
+    | Left; Left
+    | Right ]; Reflexivity.
+Qed.
 
-Lemma Zabs_eq : (x:Z) (Zle ZERO x) -> (Zabs x)=x.
-NewDestruct x; Auto with arith.
-Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
+Theorem Ztrichotomy : (m,n:Z) (Zlt m n) \/ m=n \/ (Zgt m n).
+Proof.
+  Intros m n; NewDestruct (Ztrichotomy_inf m n) as [[Hlt|Heq]|Hgt];
+    [Left | Right; Left |Right; Right]; Assumption.
 Qed.
 
-Lemma Zabs_non_eq : (x:Z) (Zle x ZERO) -> (Zabs x)=(Zopp x).
+(** Relating strict and large orders *)
+
+Lemma Zgt_lt : (m,n:Z) (Zgt m n) -> (Zlt n m).
 Proof.
-NewDestruct x; Auto with arith.
-Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
+Unfold Zgt Zlt ;Intros m n H; Elim (Zcompare_ANTISYM m n); Auto with arith.
 Qed.
 
-Definition Zabs_dec : (x:Z){x=(Zabs x)}+{x=(Zopp (Zabs x))}.
+Lemma Zlt_gt : (m,n:Z) (Zlt m n) -> (Zgt n m).
 Proof.
-NewDestruct x;Auto with arith.
-Defined.
+Unfold Zgt Zlt ;Intros m n H; Elim (Zcompare_ANTISYM n m); Auto with arith.
+Qed.
 
-Lemma Zabs_pos : (x:Z)(Zle ZERO (Zabs x)).
-NewDestruct x;Auto with arith; Compute; Intros H;Inversion H.
+Lemma Zge_le : (m,n:Z) (Zge m n) -> (Zle n m).
+Proof.
+Intros m n; Change ~(Zlt m n)-> ~(Zgt n m);
+Unfold not; Intros H1 H2; Apply H1; Apply Zgt_lt; Assumption.
 Qed.
 
-Lemma Zsgn_Zabs: (x:Z)(Zmult x (Zsgn x))=(Zabs x).
+Lemma Zle_ge : (m,n:Z) (Zle m n) -> (Zge n m).
 Proof.
-NewDestruct x; Rewrite Zmult_sym; Auto with arith.
+Intros m n; Change ~(Zgt m n)-> ~(Zlt n m);
+Unfold not; Intros H1 H2; Apply H1; Apply Zlt_gt; Assumption.
 Qed.
 
-Lemma Zabs_Zsgn: (x:Z)(Zmult (Zabs x) (Zsgn x))=x.
+Lemma Zle_not_gt     : (n,m:Z)(Zle n m) -> ~(Zgt n m).
 Proof.
-NewDestruct x; Rewrite Zmult_sym; Auto with arith.
+Trivial.
 Qed.
 
-(** From [nat] to [Z] *)
-Definition inject_nat := 
-  [x:nat]Cases x of
-           O => ZERO
-         | (S y) => (POS (anti_convert y))
-         end.
+Lemma Znot_gt_le     : (n,m:Z)~(Zgt n m) -> (Zle n m).
+Proof.
+Trivial.
+Qed.
 
-(** Successor and Predecessor functions on [Z] *)
-Definition Zs := [x:Z](Zplus x (POS xH)).
-Definition Zpred := [x:Z](Zplus x (NEG xH)).
+Lemma Zgt_not_le     : (n,m:Z)(Zgt n m) -> ~(Zle n m).
+Proof.
+Intros n m H1 H2; Apply H2; Assumption.
+Qed.
 
-(* Properties of the order relation *)
-Theorem Zgt_Sn_n : (n:Z)(Zgt (Zs n) n).
+Lemma Zle_not_lt : (n,m:Z)(Zle n m) -> ~(Zlt m n).
+Proof.
+Intros n m H1 H2.
+Assert H3:=(Zlt_gt ? ? H2).
+Apply Zle_not_gt with n m; Assumption.
+Qed.
 
-Intros n; Unfold Zgt Zs; Pattern 2 n; Rewrite <- (Zero_right n); 
-Rewrite Zcompare_Zplus_compatible;Auto with arith.
+Lemma Zlt_not_le : (n,m:Z)(Zlt n m) -> ~(Zle m n).
+Proof.
+Intros n m H1 H2.
+Apply Zle_not_lt with m n; Assumption.
 Qed.
 
-(** Properties of the order *)
-Theorem Zle_gt_trans : (n,m,p:Z)(Zle m n)->(Zgt m p)->(Zgt n p).
+(** Reflexivity *)
+
+Lemma Zle_n : (n:Z) (Zle n n).
+Proof.
+Intros n; Unfold Zle; Rewrite (Zcompare_x_x n); Discriminate.
+Qed. 
 
-Unfold Zle Zgt; Intros n m p H1 H2; (ElimCompare 'm 'n); [
-  Intro E; Elim (Zcompare_EGAL m n); Intros H3 H4;Rewrite <- (H3 E); Assumption
-| Intro H3; Apply Zcompare_trans_SUPERIEUR with y:=m;[
-    Elim (Zcompare_ANTISYM n m); Intros H4 H5;Apply H5; Assumption
-  | Assumption ]
-| Intro H3; Absurd (Zcompare m n)=SUPERIEUR;Assumption ].
+(** Antisymmetry *)
+
+Lemma Zle_antisym : (n,m:Z)(Zle n m)->(Zle m n)->n=m.
+Proof.
+Intros n m H1 H2; NewDestruct (Ztrichotomy n m) as [Hlt|[Heq|Hgt]]. 
+  Absurd (Zgt m n); [ Apply Zle_not_gt | Apply Zlt_gt]; Assumption.
+  Assumption.
+  Absurd (Zgt n m); [ Apply Zle_not_gt | Idtac]; Assumption.
 Qed.
 
-Theorem Zgt_le_trans : (n,m,p:Z)(Zgt n m)->(Zle p m)->(Zgt n p).
+(** Asymmetry *)
+
+Lemma Zgt_not_sym    : (n,m:Z)(Zgt n m) -> ~(Zgt m n).
+Proof.
+Unfold Zgt ;Intros n m H; Elim (Zcompare_ANTISYM n m); Intros H1 H2;
+Rewrite -> H1; [ Discriminate | Assumption ].
+Qed.
 
-Unfold Zle Zgt ;Intros n m p H1 H2; (ElimCompare 'p 'm); [
-  Intros E;Elim (Zcompare_EGAL p m);Intros H3 H4; Rewrite (H3 E); Assumption
-| Intro H3; Apply Zcompare_trans_SUPERIEUR with y:=m; [
-    Assumption
-  | Elim (Zcompare_ANTISYM m p); Auto with arith ]
-| Intro H3; Absurd (Zcompare p m)=SUPERIEUR;Assumption ].
+Lemma Zlt_not_sym : (n,m:Z)(Zlt n m) -> ~(Zlt m n).
+Proof.
+Intros n m H H1;
+Assert H2:(Zgt m n). Apply Zlt_gt; Assumption.
+Assert H3: (Zgt n m). Apply Zlt_gt; Assumption.
+Apply Zgt_not_sym with m n; Assumption.
 Qed.
 
-Theorem Zle_S_gt : (n,m:Z) (Zle (Zs n) m) -> (Zgt m n).
+(** Irreflexivity *)
 
-Intros n m H;Apply Zle_gt_trans with m:=(Zs n);[ Assumption | Apply Zgt_Sn_n ].
+Lemma Zgt_antirefl   : (n:Z)~(Zgt n n).
+Proof.
+Intros n H; Apply (Zgt_not_sym n n H H).
 Qed.
 
-Theorem Zcompare_n_S : (n,m:Z)(Zcompare (Zs n) (Zs m)) = (Zcompare n m).
-Intros n m;Unfold Zs ;Do 2 Rewrite -> [t:Z](Zplus_sym t (POS xH));
-Rewrite -> Zcompare_Zplus_compatible;Auto with arith.
+Lemma Zlt_n_n : (n:Z)~(Zlt n n).
+Proof.
+Intros n H; Apply (Zlt_not_sym n n H H).
 Qed.
- 
-Theorem Zgt_n_S : (n,m:Z)(Zgt m n) -> (Zgt (Zs m) (Zs n)).
 
-Unfold Zgt; Intros n m H; Rewrite Zcompare_n_S; Auto with arith.
+(** Large = strict or equal *)
+
+Lemma Zle_lt_or_eq : (n,m:Z)(Zle n m)->((Zlt n m) \/ n=m).
+Proof.
+Intros n m H; NewDestruct (Ztrichotomy n m) as [Hlt|[Heq|Hgt]]; [
+  Left; Assumption
+| Right; Assumption
+| Absurd (Zgt n m); [Apply Zle_not_gt|Idtac]; Assumption ].
 Qed.
 
-Lemma Zle_not_gt     : (n,m:Z)(Zle n m) -> ~(Zgt n m).
+Lemma Zlt_le_weak : (n,m:Z)(Zlt n m)->(Zle n m).
+Proof.
+Intros n m Hlt; Apply Znot_gt_le; Apply Zgt_not_sym; Apply Zlt_gt; Assumption.
+Qed.
+
+(** Dichotomy *)
 
-Unfold Zle Zgt; Auto with arith.
+Lemma Zle_or_lt : (n,m:Z)(Zle n m)\/(Zlt m n).
+Proof.
+Intros n m; NewDestruct (Ztrichotomy n m) as [Hlt|[Heq|Hgt]]; [
+  Left; Apply Znot_gt_le; Intro Hgt; Assert Hgt':=(Zlt_gt ? ? Hlt);
+     Apply Zgt_not_sym with m n; Assumption
+| Left; Rewrite Heq; Apply Zle_n
+| Right; Apply Zgt_lt; Assumption ].
 Qed.
 
-Lemma Zgt_antirefl   : (n:Z)~(Zgt n n).
+(** Transitivity of strict orders *)
 
-Unfold Zgt ;Intros n; Elim (Zcompare_EGAL n n); Intros H1 H2;
-Rewrite H2; [ Discriminate | Trivial with arith ].
+Lemma Zgt_trans      : (n,m,p:Z)(Zgt n m)->(Zgt m p)->(Zgt n p).
+Proof.
+Exact Zcompare_trans_SUPERIEUR.
 Qed.
 
-Lemma Zgt_not_sym    : (n,m:Z)(Zgt n m) -> ~(Zgt m n).
+Lemma Zlt_trans : (n,m,p:Z)(Zlt n m)->(Zlt m p)->(Zlt n p).
+Proof.
+Intros n m p H1 H2; Apply Zgt_lt; Apply Zgt_trans with m:= m; 
+Apply Zlt_gt; Assumption.
+Qed.
 
-Unfold Zgt ;Intros n m H; Elim (Zcompare_ANTISYM n m); Intros H1 H2;
-Rewrite -> H1; [ Discriminate | Assumption ].
+(** Mixed transitivity *)
+
+Lemma Zle_gt_trans : (n,m,p:Z)(Zle m n)->(Zgt m p)->(Zgt n p).
+Proof.
+Intros n m p H1 H2; NewDestruct (Zle_lt_or_eq m n H1) as [Hlt|Heq]; [
+  Apply Zgt_trans with m; [Apply Zlt_gt; Assumption | Assumption ]
+| Rewrite <- Heq; Assumption ].
 Qed.
 
-Lemma Zgt_not_le     : (n,m:Z)(Zgt n m) -> ~(Zle n m).
+Lemma Zgt_le_trans : (n,m,p:Z)(Zgt n m)->(Zle p m)->(Zgt n p).
+Proof.
+Intros n m p H1 H2; NewDestruct (Zle_lt_or_eq p m H2) as [Hlt|Heq]; [
+  Apply Zgt_trans with m; [Assumption|Apply Zlt_gt; Assumption]
+| Rewrite Heq; Assumption ].
+Qed.
 
-Unfold Zgt Zle not; Auto with arith.
+Lemma Zlt_le_trans : (n,m,p:Z)(Zlt n m)->(Zle m p)->(Zlt n p).
+Intros n m p H1 H2;Apply Zgt_lt;Apply Zle_gt_trans with m:=m;
+  [ Assumption | Apply Zlt_gt;Assumption ].
 Qed.
 
-Lemma Zgt_trans      : (n,m,p:Z)(Zgt n m)->(Zgt m p)->(Zgt n p).
+Lemma Zle_lt_trans : (n,m,p:Z)(Zle n m)->(Zlt m p)->(Zlt n p).
+Proof.
+Intros n m p H1 H2;Apply Zgt_lt;Apply Zgt_le_trans with m:=m; 
+  [ Apply Zlt_gt;Assumption | Assumption ].
+Qed.
 
-Unfold Zgt; Exact Zcompare_trans_SUPERIEUR.
+(** Transitivity of large orders *)
+
+Lemma Zle_trans : (n,m,p:Z)(Zle n m)->(Zle m p)->(Zle n p).
+Proof.
+Intros n m p H1 H2; Apply Znot_gt_le.
+Intro Hgt; Apply Zle_not_gt with n m. Assumption.
+Exact (Zgt_le_trans n p m Hgt H2).
 Qed.
 
-Lemma Zle_gt_S       : (n,p:Z)(Zle n p)->(Zgt (Zs p) n).
+Lemma Zge_trans : (n, m, p : Z) (Zge n m) -> (Zge m p) -> (Zge n p).
+Proof.
+Intros n m p H1 H2.
+Apply Zle_ge.
+Apply Zle_trans with m; Apply Zge_le; Trivial.
+Qed.
 
-Unfold Zle Zgt ;Intros n p H; (ElimCompare 'n 'p); [
-  Intros H1;Elim (Zcompare_EGAL n p);Intros H2 H3; Rewrite <- H2; [
-    Exact (Zgt_Sn_n n)
-  | Assumption ]
- 
-| Intros H1;Apply Zcompare_trans_SUPERIEUR with y:=p; [
-    Exact (Zgt_Sn_n p)
-  | Elim (Zcompare_ANTISYM p n); Auto with arith ]
-| Intros H1;Absurd (Zcompare n p)=SUPERIEUR;Assumption ].
+(** Compatibility of operations wrt to order *)
+
+Lemma Zgt_S_n        : (n,p:Z)(Zgt (Zs p) (Zs n))->(Zgt p n).
+Proof.
+Unfold Zs Zgt;Intros n p;Do 2 Rewrite -> [m:Z](Zplus_sym m (POS xH));
+Rewrite -> (Zcompare_Zplus_compatible p n (POS xH));Trivial with arith.
 Qed.
 
-Lemma Zgt_pred       
-	: (n,p:Z)(Zgt p (Zs n))->(Zgt (Zpred p) n).
+Lemma Zle_S_n     : (n,m:Z) (Zle (Zs m) (Zs n)) -> (Zle m n).
+Proof.
+Unfold Zle not ;Intros m n H1 H2;Apply H1;
+Unfold Zs ;Do 2 Rewrite <- (Zplus_sym (POS xH));
+Rewrite -> (Zcompare_Zplus_compatible n m (POS xH));Assumption.
+Qed.
 
-Unfold Zgt Zs Zpred ;Intros n p H; 
-Rewrite <- [x,y:Z](Zcompare_Zplus_compatible x y (POS xH));
-Rewrite (Zplus_sym p); Rewrite Zplus_assoc; Rewrite [x:Z](Zplus_sym x n);
-Simpl; Assumption.
+Lemma Zle_n_S : (n,m:Z) (Zle m n) -> (Zle (Zs m) (Zs n)).
+Proof.
+Unfold Zle not ;Intros m n H1 H2; Apply H1; 
+Rewrite <- (Zcompare_Zplus_compatible n m (POS xH));
+Do 2 Rewrite (Zplus_sym (POS xH)); Exact H2.
+Qed.
+
+Lemma Zgt_n_S : (n,m:Z)(Zgt m n) -> (Zgt (Zs m) (Zs n)).
+Proof.
+Unfold Zgt; Intros n m H; Rewrite Zcompare_n_S; Auto with arith.
 Qed.
 
 Lemma Zsimpl_gt_plus_l 
 	: (n,m,p:Z)(Zgt (Zplus p n) (Zplus p m))->(Zgt n m).
-
+Proof.
 Unfold Zgt; Intros n m p H; 
 	Rewrite <- (Zcompare_Zplus_compatible n m p); Assumption.
 Qed.
 
 Lemma Zsimpl_gt_plus_r
 	: (n,m,p:Z)(Zgt (Zplus n p) (Zplus m p))->(Zgt n m).
-
+Proof.
 Intros n m p H; Apply Zsimpl_gt_plus_l with p.
 Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial.
-
 Qed.
 
 Lemma Zgt_reg_l      
 	: (n,m,p:Z)(Zgt n m)->(Zgt (Zplus p n) (Zplus p m)).
-
+Proof.
 Unfold Zgt; Intros n m p H; Rewrite (Zcompare_Zplus_compatible n m p); 
 Assumption.
 Qed.
 
 Lemma Zgt_reg_r : (n,m,p:Z)(Zgt n m)->(Zgt (Zplus n p) (Zplus m p)).
+Proof.
 Intros n m p H; Rewrite (Zplus_sym n p); Rewrite (Zplus_sym m p); Apply Zgt_reg_l; Trivial.
 Qed.
 
-Theorem Zcompare_et_un: 
-  (x,y:Z) (Zcompare x y)=SUPERIEUR <-> 
-    ~(Zcompare x (Zplus y (POS xH)))=INFERIEUR.
-
-Intros x y; Split; [
-  Intro H; (ElimCompare 'x '(Zplus y (POS xH)));[
-    Intro H1; Rewrite H1; Discriminate
-  | Intros H1; Elim SUPERIEUR_POS with 1:=H; Intros h H2; 
-    Absurd (gt (convert h) O) /\ (lt (convert h) (S O)); [
-      Unfold not ;Intros H3;Elim H3;Intros H4 H5; Absurd (gt (convert h) O); [
-        Unfold gt ;Apply le_not_lt; Apply le_S_n; Exact H5
-      | Assumption]
-    | Split; [
-        Elim (ZL4 h); Intros i H3;Rewrite H3; Apply gt_Sn_O
-      | Change (lt (convert h) (convert xH)); 
-        Apply compare_convert_INFERIEUR;
-        Change (Zcompare (POS h) (POS xH))=INFERIEUR;
-        Rewrite <- H2; Rewrite <- [m,n:Z](Zcompare_Zplus_compatible m n y);
-        Rewrite (Zplus_sym x);Rewrite Zplus_assoc; Rewrite Zplus_inverse_r;
-        Simpl; Exact H1 ]]
-  | Intros H1;Rewrite -> H1;Discriminate ]
-| Intros H; (ElimCompare 'x '(Zplus y (POS xH))); [
-    Intros H1;Elim (Zcompare_EGAL x (Zplus y (POS xH))); Intros H2 H3;
-    Rewrite  (H2 H1); Exact (Zgt_Sn_n y)
-  | Intros H1;Absurd (Zcompare x (Zplus y (POS xH)))=INFERIEUR;Assumption
-  | Intros H1; Apply Zcompare_trans_SUPERIEUR with y:=(Zs y); 
-      [ Exact H1 | Exact (Zgt_Sn_n y) ]]].
-Qed.
+(** Order, predecessor and successor *)
 
-Lemma Zgt_S_n        : (n,p:Z)(Zgt (Zs p) (Zs n))->(Zgt p n).
-
-Unfold Zs Zgt;Intros n p;Do 2 Rewrite -> [m:Z](Zplus_sym m (POS xH));
-Rewrite -> (Zcompare_Zplus_compatible p n (POS xH));Trivial with arith.
-Qed.
-
-Lemma Zle_S_n     : (n,m:Z) (Zle (Zs m) (Zs n)) -> (Zle m n).
-
-Unfold Zle not ;Intros m n H1 H2;Apply H1;
-Unfold Zs ;Do 2 Rewrite <- (Zplus_sym (POS xH));
-Rewrite -> (Zcompare_Zplus_compatible n m (POS xH));Assumption.
+Lemma Zgt_Sn_n : (n:Z)(Zgt (Zs n) n).
+Proof.
+Exact Zcompare_Zs_SUPERIEUR.
 Qed.
 
 Lemma Zgt_le_S       : (n,p:Z)(Zgt p n)->(Zle (Zs n) p).
-
+Proof.
 Unfold Zgt Zle; Intros n p H; Elim (Zcompare_et_un p n); Intros H1 H2;
 Unfold not ;Intros H3; Unfold not in H1; Apply H1; [
   Assumption
@@ -272,507 +284,481 @@ Unfold not ;Intros H3; Unfold not in H1; Apply H1; [
 Qed.
 
 Lemma Zgt_S_le       : (n,p:Z)(Zgt (Zs p) n)->(Zle n p).
-
+Proof.
 Intros n p H;Apply Zle_S_n; Apply Zgt_le_S; Assumption.
 Qed.
 
-Theorem Zgt_S        : (n,m:Z)(Zgt (Zs n) m)->((Zgt n m)\/(<Z>m=n)).
-
-Intros n m H; Unfold Zgt; (ElimCompare 'n 'm); [
-  Elim (Zcompare_EGAL n m); Intros H1 H2 H3;Rewrite -> H1;Auto with arith
-| Intros H1;Absurd (Zcompare m n)=SUPERIEUR; 
-    [ Exact (Zgt_S_le m n H) | Elim (Zcompare_ANTISYM m n); Auto with arith ]
-| Auto with arith ].
-Qed.
-
-Theorem Zgt_trans_S  : (n,m,p:Z)(Zgt (Zs n) m)->(Zgt m p)->(Zgt n p).
-
-Intros n m p H1 H2;Apply Zle_gt_trans with m:=m;
-  [ Apply Zgt_S_le; Assumption | Assumption ].
-Qed.
-
-Theorem Zeq_S : (n,m:Z) n=m -> (Zs n)=(Zs m).
-Intros n m H; Rewrite H; Auto with arith.
+Lemma Zle_S_gt : (n,m:Z) (Zle (Zs n) m) -> (Zgt m n).
+Proof.
+Intros n m H;Apply Zle_gt_trans with m:=(Zs n);
+  [ Assumption | Apply Zgt_Sn_n ].
 Qed.
 
-Theorem Zpred_Sn : (m:Z) m=(Zpred (Zs m)).
-Intros m; Unfold Zpred Zs; Rewrite <- Zplus_assoc; Simpl; 
-Rewrite Zplus_sym; Auto with arith.
+Lemma Zle_gt_S       : (n,p:Z)(Zle n p)->(Zgt (Zs p) n).
+Proof.
+Intros n p H; Apply Zgt_le_trans with p.
+  Apply Zgt_Sn_n.
+  Assumption.
 Qed.
 
-Theorem Zeq_add_S : (n,m:Z) (Zs n)=(Zs m) -> n=m.
-Intros n m H.
-Change (Zplus (Zplus (NEG xH) (POS xH)) n)=
-       (Zplus (Zplus (NEG xH) (POS xH)) m);
-Do 2 Rewrite <- Zplus_assoc; Do 2 Rewrite (Zplus_sym (POS xH));
-Unfold Zs in H;Rewrite H; Trivial with arith.
+Lemma Zgt_pred       
+	: (n,p:Z)(Zgt p (Zs n))->(Zgt (Zpred p) n).
+Proof.
+Unfold Zgt Zs Zpred ;Intros n p H; 
+Rewrite <- [x,y:Z](Zcompare_Zplus_compatible x y (POS xH));
+Rewrite (Zplus_sym p); Rewrite Zplus_assoc; Rewrite [x:Z](Zplus_sym x n);
+Simpl; Assumption.
 Qed.
- 
-Theorem Znot_eq_S : (n,m:Z) ~(n=m) -> ~((Zs n)=(Zs m)).
 
-Unfold not ;Intros n m H1 H2;Apply H1;Apply Zeq_add_S; Assumption.
-Qed.
- 
-Lemma Zsimpl_plus_l : (n,m,p:Z)(Zplus n m)=(Zplus n p)->m=p.
-Intros n m p H; Cut (Zplus (Zopp n) (Zplus n m))=(Zplus (Zopp n) (Zplus n p));[
-  Do 2 Rewrite -> Zplus_assoc; Rewrite -> (Zplus_sym (Zopp n) n);
-  Rewrite -> Zplus_inverse_r;Simpl; Trivial with arith
-| Rewrite -> H; Trivial with arith ].
+Lemma Zlt_ZERO_pred_le_ZERO : (n:Z) (Zlt ZERO n) -> (Zle ZERO (Zpred n)).
+Intros x H.
+Rewrite (Zs_pred x) in H.
+Apply Zgt_S_le.
+Apply Zlt_gt.
+Assumption.
 Qed.
 
-Theorem Zn_Sn : (n:Z) ~(n=(Zs n)).
-Intros n;Cut ~ZERO=(POS xH);[
-  Unfold not ;Intros H1 H2;Apply H1;Apply (Zsimpl_plus_l n);Rewrite Zero_right;
-  Exact H2
-| Discriminate ].
-Qed.
+(** Special cases of ordered integers *)
 
-Lemma Zplus_n_O : (n:Z) n=(Zplus n ZERO).
-Intro; Rewrite Zero_right; Trivial with arith.
+Lemma Zle_n_Sn : (n:Z)(Zle n (Zs n)).
+Proof.
+Intros n; Apply Zgt_S_le;Apply Zgt_trans with m:=(Zs n) ;Apply Zgt_Sn_n.
 Qed.
 
-Lemma Zplus_unit_left : (n,m:Z) (Zplus n ZERO)=m -> n=m.
-Intro; Rewrite Zero_right; Trivial with arith.
+Lemma Zle_pred_n : (n:Z)(Zle (Zpred n) n).
+Proof.
+Intros n;Pattern 2 n ;Rewrite Zs_pred; Apply Zle_n_Sn.
 Qed.
 
-Lemma Zplus_unit_right : (n,m:Z) n=(Zplus m ZERO) -> n=m.
-Intros n m; Rewrite (Zero_right m); Trivial with arith.
+Lemma POS_gt_ZERO : (p:positive) (Zgt (POS p) ZERO).
+Unfold Zgt; Trivial.
 Qed.
 
-Lemma Zplus_n_Sm : (n,m:Z) (Zs (Zplus n m))=(Zplus n (Zs m)).
-
-Intros n m; Unfold Zs; Rewrite Zplus_assoc; Trivial with arith.
+  (* weaker but useful (in [Zpower] for instance) *)
+Lemma ZERO_le_POS : (p:positive) (Zle ZERO (POS p)).
+Intro; Unfold Zle; Discriminate.
 Qed.
 
-Lemma Zmult_n_O : (n:Z) ZERO=(Zmult n ZERO).
-
-Intro;Rewrite Zmult_sym;Simpl; Trivial with arith.
+Lemma NEG_lt_ZERO : (p:positive)(Zlt (NEG p) ZERO).
+Unfold Zlt; Trivial.
 Qed.
 
-Lemma Zmult_n_Sm : (n,m:Z) (Zplus (Zmult n m) n)=(Zmult n (Zs m)).
-
-Intros n m;Unfold Zs; Rewrite Zmult_plus_distr_r;
-Rewrite (Zmult_sym n (POS xH));Rewrite Zmult_one; Trivial with arith.
+(** Weakening equality within order *)
+ 
+Lemma Zlt_not_eq : (x,y:Z)(Zlt x y) -> ~x=y.
+Proof.
+Unfold not; Intros x y H H0.
+Rewrite H0 in H.
+Apply (Zlt_n_n ? H).
 Qed.
 
-Theorem Zle_n : (n:Z) (Zle n n).
-Intros n;Elim (Zcompare_EGAL n n);Unfold Zle ;Intros H1 H2;Rewrite H2;
-  [ Discriminate | Trivial with arith ].
-Qed. 
-
-Theorem Zle_refl : (n,m:Z) n=m -> (Zle n m).
+Lemma Zle_refl : (n,m:Z) n=m -> (Zle n m).
+Proof.
 Intros; Rewrite H; Apply Zle_n.
 Qed.
 
-Theorem Zle_trans : (n,m,p:Z)(Zle n m)->(Zle m p)->(Zle n p).
-
-Intros n m p;Unfold 1 3 Zle; Unfold not; Intros H1 H2 H3;Apply H1;
-Exact (Zgt_le_trans n p m H3 H2).
-Qed.
-
-Theorem Zle_n_Sn : (n:Z)(Zle n (Zs n)).
+(** Transitivity using successor *)
 
-Intros n; Apply Zgt_S_le;Apply Zgt_trans with m:=(Zs n) ;Apply Zgt_Sn_n.
+Lemma Zgt_trans_S  : (n,m,p:Z)(Zgt (Zs n) m)->(Zgt m p)->(Zgt n p).
+Proof.
+Intros n m p H1 H2;Apply Zle_gt_trans with m:=m;
+  [ Apply Zgt_S_le; Assumption | Assumption ].
 Qed.
 
-Lemma Zle_n_S : (n,m:Z) (Zle m n) -> (Zle (Zs m) (Zs n)).
-
-Unfold Zle not ;Intros m n H1 H2; Apply H1; 
-Rewrite <- (Zcompare_Zplus_compatible n m (POS xH));
-Do 2 Rewrite (Zplus_sym (POS xH)); Exact H2.
+Lemma Zgt_S        : (n,m:Z)(Zgt (Zs n) m)->((Zgt n m)\/(m=n)).
+Proof.
+Intros n m H.
+Assert Hle : (Zle m n).
+  Apply Zgt_S_le; Assumption.
+NewDestruct (Zle_lt_or_eq ? ? Hle) as [Hlt|Heq].
+  Left; Apply Zlt_gt; Assumption.  
+  Right; Assumption.
 Qed.
 
 Hints Resolve Zle_n Zle_n_Sn Zle_trans Zle_n_S : zarith.
 Hints Immediate Zle_refl : zarith.
 
-Lemma Zs_pred : (n:Z) n=(Zs (Zpred n)).
-
-Intros n; Unfold Zs Zpred ;Rewrite <- Zplus_assoc; Simpl; Rewrite Zero_right;
-Trivial with arith.
-Qed. 
-
-Hints Immediate Zs_pred : zarith.
- 
-Theorem Zle_pred_n : (n:Z)(Zle (Zpred n) n).
-
-Intros n;Pattern 2 n ;Rewrite Zs_pred; Apply Zle_n_Sn.
-Qed.
- 
-Theorem Zle_trans_S : (n,m:Z)(Zle (Zs n) m)->(Zle n m).
-
+Lemma Zle_trans_S : (n,m:Z)(Zle (Zs n) m)->(Zle n m).
+Proof.
 Intros n m H;Apply Zle_trans with m:=(Zs n); [ Apply Zle_n_Sn | Assumption ].
 Qed.
 
-Theorem Zle_Sn_n : (n:Z)~(Zle (Zs n) n).
-
+Lemma Zle_Sn_n : (n:Z)~(Zle (Zs n) n).
+Proof.
 Intros n; Apply Zgt_not_le; Apply Zgt_Sn_n.
 Qed.
 
-Theorem Zle_antisym : (n,m:Z)(Zle n m)->(Zle m n)->(n=m).
-
-Unfold Zle ;Intros n m H1 H2; (ElimCompare 'n 'm); [
-  Elim (Zcompare_EGAL n m);Auto with arith
-| Intros H3;Absurd (Zcompare m n)=SUPERIEUR; [
-    Assumption
-  | Elim (Zcompare_ANTISYM m n);Auto with arith ]
-| Intros H3;Absurd (Zcompare n m)=SUPERIEUR;Assumption ].
-Qed.
-
-Theorem Zgt_lt : (m,n:Z) (Zgt m n) -> (Zlt n m).
-Unfold Zgt Zlt ;Intros m n H; Elim (Zcompare_ANTISYM m n); Auto with arith.
-Qed.
-
-Theorem Zlt_gt : (m,n:Z) (Zlt m n) -> (Zgt n m).
-Unfold Zgt Zlt ;Intros m n H; Elim (Zcompare_ANTISYM n m); Auto with arith.
-Qed.
-
-Theorem Zge_le : (m,n:Z) (Zge m n) -> (Zle n m).
-Intros m n; Change ~(Zlt m n)-> ~(Zgt n m);
-Unfold not; Intros H1 H2; Apply H1; Apply Zgt_lt; Assumption.
-Qed.
-
-Theorem Zle_ge : (m,n:Z) (Zle m n) -> (Zge n m).
-Intros m n; Change ~(Zgt m n)-> ~(Zlt n m);
-Unfold not; Intros H1 H2; Apply H1; Apply Zlt_gt; Assumption.
-Qed.
-
-Theorem Zge_trans : (n, m, p : Z) (Zge n m) -> (Zge m p) -> (Zge n p).
-Intros n m p H1 H2.
-Apply Zle_ge.
-Apply Zle_trans with m; Apply Zge_le; Trivial.
-Qed.
-
-Theorem Zlt_n_Sn : (n:Z)(Zlt n (Zs n)).
+Lemma Zlt_n_Sn : (n:Z)(Zlt n (Zs n)).
+Proof.
 Intro n; Apply Zgt_lt; Apply Zgt_Sn_n.
 Qed.
-Theorem Zlt_S : (n,m:Z)(Zlt n m)->(Zlt n (Zs m)).
+
+Lemma Zlt_S : (n,m:Z)(Zlt n m)->(Zlt n (Zs m)).
 Intros n m H;Apply Zgt_lt; Apply Zgt_trans with m:=m; [
   Apply Zgt_Sn_n
 | Apply Zlt_gt; Assumption ].
 Qed.
 
-Theorem Zlt_n_S : (n,m:Z)(Zlt n m)->(Zlt (Zs n) (Zs m)).
+Lemma Zlt_n_S : (n,m:Z)(Zlt n m)->(Zlt (Zs n) (Zs m)).
+Proof.
 Intros n m H;Apply Zgt_lt;Apply Zgt_n_S;Apply Zlt_gt; Assumption.
 Qed.
 
-Theorem Zlt_S_n : (n,m:Z)(Zlt (Zs n) (Zs m))->(Zlt n m).
-
+Lemma Zlt_S_n : (n,m:Z)(Zlt (Zs n) (Zs m))->(Zlt n m).
+Proof.
 Intros n m H;Apply Zgt_lt;Apply Zgt_S_n;Apply Zlt_gt; Assumption.
 Qed.
 
-Theorem Zlt_n_n : (n:Z)~(Zlt n n).
-
-Intros n;Elim (Zcompare_EGAL n n); Unfold Zlt ;Intros H1 H2;
-Rewrite H2; [ Discriminate | Trivial with arith ].
-Qed.
-
 Lemma Zlt_pred : (n,p:Z)(Zlt (Zs n) p)->(Zlt n (Zpred p)).
-
+Proof.
 Intros n p H;Apply Zlt_S_n; Rewrite <- Zs_pred; Assumption.
 Qed.
 
 Lemma Zlt_pred_n_n : (n:Z)(Zlt (Zpred n) n).
-
+Proof.
 Intros n; Apply Zlt_S_n; Rewrite <- Zs_pred; Apply Zlt_n_Sn.
 Qed.
  
-Theorem Zlt_le_S : (n,p:Z)(Zlt n p)->(Zle (Zs n) p).
+Lemma Zlt_le_S : (n,p:Z)(Zlt n p)->(Zle (Zs n) p).
+Proof.
 Intros n p H; Apply Zgt_le_S; Apply Zlt_gt; Assumption.
 Qed.
 
-Theorem Zlt_n_Sm_le : (n,m:Z)(Zlt n (Zs m))->(Zle n m).
+Lemma Zlt_n_Sm_le : (n,m:Z)(Zlt n (Zs m))->(Zle n m).
+Proof.
 Intros n m H; Apply Zgt_S_le; Apply Zlt_gt; Assumption.
 Qed.
 
-Theorem Zle_lt_n_Sm : (n,m:Z)(Zle n m)->(Zlt n (Zs m)).
+Lemma Zle_lt_n_Sm : (n,m:Z)(Zle n m)->(Zlt n (Zs m)).
+Proof.
 Intros n m H; Apply Zgt_lt; Apply Zle_gt_S; Assumption.
 Qed.
 
-Theorem Zlt_le_weak : (n,m:Z)(Zlt n m)->(Zle n m).
-Unfold Zlt Zle ;Intros n m H;Rewrite H;Discriminate.
-Qed.
-
-Theorem Zlt_trans : (n,m,p:Z)(Zlt n m)->(Zlt m p)->(Zlt n p).
-Intros n m p H1 H2; Apply Zgt_lt; Apply Zgt_trans with m:= m; 
-Apply Zlt_gt; Assumption.
-Qed.
-Theorem Zlt_le_trans : (n,m,p:Z)(Zlt n m)->(Zle m p)->(Zlt n p).
-Intros n m p H1 H2;Apply Zgt_lt;Apply Zle_gt_trans with m:=m;
-  [ Assumption | Apply Zlt_gt;Assumption ].
-Qed.
-
-Theorem Zle_lt_trans : (n,m,p:Z)(Zle n m)->(Zlt m p)->(Zlt n p).
-
-Intros n m p H1 H2;Apply Zgt_lt;Apply Zgt_le_trans with m:=m; 
-  [ Apply Zlt_gt;Assumption | Assumption ].
-Qed.
- 
-Theorem Zle_lt_or_eq : (n,m:Z)(Zle n m)->((Zlt n m) \/ n=m).
-
-Unfold Zle Zlt ;Intros n m H; (ElimCompare 'n 'm); [
-  Elim (Zcompare_EGAL n m);Auto with arith
-| Auto with arith
-| Intros H';Absurd (Zcompare n m)=SUPERIEUR;Assumption ].
-Qed.
-
-Theorem Zle_or_lt : (n,m:Z)((Zle n m)\/(Zlt m n)).
-
-Unfold Zle Zlt ;Intros n m; (ElimCompare 'n 'm); [
-  Intros E;Rewrite -> E;Left;Discriminate
-| Intros E;Rewrite -> E;Left;Discriminate
-| Elim (Zcompare_ANTISYM n m); Auto with arith ].
-Qed.
-
-Theorem Zle_not_lt : (n,m:Z)(Zle n m) -> ~(Zlt m n).
-
-Unfold Zle Zlt; Unfold not ;Intros n m H1 H2;Apply H1; 
-Elim (Zcompare_ANTISYM n m);Auto with arith.
-Qed.
-
-Theorem Zlt_not_le : (n,m:Z)(Zlt n m) -> ~(Zle m n).
-Unfold Zlt Zle not ;Intros n m H1 H2; Apply H2; Elim (Zcompare_ANTISYM m n);
-Auto with arith.
-Qed.
-
-Theorem Zlt_not_sym : (n,m:Z)(Zlt n m) -> ~(Zlt m n).
-Intros n m H;Apply Zle_not_lt; Apply Zlt_le_weak; Assumption.
-Qed.
-
-Theorem Zle_le_S : (x,y:Z)(Zle x y)->(Zle x (Zs y)).
+Lemma Zle_le_S : (x,y:Z)(Zle x y)->(Zle x (Zs y)).
+Proof.
 Intros.
 Apply Zle_trans with y; Trivial with zarith.
 Qed.
 
 Hints Resolve Zle_le_S : zarith.
 
-Definition Zmin := [n,m:Z]
- <Z>Cases (Zcompare n m) of
-      EGAL      => n
-    | INFERIEUR => n
-    | SUPERIEUR => m
-    end.
-
-Lemma Zmin_SS : (n,m:Z)((Zs (Zmin n m))=(Zmin (Zs n) (Zs m))).
-
-Intros n m;Unfold Zmin; Rewrite (Zcompare_n_S n m);
-(ElimCompare 'n 'm);Intros E;Rewrite E;Auto with arith.
-Qed.
-
-Lemma Zle_min_l : (n,m:Z)(Zle (Zmin n m) n).
-
-Intros n m;Unfold Zmin ; (ElimCompare 'n 'm);Intros E;Rewrite -> E;
-  [ Apply Zle_n | Apply Zle_n | Apply Zlt_le_weak; Apply Zgt_lt;Exact E ].
-Qed.
-
-Lemma Zle_min_r : (n,m:Z)(Zle (Zmin n m) m).
-
-Intros n m;Unfold Zmin ; (ElimCompare 'n 'm);Intros E;Rewrite -> E;[
-  Unfold Zle ;Rewrite -> E;Discriminate
-| Unfold Zle ;Rewrite -> E;Discriminate
-| Apply Zle_n ].
-Qed.
-
-Lemma Zmin_case : (n,m:Z)(P:Z->Set)(P n)->(P m)->(P (Zmin n m)).
-Intros n m P H1 H2; Unfold Zmin; Case (Zcompare n m);Auto with arith.
-Qed.
-
-Lemma Zmin_or : (n,m:Z)(Zmin n m)=n \/ (Zmin n m)=m.
-Unfold Zmin; Intros; Elim (Zcompare n m); Auto.
-Qed.
-
-Lemma Zmin_n_n : (n:Z) (Zmin n n)=n.
-Unfold Zmin; Intros; Elim (Zcompare n n); Auto.
-Qed.
-
-Lemma Zplus_assoc_l : (n,m,p:Z)((Zplus n (Zplus m p))=(Zplus (Zplus n m) p)).
-
-Exact Zplus_assoc.
-Qed.
-
-Lemma Zplus_assoc_r : (n,m,p:Z)(Zplus (Zplus n m) p) =(Zplus n (Zplus m p)).
-
-Intros; Symmetry; Apply Zplus_assoc.
-Qed.
-
-Lemma Zplus_permute : (n,m,p:Z) (Zplus n (Zplus m p))=(Zplus m (Zplus n p)).
-
-Intros n m p;
-Rewrite Zplus_sym;Rewrite <- Zplus_assoc; Rewrite (Zplus_sym p n); Trivial with arith.
-Qed.
+(** Simplification and compatibility *)
 
 Lemma Zsimpl_le_plus_l : (p,n,m:Z)(Zle (Zplus p n) (Zplus p m))->(Zle n m).
-
+Proof.
 Intros p n m; Unfold Zle not ;Intros H1 H2;Apply H1; 
 Rewrite (Zcompare_Zplus_compatible n m p); Assumption.
 Qed.
  
 Lemma Zsimpl_le_plus_r : (p,n,m:Z)(Zle (Zplus n p) (Zplus m p))->(Zle n m).
-
+Proof.
 Intros p n m H; Apply Zsimpl_le_plus_l with p.
 Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial.
 Qed.
 
 Lemma Zle_reg_l : (n,m,p:Z)(Zle n m)->(Zle (Zplus p n) (Zplus p m)).
-
+Proof.
 Intros n m p; Unfold Zle not ;Intros H1 H2;Apply H1; 
 Rewrite <- (Zcompare_Zplus_compatible n m p); Assumption.
 Qed.
 
-Lemma Zle_reg_r : (a,b,c:Z) (Zle a b)->(Zle (Zplus a c) (Zplus b c)).
-
+Lemma Zle_reg_r : (n,m,p:Z) (Zle n m)->(Zle (Zplus n p) (Zplus m p)).
+Proof.
 Intros a b c;Do 2 Rewrite [n:Z](Zplus_sym n c); Exact (Zle_reg_l a b c).
 Qed.
 
 Lemma Zle_plus_plus : 
  (n,m,p,q:Z) (Zle n m)->(Zle p q)->(Zle (Zplus n p) (Zplus m q)).
-
+Proof.
 Intros n m p q; Intros H1 H2;Apply Zle_trans with m:=(Zplus n q); [
   Apply Zle_reg_l;Assumption | Apply Zle_reg_r;Assumption ].
 Qed.
 
-Lemma Zplus_Snm_nSm : (n,m:Z)(Zplus (Zs n) m)=(Zplus n (Zs m)).
-
-Unfold Zs ;Intros n m; Rewrite <- Zplus_assoc; Rewrite (Zplus_sym (POS xH));
-Trivial with arith.
-Qed.
-
 Lemma Zsimpl_lt_plus_l 
 	: (n,m,p:Z)(Zlt (Zplus p n) (Zplus p m))->(Zlt n m).
-
+Proof.
 Unfold Zlt ;Intros n m p; 
 	Rewrite Zcompare_Zplus_compatible;Trivial with arith.
 Qed.
  
 Lemma Zsimpl_lt_plus_r
 	: (n,m,p:Z)(Zlt (Zplus n p) (Zplus m p))->(Zlt n m).
-
+Proof.
 Intros n m p H; Apply Zsimpl_lt_plus_l with p.
 Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial.
 Qed.
  
 Lemma Zlt_reg_l : (n,m,p:Z)(Zlt n m)->(Zlt (Zplus p n) (Zplus p m)).
+Proof.
 Unfold Zlt ;Intros n m p; Rewrite Zcompare_Zplus_compatible;Trivial with arith.
 Qed.
 
 Lemma Zlt_reg_r : (n,m,p:Z)(Zlt n m)->(Zlt (Zplus n p) (Zplus m p)).
+Proof.
 Intros n m p H; Rewrite (Zplus_sym n p); Rewrite (Zplus_sym m p); Apply Zlt_reg_l; Trivial.
 Qed.
 
 Lemma Zlt_le_reg :
  (a,b,c,d:Z) (Zlt a b)->(Zle c d)->(Zlt (Zplus a c) (Zplus b d)).
+Proof.
 Intros a b c d H0 H1.
 Apply Zlt_le_trans with (Zplus b c).
 Apply  Zlt_reg_r; Trivial.
 Apply  Zle_reg_l; Trivial.
 Qed.
 
-
 Lemma Zle_lt_reg :
  (a,b,c,d:Z) (Zle a b)->(Zlt c d)->(Zlt (Zplus a c) (Zplus b d)).
+Proof.
 Intros a b c d H0 H1.
 Apply Zle_lt_trans with (Zplus b c).
 Apply  Zle_reg_r; Trivial.
 Apply  Zlt_reg_l; Trivial.
 Qed.
 
+(** Equivalence between inequalities (used in contrib/graph) *)
 
-Definition Zminus := [m,n:Z](Zplus m (Zopp n)).
+Lemma Zle_plus_swap : (x,y,z:Z) (Zle (Zplus x z) y) <-> (Zle x (Zminus y z)).
+Proof.
+    Intros. Split. Intro. Rewrite <- (Zero_right x). Rewrite <- (Zplus_inverse_r z).
+    Rewrite Zplus_assoc_l. Exact (Zle_reg_r ? ? ? H).
+    Intro. Rewrite <- (Zero_right y). Rewrite <- (Zplus_inverse_l z). Rewrite Zplus_assoc_l.
+    Apply Zle_reg_r. Assumption.
+Qed.
 
-V8Infix "-" Zminus : Z_scope.
+Lemma Zge_iff_le : (x,y:Z) (Zge x y) <-> (Zle y x).
+Proof.
+    Intros. Split. Intro. Apply Zge_le. Assumption.
+    Intro. Apply Zle_ge. Assumption.
+Qed.
 
-Lemma Zminus_plus_simpl : 
-  (n,m,p:Z)((Zminus n m)=(Zminus (Zplus p n) (Zplus p m))).
+Lemma Zlt_plus_swap : (x,y,z:Z) (Zlt (Zplus x z) y) <-> (Zlt x (Zminus y z)).
+Proof.
+    Intros. Split. Intro. Unfold Zminus. Rewrite Zplus_sym. Rewrite <- (Zero_left x).
+    Rewrite <- (Zplus_inverse_l z). Rewrite Zplus_assoc_r. Apply Zlt_reg_l. Rewrite Zplus_sym.
+    Assumption.
+    Intro. Rewrite Zplus_sym. Rewrite <- (Zero_left y). Rewrite <- (Zplus_inverse_r z).
+    Rewrite Zplus_assoc_r. Apply Zlt_reg_l. Rewrite Zplus_sym. Assumption.
+Qed.
 
-Intros n m p;Unfold Zminus; Rewrite Zopp_Zplus; Rewrite Zplus_assoc;
-Rewrite (Zplus_sym p); Rewrite <- (Zplus_assoc n p); Rewrite Zplus_inverse_r;
-Rewrite Zero_right; Trivial with arith.
+Lemma Zgt_iff_lt : (x,y:Z) (Zgt x y) <-> (Zlt y x).
+Proof.
+    Intros. Split. Intro. Apply Zgt_lt. Assumption.
+    Intro. Apply Zlt_gt. Assumption.
 Qed.
 
-Lemma Zminus_n_O : (n:Z)(n=(Zminus n ZERO)).
+Lemma Zeq_plus_swap : (x,y,z:Z) (Zplus x z)=y <-> x=(Zminus y z).
+Proof.
+    Intros. Split. Intro. Rewrite <- H. Unfold Zminus. Rewrite Zplus_assoc_r.
+    Rewrite Zplus_inverse_r. Apply sym_eq. Apply Zero_right.
+    Intro. Rewrite H. Unfold Zminus. Rewrite Zplus_assoc_r. Rewrite Zplus_inverse_l.
+    Apply Zero_right.
+Qed.
+
+(** Reverting [x ?= y] to trichotomy *)
+
+Lemma rename : (A:Set)(P:A->Prop)(x:A) ((y:A)(x=y)->(P y)) -> (P x).
+Auto with arith. 
+Qed.
+
+Theorem Zcompare_elim :
+  (c1,c2,c3:Prop)(x,y:Z)
+    ((x=y) -> c1) ->((Zlt x y) -> c2) ->((Zgt x y)-> c3)
+     -> Cases (Zcompare x y) of EGAL => c1 | INFERIEUR => c2 | SUPERIEUR => c3 end.
+Proof.
+Intros.
+Apply rename with x:=(Zcompare x y); Intro r; Elim r;
+[ Intro; Apply H; Apply (Zcompare_EGAL_eq x y); Assumption
+| Unfold Zlt in H0; Assumption
+| Unfold Zgt in H1; Assumption ].
+Qed.
 
-Intro; Unfold Zminus; Simpl;Rewrite Zero_right; Trivial with arith.
+Lemma Zcompare_eq_case : 
+  (c1,c2,c3:Prop)(x,y:Z) c1 -> x=y ->
+  Cases (Zcompare x y) of EGAL => c1 | INFERIEUR => c2 | SUPERIEUR => c3 end.
+Intros.
+Rewrite H0; Rewrite (Zcompare_x_x).
+Assumption.
 Qed.
 
-Lemma Zminus_n_n : (n:Z)(ZERO=(Zminus n n)).
-Intro; Unfold Zminus; Rewrite Zplus_inverse_r; Trivial with arith.
+(** Decompose an egality between two [?=] relations into 3 implications *)
+
+Theorem Zcompare_egal_dec :
+   (x1,y1,x2,y2:Z)
+    ((Zlt x1 y1)->(Zlt x2 y2))
+     ->((Zcompare x1 y1)=EGAL -> (Zcompare x2 y2)=EGAL)
+        ->((Zgt x1 y1)->(Zgt x2 y2))->(Zcompare x1 y1)=(Zcompare x2 y2).
+Intros x1 y1 x2 y2.
+Unfold Zgt; Unfold Zlt;
+Case (Zcompare x1 y1); Case (Zcompare x2 y2); Auto with arith; Symmetry; Auto with arith.
 Qed.
 
-Lemma Zplus_minus : (n,m,p:Z)(n=(Zplus m p))->(p=(Zminus n m)).
+(** Relating [x ?= y] to [Zle], [Zlt], [Zge] or [Zgt] *)
 
-Intros n m p H;Unfold Zminus;Apply (Zsimpl_plus_l m); 
-Rewrite (Zplus_sym m (Zplus n (Zopp m))); Rewrite <- Zplus_assoc;
-Rewrite Zplus_inverse_l; Rewrite Zero_right; Rewrite H; Trivial with arith.
+Lemma Zle_Zcompare :
+  (x,y:Z)(Zle x y) ->
+  Cases (Zcompare x y) of EGAL => True | INFERIEUR => True | SUPERIEUR => False end.
+Intros x y; Unfold Zle; Elim (Zcompare x y); Auto with arith.
 Qed.
- 
-Lemma Zminus_plus : (n,m:Z)(Zminus (Zplus n m) n)=m.
-Intros n m;Unfold Zminus ;Rewrite -> (Zplus_sym n m);Rewrite <- Zplus_assoc;
-Rewrite -> Zplus_inverse_r; Apply Zero_right.
+
+Lemma Zlt_Zcompare :
+  (x,y:Z)(Zlt x y)  ->
+  Cases (Zcompare x y) of EGAL => False | INFERIEUR => True | SUPERIEUR => False end.
+Intros x y; Unfold Zlt; Elim (Zcompare x y); Intros; Discriminate Orelse Trivial with arith.
 Qed.
 
-Lemma Zle_plus_minus : (n,m:Z) (Zplus n (Zminus m n))=m.
+Lemma Zge_Zcompare :
+  (x,y:Z)(Zge x y)->
+  Cases (Zcompare x y) of EGAL => True | INFERIEUR => False | SUPERIEUR => True end.
+Intros x y; Unfold Zge; Elim (Zcompare x y); Auto with arith. 
+Qed.
 
-Unfold Zminus; Intros n m; Rewrite Zplus_permute; Rewrite Zplus_inverse_r;
-Apply Zero_right.
+Lemma Zgt_Zcompare :
+  (x,y:Z)(Zgt x y) ->
+  Cases (Zcompare x y) of EGAL => False | INFERIEUR => False | SUPERIEUR => True end.
+Intros x y; Unfold Zgt; Elim (Zcompare x y); Intros; Discriminate Orelse Trivial with arith.
 Qed.
 
-Lemma Zminus_Sn_m : (n,m:Z)((Zs (Zminus n m))=(Zminus (Zs n) m)).
+(**********************************************************************)
+(** Minimum on binary integer numbers *)
 
-Intros n m;Unfold Zminus Zs; Rewrite (Zplus_sym n (Zopp m));
-Rewrite <- Zplus_assoc;Apply Zplus_sym.
+Definition Zmin := [n,m:Z]
+ <Z>Cases (Zcompare n m) of
+      EGAL      => n
+    | INFERIEUR => n
+    | SUPERIEUR => m
+    end.
+
+(** Properties of minimum on binary integer numbers *)
+
+Lemma Zmin_SS : (n,m:Z)((Zs (Zmin n m))=(Zmin (Zs n) (Zs m))).
+Proof.
+Intros n m;Unfold Zmin; Rewrite (Zcompare_n_S n m);
+(ElimCompare 'n 'm);Intros E;Rewrite E;Auto with arith.
 Qed.
 
-Lemma Zlt_minus : (n,m:Z)(Zlt ZERO m)->(Zlt (Zminus n m) n).
+Lemma Zle_min_l : (n,m:Z)(Zle (Zmin n m) n).
+Proof.
+Intros n m;Unfold Zmin ; (ElimCompare 'n 'm);Intros E;Rewrite -> E;
+  [ Apply Zle_n | Apply Zle_n | Apply Zlt_le_weak; Apply Zgt_lt;Exact E ].
+Qed.
 
-Intros n m H; Apply Zsimpl_lt_plus_l with p:=m; Rewrite Zle_plus_minus;
-Pattern 1 n ;Rewrite <- (Zero_right n); Rewrite (Zplus_sym m n);
-Apply Zlt_reg_l; Assumption.
+Lemma Zle_min_r : (n,m:Z)(Zle (Zmin n m) m).
+Proof.
+Intros n m;Unfold Zmin ; (ElimCompare 'n 'm);Intros E;Rewrite -> E;[
+  Unfold Zle ;Rewrite -> E;Discriminate
+| Unfold Zle ;Rewrite -> E;Discriminate
+| Apply Zle_n ].
 Qed.
 
-Lemma Zlt_O_minus_lt : (n,m:Z)(Zlt ZERO (Zminus n m))->(Zlt m n).
+Lemma Zmin_case : (n,m:Z)(P:Z->Set)(P n)->(P m)->(P (Zmin n m)).
+Proof.
+Intros n m P H1 H2; Unfold Zmin; Case (Zcompare n m);Auto with arith.
+Qed.
 
-Intros n m H; Apply Zsimpl_lt_plus_l with p:=(Zopp m); Rewrite Zplus_inverse_l;
-Rewrite Zplus_sym;Exact H.
+Lemma Zmin_or : (n,m:Z)(Zmin n m)=n \/ (Zmin n m)=m.
+Proof.
+Unfold Zmin; Intros; Elim (Zcompare n m); Auto.
 Qed.
 
-Lemma Zmult_plus_distr_l : 
-  (n,m,p:Z)((Zmult (Zplus n m) p)=(Zplus (Zmult n p) (Zmult m p))).
+Lemma Zmin_n_n : (n:Z) (Zmin n n)=n.
+Proof.
+Unfold Zmin; Intros; Elim (Zcompare n n); Auto.
+Qed.
 
-Intros n m p;Rewrite Zmult_sym;Rewrite Zmult_plus_distr_r; 
-Do 2 Rewrite -> (Zmult_sym p); Trivial with arith.
+Lemma Zmin_plus :
+ (x,y,n:Z)(Zmin (Zplus x n) (Zplus y n))=(Zplus (Zmin x y) n).
+Proof.
+Intros; Unfold Zmin.
+Rewrite (Zplus_sym x n);
+Rewrite (Zplus_sym y n);
+Rewrite (Zcompare_Zplus_compatible x y n).
+Case (Zcompare x y); Apply Zplus_sym.
 Qed.
 
-Lemma Zmult_minus_distr :
-  (n,m,p:Z)((Zmult (Zminus n m) p)=(Zminus (Zmult n p) (Zmult m p))).
-Intros n m p;Unfold Zminus; Rewrite Zmult_plus_distr_l; Rewrite Zopp_Zmult;
-Trivial with arith.
+(**********************************************************************)
+(* Absolute value on integers *)
+
+Definition absolu [x:Z] : nat :=
+  Cases x of
+     ZERO   => O
+  | (POS p) => (convert p)
+  | (NEG p) => (convert p)
+  end.
+
+Definition Zabs [z:Z] : Z :=
+  Cases z of 
+     ZERO   => ZERO
+  | (POS p) => (POS p)
+  | (NEG p) => (POS p)
+  end.
+
+(** Properties of absolute value *)
+
+Lemma Zabs_eq : (x:Z) (Zle ZERO x) -> (Zabs x)=x.
+NewDestruct x; Auto with arith.
+Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
 Qed.
- 
-Lemma Zmult_assoc_r : (n,m,p:Z)((Zmult (Zmult n m) p) = (Zmult n (Zmult m p))).
-Intros n m p; Rewrite Zmult_assoc; Trivial with arith.
+
+Lemma Zabs_non_eq : (x:Z) (Zle x ZERO) -> (Zabs x)=(Zopp x).
+Proof.
+NewDestruct x; Auto with arith.
+Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
 Qed.
 
-Lemma Zmult_assoc_l : (n,m,p:Z)(Zmult n (Zmult m p)) = (Zmult (Zmult n m) p).
-Intros n m p; Rewrite Zmult_assoc; Trivial with arith.
+Definition Zabs_dec : (x:Z){x=(Zabs x)}+{x=(Zopp (Zabs x))}.
+Proof.
+NewDestruct x;Auto with arith.
+Defined.
+
+Lemma Zabs_pos : (x:Z)(Zle ZERO (Zabs x)).
+NewDestruct x;Auto with arith; Compute; Intros H;Inversion H.
 Qed.
 
-Theorem Zmult_permute : (n,m,p:Z)(Zmult n (Zmult m p)) = (Zmult m (Zmult n p)).
-Intros; Rewrite -> (Zmult_assoc m n p); Rewrite -> (Zmult_sym m n).
-Apply Zmult_assoc.
+Lemma Zsgn_Zabs: (x:Z)(Zmult x (Zsgn x))=(Zabs x).
+Proof.
+NewDestruct x; Rewrite Zmult_sym; Auto with arith.
 Qed.
 
-Lemma Zmult_1_n : (n:Z)(Zmult (POS xH) n)=n.
-Exact Zmult_one.
+Lemma Zabs_Zsgn: (x:Z)(Zmult (Zabs x) (Zsgn x))=x.
+Proof.
+NewDestruct x; Rewrite Zmult_sym; Auto with arith.
 Qed.
 
-Lemma Zmult_n_1 : (n:Z)(Zmult n (POS xH))=n.
-Intro; Rewrite Zmult_sym; Apply Zmult_one.
+(** absolute value in nat is compatible with order *)
+
+Lemma absolu_lt : (x,y:Z) (Zle ZERO x)/\(Zlt x  y) -> (lt (absolu x) (absolu y)).
+Proof.
+Intros x y. Case x; Simpl. Case y; Simpl.
+
+Intro. Absurd (Zlt ZERO ZERO). Compute. Intro H0. Discriminate H0. Intuition.
+Intros. Elim (ZL4 p). Intros. Rewrite H0. Auto with arith.
+Intros. Elim (ZL4 p). Intros. Rewrite H0. Auto with arith.
+
+Case y; Simpl.
+Intros. Absurd (Zlt (POS p) ZERO). Compute. Intro H0. Discriminate H0. Intuition.
+Intros. Change (gt (convert p) (convert p0)).
+Apply compare_convert_SUPERIEUR.
+Elim H; Auto with arith. Intro. Exact (ZC2 p0 p).
+
+Intros. Absurd (Zlt (POS p0) (NEG p)).
+Compute. Intro H0. Discriminate H0. Intuition.
+
+Intros. Absurd (Zle ZERO (NEG p)). Compute. Auto with arith. Intuition.
 Qed.
 
-Lemma Zmult_Sm_n : (n,m:Z) (Zplus (Zmult n m) m)=(Zmult (Zs n) m).
-Intros n m; Unfold Zs; Rewrite Zmult_plus_distr_l; Rewrite Zmult_1_n;
-Trivial with arith.
+Lemma Zlt_minus : (n,m:Z)(Zlt ZERO m)->(Zlt (Zminus n m) n).
+Proof.
+Intros n m H; Apply Zsimpl_lt_plus_l with p:=m; Rewrite Zle_plus_minus;
+Pattern 1 n ;Rewrite <- (Zero_right n); Rewrite (Zplus_sym m n);
+Apply Zlt_reg_l; Assumption.
 Qed.
 
+Lemma Zlt_O_minus_lt : (n,m:Z)(Zlt ZERO (Zminus n m))->(Zlt m n).
+Proof.
+Intros n m H; Apply Zsimpl_lt_plus_l with p:=(Zopp m); Rewrite Zplus_inverse_l;
+Rewrite Zplus_sym;Exact H.
+Qed.
 
 (** Just for compatibility with previous versions. 
     Use [Zmult_plus_distr_r] and [Zmult_plus_distr_l] rather than