Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

20 files changed, 4191 insertions, 565 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 71e48360..1ff88604 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -6,10 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: BinInt.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: BinInt.v 11015 2008-05-28 20:06:42Z herbelin $ i*)
 
 (***********************************************************)
-(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 (***********************************************************)
 
 Require Export BinPos.
@@ -40,43 +40,48 @@ Arguments Scope Zneg [positive_scope].
 Definition Zdouble_plus_one (x:Z) :=
   match x with
     | Z0 => Zpos 1
-    | Zpos p => Zpos (xI p)
+    | Zpos p => Zpos p~1
     | Zneg p => Zneg (Pdouble_minus_one p)
   end.
 
 Definition Zdouble_minus_one (x:Z) :=
   match x with
     | Z0 => Zneg 1
-    | Zneg p => Zneg (xI p)
+    | Zneg p => Zneg p~1
     | Zpos p => Zpos (Pdouble_minus_one p)
   end.
 
 Definition Zdouble (x:Z) :=
   match x with
     | Z0 => Z0
-    | Zpos p => Zpos (xO p)
-    | Zneg p => Zneg (xO p)
+    | Zpos p => Zpos p~0
+    | Zneg p => Zneg p~0
   end.
 
+Open Local Scope positive_scope.
+
 Fixpoint ZPminus (x y:positive) {struct y} : Z :=
   match x, y with
-    | xI x', xI y' => Zdouble (ZPminus x' y')
-    | xI x', xO y' => Zdouble_plus_one (ZPminus x' y')
-    | xI x', xH => Zpos (xO x')
-    | xO x', xI y' => Zdouble_minus_one (ZPminus x' y')
-    | xO x', xO y' => Zdouble (ZPminus x' y')
-    | xO x', xH => Zpos (Pdouble_minus_one x')
-    | xH, xI y' => Zneg (xO y')
-    | xH, xO y' => Zneg (Pdouble_minus_one y')
-    | xH, xH => Z0
+    | p~1, q~1 => Zdouble (ZPminus p q)
+    | p~1, q~0 => Zdouble_plus_one (ZPminus p q)
+    | p~1, 1 => Zpos p~0
+    | p~0, q~1 => Zdouble_minus_one (ZPminus p q)
+    | p~0, q~0 => Zdouble (ZPminus p q)
+    | p~0, 1 => Zpos (Pdouble_minus_one p)
+    | 1, q~1 => Zneg q~0
+    | 1, q~0 => Zneg (Pdouble_minus_one q)
+    | 1, 1 => Z0
   end.
 
+Close Local Scope positive_scope.
+
 (** ** Addition on integers *)
 
 Definition Zplus (x y:Z) :=
   match x, y with
     | Z0, y => y
-    | x, Z0 => x
+    | Zpos x', Z0 => Zpos x'
+    | Zneg x', Z0 => Zneg x'
     | Zpos x', Zpos y' => Zpos (x' + y')
     | Zpos x', Zneg y' =>
       match (x' ?= y')%positive Eq with
@@ -217,6 +222,7 @@ Qed.
 
 
 (**********************************************************************)
+
 (** ** Properties of opposite on binary integer numbers *)
 
 Theorem Zopp_neg : forall p:positive, - Zneg p = Zpos p.
@@ -247,30 +253,6 @@ Proof.
       | simplify_eq H; intro E; rewrite E; trivial ].
 Qed.
 
-(*************************************************************************)
-(** **  Properties of the direct definition of successor and predecessor *)
-
-Lemma Zpred'_succ' : forall n:Z, Zpred' (Zsucc' n) = n.
-Proof.
-  intro x; destruct x; simpl in |- *.
-    reflexivity.
-  destruct p; simpl in |- *; try rewrite Pdouble_minus_one_o_succ_eq_xI;
-    reflexivity.
-  destruct p; simpl in |- *; try rewrite Psucc_o_double_minus_one_eq_xO;
-    reflexivity.
-Qed.
-
-Lemma Zsucc'_discr : forall n:Z, n <> Zsucc' n.
-Proof.
-  intro x; destruct x; simpl in |- *.
-  discriminate.
-  injection; apply Psucc_discr.
-  destruct p; simpl in |- *.
-    discriminate.
-    intro H; symmetry  in H; injection H; apply double_moins_un_xO_discr.
-    discriminate.
-Qed.
-
 (**********************************************************************)
 (** ** Other properties of binary integer numbers *)
 
@@ -313,10 +295,15 @@ Qed.
 Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m.
 Proof.
   intro x; destruct x as [| p| p]; intro y; destruct y as [| q| q];
-    simpl in |- *; reflexivity || destruct ((p ?= q)%positive Eq); 
+    simpl in |- *; reflexivity || destruct ((p ?= q)%positive Eq);
       reflexivity.
 Qed.
 
+Theorem Zopp_succ : forall n:Z, Zopp (Zsucc n) = Zpred (Zopp n).
+Proof.
+intro; unfold Zsucc; now rewrite Zopp_plus_distr.
+Qed.
+
 (** ** opposite is inverse for addition *)
 
 Theorem Zplus_opp_r : forall n:Z, n + - n = Z0.
@@ -520,11 +507,13 @@ Proof.
       trivial with arith.
 Qed.
 
-Lemma Zplus_succ_r : forall n m:Z, Zsucc (n + m) = n + Zsucc m.
+Lemma Zplus_succ_r_reverse : forall n m:Z, Zsucc (n + m) = n + Zsucc m.
 Proof.
   intros n m; unfold Zsucc in |- *; rewrite Zplus_assoc; trivial with arith.
 Qed.
 
+Notation Zplus_succ_r := Zplus_succ_r_reverse (only parsing).
+
 Lemma Zplus_succ_comm : forall n m:Z, Zsucc n + m = n + Zsucc m.
 Proof.
   unfold Zsucc in |- *; intros n m; rewrite <- Zplus_assoc;
@@ -586,10 +575,10 @@ Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n).
 Proof.
   intros n; unfold Zsucc, Zpred in |- *; rewrite <- Zplus_assoc; simpl in |- *;
     rewrite Zplus_0_r; trivial with arith.
-Qed. 
+Qed.
 
 Hint Immediate Zsucc_pred: zarith.
- 
+
 Theorem Zpred_succ : forall n:Z, n = Zpred (Zsucc n).
 Proof.
   intros m; unfold Zpred, Zsucc in |- *; rewrite <- Zplus_assoc; simpl in |- *;
@@ -603,7 +592,59 @@ Proof.
     do 2 rewrite <- Zplus_assoc; do 2 rewrite (Zplus_comm (Zpos 1));
       unfold Zsucc in H; rewrite H; trivial with arith.
 Qed.
- 
+
+(*************************************************************************)
+(** **  Properties of the direct definition of successor and predecessor *)
+
+Theorem Zsucc_succ' : forall n:Z, Zsucc n = Zsucc' n.
+Proof.
+destruct n as [| p | p]; simpl.
+reflexivity.
+now rewrite Pplus_one_succ_r.
+now destruct p as [q | q |].
+Qed.
+
+Theorem Zpred_pred' : forall n:Z, Zpred n = Zpred' n.
+Proof.
+destruct n as [| p | p]; simpl.
+reflexivity.
+now destruct p as [q | q |].
+now rewrite Pplus_one_succ_r.
+Qed.
+
+Theorem Zsucc'_inj : forall n m:Z, Zsucc' n = Zsucc' m -> n = m.
+Proof.
+intros n m; do 2 rewrite <- Zsucc_succ'; now apply Zsucc_inj.
+Qed.
+
+Theorem Zsucc'_pred' : forall n:Z, Zsucc' (Zpred' n) = n.
+Proof.
+intro; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred';
+symmetry; apply Zsucc_pred.
+Qed.
+
+Theorem Zpred'_succ' : forall n:Z, Zpred' (Zsucc' n) = n.
+Proof.
+intro; apply Zsucc'_inj; now rewrite Zsucc'_pred'.
+Qed.
+
+Theorem Zpred'_inj : forall n m:Z, Zpred' n = Zpred' m -> n = m.
+Proof.
+intros n m H.
+rewrite <- (Zsucc'_pred' n); rewrite <- (Zsucc'_pred' m); now rewrite H.
+Qed.
+
+Theorem Zsucc'_discr : forall n:Z, n <> Zsucc' n.
+Proof.
+  intro x; destruct x; simpl in |- *.
+  discriminate.
+  injection; apply Psucc_discr.
+  destruct p; simpl in |- *.
+    discriminate.
+    intro H; symmetry  in H; injection H; apply double_moins_un_xO_discr.
+    discriminate.
+Qed.
+
 (** Misc properties, usually redundant or non natural *)
 
 Lemma Zsucc_eq_compat : forall n m:Z, n = m -> Zsucc n = Zsucc m.
@@ -645,6 +686,22 @@ Qed.
 
 (** ** Relating [minus] with [plus] and [Zsucc] *)
 
+Lemma Zminus_plus_distr : forall n m p:Z, n - (m + p) = n - m - p.
+Proof.
+intros; unfold Zminus; rewrite Zopp_plus_distr; apply Zplus_assoc.
+Qed.
+
+Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m.
+Proof.
+  intros n m; unfold Zminus, Zsucc in |- *; rewrite (Zplus_comm n (- m));
+    rewrite <- Zplus_assoc; apply Zplus_comm.
+Qed.
+
+Lemma Zminus_succ_r : forall n m:Z, n - (Zsucc m) = Zpred (n - m).
+Proof.
+intros; unfold Zsucc; now rewrite Zminus_plus_distr.
+Qed.
+
 Lemma Zplus_minus_eq : forall n m p:Z, n = m + p -> p = n - m.
 Proof.
   intros n m p H; unfold Zminus in |- *; apply (Zplus_reg_l m);
@@ -665,12 +722,6 @@ Proof.
     apply Zplus_0_r.
 Qed.
 
-Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m.
-Proof.
-  intros n m; unfold Zminus, Zsucc in |- *; rewrite (Zplus_comm n (- m));
-    rewrite <- Zplus_assoc; apply Zplus_comm.
-Qed.
-
 Lemma Zminus_plus_simpl_l : forall n m p:Z, p + n - (p + m) = n - m.
 Proof.
   intros n m p; unfold Zminus in |- *; rewrite Zopp_plus_distr;
@@ -696,6 +747,16 @@ Proof.
   reflexivity.
 Qed.
 
+Lemma Zpos_minus_morphism : forall a b:positive, Pcompare a b Eq = Lt -> 
+  Zpos (b-a) = Zpos b - Zpos a.
+Proof.
+  intros.
+  simpl.
+  change Eq with (CompOpp Eq).
+  rewrite <- Pcompare_antisym.
+  rewrite H; simpl; auto.
+Qed.
+
 (** ** Misc redundant properties *)
 
 Lemma Zeq_minus : forall n m:Z, n = m -> n - m = Z0.
@@ -805,6 +866,19 @@ Proof.
 	reflexivity).
 Qed.
 
+(** ** Multiplication and Doubling *)
+
+Lemma Zdouble_mult : forall z, Zdouble z = (Zpos 2) * z.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma Zdouble_plus_one_mult : forall z, 
+  Zdouble_plus_one z = (Zpos 2) * z + (Zpos 1).
+Proof.
+  destruct z; simpl; auto with zarith.
+Qed.
+
 (** ** Multiplication and Opposite *)
 
 Theorem Zopp_mult_distr_l : forall n m:Z, - (n * m) = - n * m.
@@ -967,22 +1041,37 @@ Qed.
 (**********************************************************************)
 (** * Relating binary positive numbers and binary integers *)
 
-Lemma Zpos_xI : forall p:positive, Zpos (xI p) = Zpos 2 * Zpos p + Zpos 1.
+Lemma Zpos_eq : forall p q:positive, p = q -> Zpos p = Zpos q.
+Proof.
+  intros; f_equal; auto.
+Qed.
+
+Lemma Zpos_eq_rev : forall p q:positive, Zpos p = Zpos q -> p = q.
+Proof.
+  inversion 1; auto.
+Qed.
+
+Lemma Zpos_eq_iff : forall p q:positive, p = q <-> Zpos p = Zpos q.
+Proof.
+  split; [apply Zpos_eq|apply Zpos_eq_rev].
+Qed.
+
+Lemma Zpos_xI : forall p:positive, Zpos p~1 = Zpos 2 * Zpos p + Zpos 1.
 Proof.
   intro; apply refl_equal.
 Qed.
 
-Lemma Zpos_xO : forall p:positive, Zpos (xO p) = Zpos 2 * Zpos p.
+Lemma Zpos_xO : forall p:positive, Zpos p~0 = Zpos 2 * Zpos p.
 Proof.
   intro; apply refl_equal.
 Qed.
 
-Lemma Zneg_xI : forall p:positive, Zneg (xI p) = Zpos 2 * Zneg p - Zpos 1.
+Lemma Zneg_xI : forall p:positive, Zneg p~1 = Zpos 2 * Zneg p - Zpos 1.
 Proof.
   intro; apply refl_equal.
 Qed.
 
-Lemma Zneg_xO : forall p:positive, Zneg (xO p) = Zpos 2 * Zneg p.
+Lemma Zneg_xO : forall p:positive, Zneg p~0 = Zpos 2 * Zneg p.
 Proof.
   reflexivity.
 Qed.
@@ -1057,7 +1146,8 @@ Definition Zabs_N (z:Z) :=
     | Zneg p => Npos p
   end.
 
-Definition Z_of_N (x:N) := match x with
-                             | N0 => Z0
-                             | Npos p => Zpos p
-                           end.
+Definition Z_of_N (x:N) := 
+  match x with
+    | N0 => Z0
+    | Npos p => Zpos p
+  end.
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index 3cee9190..fcb44d6f 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -7,11 +7,11 @@
 (***********************************************************************)
 
 (* Finite sets library.  
- * Authors: Pierre Letouzey and Jean-Christophe Filliâtre 
- * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
+ * Authors: Pierre Letouzey and Jean-Christophe Filliâtre 
+ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: Int.v 9319 2006-10-30 12:41:21Z barras $ *)
+(* $Id: Int.v 10739 2008-04-01 14:45:20Z herbelin $ *)
 
 (** An axiomatization of integers. *) 
 
@@ -352,46 +352,15 @@ Module MoreInt (I:Int).
   Ltac i2z_refl := 
     i2z_gen;
     match goal with |- ?t => 
-      let e := p2ep t 
-	in 
-	(change (ep2p e); 
-	  apply norm_ep_correct2; 
-	    simpl)
+      let e := p2ep t in 
+      change (ep2p e); apply norm_ep_correct2; simpl
     end.
 
-  Ltac iauto := i2z_refl; auto.
-  Ltac iomega := i2z_refl; intros; romega.
-
-  Open Scope Z_scope.
-
-  Lemma max_spec : forall (x y:Z), 
-    x >= y /\ Zmax x y = x  \/
-    x < y /\ Zmax x y = y.
-  Proof.
-    intros; unfold Zmax, Zlt, Zge.
-    destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate.
-  Qed.
-
-  Ltac omega_max_genspec x y := 
-    generalize (max_spec x y); 
-    (let z := fresh "z" in let Hz := fresh "Hz" in 
-     set (z:=Zmax x y); clearbody z).
-
-  Ltac omega_max_loop := 
-    match goal with 
-      (* hack: we don't want [i2z (height ...)] to be reduced by romega later... *)
-      | |- context [ i2z (?f ?x) ] => 
-          let i := fresh "i2z" in (set (i:=i2z (f x)); clearbody i); omega_max_loop
-      | |- context [ Zmax ?x ?y ] => omega_max_genspec x y; omega_max_loop
-      | _ => intros
-    end.
-
-  Ltac omega_max := i2z_refl; omega_max_loop; try romega.
+  (* i2z_refl can be replaced below by (simpl in *; i2z). 
+     The reflexive version improves compilation of AVL files by about 15%  *)
   
-  Ltac false_omega := i2z_refl; intros; romega.
-  Ltac false_omega_max := elimtype False; omega_max.
+  Ltac omega_max := i2z_refl; romega with Z.
 
-  Open Scope Int_scope.
 End MoreInt.
 
 
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index 7febbf6a..b831afee 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ZArith_dec.v 9958 2007-07-06 22:47:40Z letouzey $ i*)
+(*i $Id: ZArith_dec.v 9759 2007-04-12 17:46:54Z notin $ i*)
 
 Require Import Sumbool.
 
diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v
new file mode 100644
index 00000000..03e061f2
--- /dev/null
+++ b/theories/ZArith/ZOdiv.v
@@ -0,0 +1,953 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+
+Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing.
+Require Export ZOdiv_def.
+Require Zdiv.
+
+Open Scope Z_scope.
+
+(** This file provides results about the Round-Toward-Zero Euclidean 
+  division [ZOdiv_eucl], whose projections are [ZOdiv] and [ZOmod].
+  Definition of this division can be found in file [ZOdiv_def]. 
+
+  This division and the one defined in Zdiv agree only on positive 
+  numbers. Otherwise, Zdiv performs Round-Toward-Bottom. 
+
+  The current approach is compatible with the division of usual 
+  programming languages such as Ocaml. In addition, it has nicer 
+  properties with respect to opposite and other usual operations.
+*)
+
+(** Since ZOdiv and Zdiv are not meant to be used concurrently, 
+   we reuse the same notation. *)
+
+Infix "/" := ZOdiv : Z_scope.
+Infix "mod" := ZOmod (at level 40, no associativity) : Z_scope.
+
+Infix "/" := Ndiv : N_scope.
+Infix "mod" := Nmod (at level 40, no associativity) : N_scope.
+
+(** Auxiliary results on the ad-hoc comparison [NPgeb]. *)
+
+Lemma NPgeb_Zge : forall (n:N)(p:positive), 
+  NPgeb n p = true -> Z_of_N n >= Zpos p.
+Proof.
+ destruct n as [|n]; simpl; intros.
+ discriminate.
+ red; simpl; destruct Pcompare; now auto.
+Qed.
+
+Lemma NPgeb_Zlt : forall (n:N)(p:positive), 
+  NPgeb n p = false -> Z_of_N n < Zpos p.
+Proof.
+ destruct n as [|n]; simpl; intros.
+ red; auto.
+ red; simpl; destruct Pcompare; now auto.
+Qed.
+
+(** * Relation between division on N and on Z. *)
+
+Lemma Ndiv_Z0div : forall a b:N, 
+  Z_of_N (a/b) = (Z_of_N a / Z_of_N b).
+Proof.
+  intros.
+  destruct a; destruct b; simpl; auto.
+  unfold Ndiv, ZOdiv; simpl; destruct Pdiv_eucl; auto.
+Qed.
+
+Lemma Nmod_Z0mod : forall a b:N, 
+  Z_of_N (a mod b) = (Z_of_N a) mod (Z_of_N b).
+Proof.
+  intros.
+  destruct a; destruct b; simpl; auto.
+  unfold Nmod, ZOmod; simpl; destruct Pdiv_eucl; auto.
+Qed.
+
+(** * Characterization of this euclidean division. *)
+
+(** First, the usual equation [a=q*b+r]. Notice that [a mod 0] 
+   has been chosen to be [a], so this equation holds even for [b=0].
+*)
+
+Theorem N_div_mod_eq : forall a b, 
+  a = (b * (Ndiv a b) + (Nmod a b))%N.
+Proof.
+  intros; generalize (Ndiv_eucl_correct a b).
+  unfold Ndiv, Nmod; destruct Ndiv_eucl; simpl.
+  intro H; rewrite H; rewrite Nmult_comm; auto.
+Qed.
+
+Theorem ZO_div_mod_eq : forall a b, 
+  a = b * (ZOdiv a b) + (ZOmod a b).
+Proof.
+  intros; generalize (ZOdiv_eucl_correct a b).
+  unfold ZOdiv, ZOmod; destruct ZOdiv_eucl; simpl.
+  intro H; rewrite H; rewrite Zmult_comm; auto.
+Qed.
+
+(** Then, the inequalities constraining the remainder. *)
+
+Theorem Pdiv_eucl_remainder : forall a b:positive, 
+  Z_of_N (snd (Pdiv_eucl a b)) < Zpos b. 
+Proof.
+  induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta.
+  intros b; generalize (IHa b); case Pdiv_eucl.
+    intros q1 r1 Hr1; simpl in Hr1.
+    case_eq (NPgeb (2*r1+1) b); intros; unfold snd.
+    romega with *.
+    apply NPgeb_Zlt; auto.
+  intros b; generalize (IHa b); case Pdiv_eucl.
+    intros q1 r1 Hr1; simpl in Hr1.
+    case_eq (NPgeb (2*r1) b); intros; unfold snd.
+    romega with *.
+    apply NPgeb_Zlt; auto.
+  destruct b; simpl; romega with *.
+Qed.
+
+Theorem Nmod_lt : forall (a b:N), b<>0%N -> 
+  (a mod b < b)%N.
+Proof.
+  destruct b as [ |b]; intro H; try solve [elim H;auto].
+  destruct a as [ |a]; try solve [compute;auto]; unfold Nmod, Ndiv_eucl.
+  generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl.
+  romega with *.
+Qed.
+
+(** The remainder is bounded by the divisor, in term of absolute values *)
+
+Theorem ZOmod_lt : forall a b:Z, b<>0 -> 
+  Zabs (a mod b) < Zabs b.
+Proof.
+  destruct b as [ |b|b]; intro H; try solve [elim H;auto]; 
+  destruct a as [ |a|a]; try solve [compute;auto]; unfold ZOmod, ZOdiv_eucl; 
+  generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl; 
+  try rewrite Zabs_Zopp; rewrite Zabs_eq; auto; apply Z_of_N_le_0.
+Qed.
+
+(** The sign of the remainder is the one of [a]. Due to the possible 
+   nullity of [a], a general result is to be stated in the following form:
+*)   
+
+Theorem ZOmod_sgn : forall a b:Z, 
+  0 <= Zsgn (a mod b) * Zsgn a.
+Proof.
+  destruct b as [ |b|b]; destruct a as [ |a|a]; simpl; auto with zarith;
+  unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl;
+  simpl; destruct n0; simpl; auto with zarith.
+Qed.
+
+(** This can also be said in a simplier way: *)
+
+Theorem Zsgn_pos_iff : forall z, 0 <= Zsgn z <-> 0 <= z.
+Proof.
+ destruct z; simpl; intuition auto with zarith.
+Qed.
+
+Theorem ZOmod_sgn2 : forall a b:Z, 
+  0 <= (a mod b) * a.
+Proof.
+  intros; rewrite <-Zsgn_pos_iff, Zsgn_Zmult; apply ZOmod_sgn.
+Qed.  
+
+(** Reformulation of [ZOdiv_lt] and [ZOmod_sgn] in 2 
+  then 4 particular cases. *)
+
+Theorem ZOmod_lt_pos : forall a b:Z, 0<=a -> b<>0 ->   
+  0 <= a mod b < Zabs b.
+Proof.
+  intros.
+  assert (0 <= a mod b).
+   generalize (ZOmod_sgn a b).
+   destruct (Zle_lt_or_eq 0 a H).
+   rewrite <- Zsgn_pos in H1; rewrite H1; romega with *.
+   subst a; simpl; auto.
+  generalize (ZOmod_lt a b H0); romega with *.
+Qed.
+
+Theorem ZOmod_lt_neg : forall a b:Z, a<=0 -> b<>0 ->   
+  -Zabs b < a mod b <= 0.
+Proof.
+  intros.
+  assert (a mod b <= 0).
+   generalize (ZOmod_sgn a b).
+   destruct (Zle_lt_or_eq a 0 H).
+   rewrite <- Zsgn_neg in H1; rewrite H1; romega with *.
+   subst a; simpl; auto.
+  generalize (ZOmod_lt a b H0); romega with *.
+Qed.
+
+Theorem ZOmod_lt_pos_pos : forall a b:Z, 0<=a -> 0<b -> 0 <= a mod b < b.
+Proof.
+  intros; generalize (ZOmod_lt_pos a b); romega with *.
+Qed.
+
+Theorem ZOmod_lt_pos_neg : forall a b:Z, 0<=a -> b<0 -> 0 <= a mod b < -b.
+Proof.
+  intros; generalize (ZOmod_lt_pos a b); romega with *.
+Qed.
+
+Theorem ZOmod_lt_neg_pos : forall a b:Z, a<=0 -> 0<b -> -b < a mod b <= 0.
+Proof.
+  intros; generalize (ZOmod_lt_neg a b); romega with *.
+Qed.
+
+Theorem ZOmod_lt_neg_neg : forall a b:Z, a<=0 -> b<0 -> b < a mod b <= 0.
+Proof.
+  intros; generalize (ZOmod_lt_neg a b); romega with *.
+Qed.
+
+(** * Division and Opposite *)
+
+(* The precise equalities that are invalid with "historic" Zdiv. *)
+
+Theorem ZOdiv_opp_l : forall a b:Z, (-a)/b = -(a/b).
+Proof.
+ destruct a; destruct b; simpl; auto; 
+  unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
+Qed.
+
+Theorem ZOdiv_opp_r : forall a b:Z, a/(-b) = -(a/b).
+Proof.
+ destruct a; destruct b; simpl; auto; 
+  unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
+Qed.
+
+Theorem ZOmod_opp_l : forall a b:Z, (-a) mod b = -(a mod b).
+Proof.
+ destruct a; destruct b; simpl; auto; 
+  unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
+Qed.
+
+Theorem ZOmod_opp_r : forall a b:Z, a mod (-b) = a mod b.
+Proof.
+ destruct a; destruct b; simpl; auto; 
+  unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
+Qed.
+
+Theorem ZOdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b.
+Proof.
+ destruct a; destruct b; simpl; auto; 
+  unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
+Qed.
+
+Theorem ZOmod_opp_opp : forall a b:Z, (-a) mod (-b) = -(a mod b).
+Proof.
+ destruct a; destruct b; simpl; auto; 
+  unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
+Qed.
+
+(** * Unicity results *)
+
+Definition Remainder a b r := 
+  (0 <= a /\ 0 <= r < Zabs b) \/ (a <= 0 /\ -Zabs b < r <= 0).
+
+Definition Remainder_alt a b r := 
+  Zabs r < Zabs b /\ 0 <= r * a.
+
+Lemma Remainder_equiv : forall a b r, 
+ Remainder a b r <-> Remainder_alt a b r.
+Proof.
+  unfold Remainder, Remainder_alt; intuition.
+  romega with *.
+  romega with *.
+  rewrite <-(Zmult_opp_opp).
+  apply Zmult_le_0_compat; romega.
+  assert (0 <= Zsgn r * Zsgn a) by (rewrite <-Zsgn_Zmult, Zsgn_pos_iff; auto). 
+  destruct r; simpl Zsgn in *; romega with *.
+Qed.
+
+Theorem ZOdiv_mod_unique_full:
+ forall a b q r, Remainder a b r -> 
+   a = b*q + r -> q = a/b /\ r = a mod b.
+Proof.
+  destruct 1 as [(H,H0)|(H,H0)]; intros.
+  apply Zdiv.Zdiv_mod_unique with b; auto.
+  apply ZOmod_lt_pos; auto.
+  romega with *.
+  rewrite <- H1; apply ZO_div_mod_eq.
+
+  rewrite <- (Zopp_involutive a).
+  rewrite ZOdiv_opp_l, ZOmod_opp_l.
+  generalize (Zdiv.Zdiv_mod_unique b (-q) (-a/b) (-r) (-a mod b)).
+  generalize (ZOmod_lt_pos (-a) b).
+  rewrite <-ZO_div_mod_eq, <-Zopp_mult_distr_r, <-Zopp_plus_distr, <-H1.
+  romega with *.
+Qed.
+
+Theorem ZOdiv_unique_full: 
+ forall a b q r, Remainder a b r -> 
+  a = b*q + r -> q = a/b.
+Proof.
+ intros; destruct (ZOdiv_mod_unique_full a b q r); auto.
+Qed.
+
+Theorem ZOdiv_unique:
+ forall a b q r, 0 <= a -> 0 <= r < b -> 
+   a = b*q + r -> q = a/b.
+Proof.
+  intros; eapply ZOdiv_unique_full; eauto.
+  red; romega with *.
+Qed.
+
+Theorem ZOmod_unique_full: 
+ forall a b q r, Remainder a b r -> 
+  a = b*q + r -> r = a mod b.
+Proof.
+ intros; destruct (ZOdiv_mod_unique_full a b q r); auto.
+Qed.
+
+Theorem ZOmod_unique:
+ forall a b q r, 0 <= a -> 0 <= r < b -> 
+   a = b*q + r -> r = a mod b.
+Proof.
+  intros; eapply ZOmod_unique_full; eauto.
+  red; romega with *.
+Qed.
+
+(** * Basic values of divisions and modulo. *)
+
+Lemma ZOmod_0_l: forall a, 0 mod a = 0.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma ZOmod_0_r: forall a, a mod 0 = a.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma ZOdiv_0_l: forall a, 0/a = 0.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma ZOdiv_0_r: forall a, a/0 = 0.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma ZOmod_1_r: forall a, a mod 1 = 0.
+Proof.
+  intros; symmetry; apply ZOmod_unique_full with a; auto with zarith.
+  rewrite Remainder_equiv; red; simpl; auto with zarith.
+Qed.
+
+Lemma ZOdiv_1_r: forall a, a/1 = a.
+Proof.
+  intros; symmetry; apply ZOdiv_unique_full with 0; auto with zarith.
+  rewrite Remainder_equiv; red; simpl; auto with zarith.
+Qed.
+
+Hint Resolve ZOmod_0_l ZOmod_0_r ZOdiv_0_l ZOdiv_0_r ZOdiv_1_r ZOmod_1_r 
+ : zarith.
+
+Lemma ZOdiv_1_l: forall a, 1 < a -> 1/a = 0.
+Proof.
+  intros; symmetry; apply ZOdiv_unique with 1; auto with zarith.
+Qed.
+
+Lemma ZOmod_1_l: forall a, 1 < a ->  1 mod a = 1.
+Proof.
+  intros; symmetry; apply ZOmod_unique with 0; auto with zarith.
+Qed.
+
+Lemma ZO_div_same : forall a:Z, a<>0 -> a/a = 1.
+Proof.
+  intros; symmetry; apply ZOdiv_unique_full with 0; auto with *.
+  rewrite Remainder_equiv; red; simpl; romega with *.
+Qed.
+
+Lemma ZO_mod_same : forall a, a mod a = 0.
+Proof.
+  destruct a; intros; symmetry.
+  compute; auto.
+  apply ZOmod_unique with 1; auto with *; romega with *.
+  apply ZOmod_unique_full with 1; auto with *; red; romega with *.
+Qed.
+
+Lemma ZO_mod_mult : forall a b, (a*b) mod b = 0.
+Proof.
+  intros a b; destruct (Z_eq_dec b 0) as [Hb|Hb].
+  subst; simpl; rewrite ZOmod_0_r; auto with zarith.
+  symmetry; apply ZOmod_unique_full with a; [ red; romega with * | ring ].
+Qed.
+
+Lemma ZO_div_mult : forall a b:Z, b <> 0 -> (a*b)/b = a.
+Proof.
+  intros; symmetry; apply ZOdiv_unique_full with 0; auto with zarith; 
+   [ red; romega with * | ring].
+Qed.
+
+(** * Order results about ZOmod and ZOdiv *)
+
+(* Division of positive numbers is positive. *)
+
+Lemma ZO_div_pos: forall a b, 0 <= a -> 0 <= b -> 0 <= a/b.
+Proof.
+  intros.
+  destruct (Zle_lt_or_eq 0 b H0).
+  assert (H2:=ZOmod_lt_pos_pos a b H H1).
+  rewrite (ZO_div_mod_eq a b) in H.
+  destruct (Z_lt_le_dec (a/b) 0); auto.
+  assert (b*(a/b) <= -b).
+   replace (-b) with (b*-1); [ | ring].
+   apply Zmult_le_compat_l; auto with zarith.
+  romega.
+  subst b; rewrite ZOdiv_0_r; auto.
+Qed.
+
+(** As soon as the divisor is greater or equal than 2, 
+    the division is strictly decreasing. *)
+
+Lemma ZO_div_lt : forall a b:Z, 0 < a -> 2 <= b -> a/b < a.
+Proof.
+  intros. 
+  assert (Hb : 0 < b) by romega.
+  assert (H1 : 0 <= a/b) by (apply ZO_div_pos; auto with zarith).
+  assert (H2 : 0 <= a mod b < b) by (apply ZOmod_lt_pos_pos; auto with zarith).
+  destruct (Zle_lt_or_eq 0 (a/b) H1) as [H3|H3]; [ | rewrite <- H3; auto].
+  pattern a at 2; rewrite (ZO_div_mod_eq a b).
+  apply Zlt_le_trans with (2*(a/b)).
+  romega.
+  apply Zle_trans with (b*(a/b)).
+  apply Zmult_le_compat_r; auto.
+  romega.
+Qed.
+
+(** A division of a small number by a bigger one yields zero. *)
+
+Theorem ZOdiv_small: forall a b, 0 <= a < b -> a/b = 0.
+Proof.
+  intros a b H; apply sym_equal; apply ZOdiv_unique with a; auto with zarith.
+Qed.
+
+(** Same situation, in term of modulo: *)
+
+Theorem ZOmod_small: forall a n, 0 <= a < n -> a mod n = a.
+Proof.
+  intros a b H; apply sym_equal; apply ZOmod_unique with 0; auto with zarith.
+Qed.
+
+(** [Zge] is compatible with a positive division. *)
+
+Lemma ZO_div_monotone_pos : forall a b c:Z, 0<=c -> 0<=a<=b -> a/c <= b/c.
+Proof.
+  intros.
+  destruct H0.
+  destruct (Zle_lt_or_eq 0 c H); 
+   [ clear H | subst c; do 2 rewrite ZOdiv_0_r; auto].
+  generalize (ZO_div_mod_eq a c).
+  generalize (ZOmod_lt_pos_pos a c H0 H2).
+  generalize (ZO_div_mod_eq b c).
+  generalize (ZOmod_lt_pos_pos b c (Zle_trans _ _ _ H0 H1) H2).
+  intros.
+  elim (Z_le_gt_dec (a / c) (b / c)); auto with zarith.
+  intro.
+  absurd (a - b >= 1).
+  omega.
+  replace (a-b) with (c * (a/c-b/c) + a mod c - b mod c) by 
+    (symmetry; pattern a at 1; rewrite H5; pattern b at 1; rewrite H3; ring).
+  assert (c * (a / c - b / c) >= c * 1).
+  apply Zmult_ge_compat_l.
+  omega.
+  omega.
+  assert (c * 1 = c).
+  ring.
+  omega.
+Qed.
+
+Lemma ZO_div_monotone : forall a b c, 0<=c -> a<=b -> a/c <= b/c.
+Proof.
+  intros.
+  destruct (Z_le_gt_dec 0 a).
+  apply ZO_div_monotone_pos; auto with zarith.
+  destruct (Z_le_gt_dec 0 b).
+  apply Zle_trans with 0.
+  apply Zle_left_rev.
+  simpl.
+  rewrite <- ZOdiv_opp_l.
+  apply ZO_div_pos; auto with zarith.
+  apply ZO_div_pos; auto with zarith.
+  rewrite <-(Zopp_involutive a), (ZOdiv_opp_l (-a)).
+  rewrite <-(Zopp_involutive b), (ZOdiv_opp_l (-b)).
+  generalize (ZO_div_monotone_pos (-b) (-a) c H).
+  romega.
+Qed.
+
+(** With our choice of division, rounding of (a/b) is always done toward zero: *)
+
+Lemma ZO_mult_div_le : forall a b:Z, 0 <= a -> 0 <= b*(a/b) <= a.
+Proof.
+  intros a b Ha.
+  destruct b as [ |b|b].
+  simpl; auto with zarith.
+  split.
+  apply Zmult_le_0_compat; auto with zarith.
+  apply ZO_div_pos; auto with zarith.
+  generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_pos_pos a (Zpos b) Ha); romega with *.
+  change (Zneg b) with (-Zpos b); rewrite ZOdiv_opp_r, Zmult_opp_opp.
+  split.
+  apply Zmult_le_0_compat; auto with zarith.
+  apply ZO_div_pos; auto with zarith.
+  generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_pos_pos a (Zpos b) Ha); romega with *.
+Qed.
+
+Lemma ZO_mult_div_ge : forall a b:Z, a <= 0 -> a <= b*(a/b) <= 0.
+Proof.
+  intros a b Ha.
+  destruct b as [ |b|b].
+  simpl; auto with zarith.
+  split.
+  generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_neg_pos a (Zpos b) Ha); romega with *.
+  apply Zle_left_rev; unfold Zplus.
+  rewrite Zopp_mult_distr_r, <-ZOdiv_opp_l.
+  apply Zmult_le_0_compat; auto with zarith.
+  apply ZO_div_pos; auto with zarith.
+  change (Zneg b) with (-Zpos b); rewrite ZOdiv_opp_r, Zmult_opp_opp.
+  split.
+  generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_neg_pos a (Zpos b) Ha); romega with *.
+  apply Zle_left_rev; unfold Zplus.
+  rewrite Zopp_mult_distr_r, <-ZOdiv_opp_l.
+  apply Zmult_le_0_compat; auto with zarith.
+  apply ZO_div_pos; auto with zarith.
+Qed.
+
+(** The previous inequalities between [b*(a/b)] and [a] are exact 
+    iff the modulo is zero. *)
+
+Lemma ZO_div_exact_full_1 : forall a b:Z, a = b*(a/b) -> a mod b = 0.
+Proof.
+  intros; generalize (ZO_div_mod_eq a b); romega.
+Qed.
+
+Lemma ZO_div_exact_full_2 : forall a b:Z, a mod b = 0 -> a = b*(a/b).
+Proof.
+  intros; generalize (ZO_div_mod_eq a b); romega.
+Qed.
+
+(** A modulo cannot grow beyond its starting point. *)
+
+Theorem ZOmod_le: forall a b, 0 <= a -> 0 <= b -> a mod b <= a.
+Proof. 
+  intros a b H1 H2.
+  destruct (Zle_lt_or_eq _ _ H2).
+  case (Zle_or_lt b a); intros H3.
+  case (ZOmod_lt_pos_pos a b); auto with zarith.
+  rewrite ZOmod_small; auto with zarith.
+  subst; rewrite ZOmod_0_r; auto with zarith.
+Qed.
+
+(** Some additionnal inequalities about Zdiv. *)
+
+Theorem ZOdiv_le_upper_bound: 
+  forall a b q, 0 <= a -> 0 < b -> a <= q*b -> a/b <= q.
+Proof.
+  intros a b q H1 H2 H3.
+  apply Zmult_le_reg_r with b; auto with zarith.
+  apply Zle_trans with (2 := H3).
+  pattern a at 2; rewrite (ZO_div_mod_eq a b); auto with zarith.
+  rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b); auto with zarith.
+Qed.
+
+Theorem ZOdiv_lt_upper_bound: 
+  forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q.
+Proof.
+  intros a b q H1 H2 H3.
+  apply Zmult_lt_reg_r with b; auto with zarith.
+  apply Zle_lt_trans with (2 := H3).
+  pattern a at 2; rewrite (ZO_div_mod_eq a b); auto with zarith.
+  rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b); auto with zarith.
+Qed.
+
+Theorem ZOdiv_le_lower_bound: 
+  forall a b q, 0 <= a -> 0 < b -> q*b <= a -> q <= a/b.
+Proof.
+  intros a b q H1 H2 H3.
+  assert (q < a / b + 1); auto with zarith.
+  apply Zmult_lt_reg_r with b; auto with zarith.
+  apply Zle_lt_trans with (1 := H3).
+  pattern a at 1; rewrite (ZO_div_mod_eq a b); auto with zarith.
+  rewrite Zmult_plus_distr_l; rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b);
+   auto with zarith.
+Qed.
+
+Theorem ZOdiv_sgn: forall a b, 
+  0 <= Zsgn (a/b) * Zsgn a * Zsgn b.
+Proof.
+  destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith; 
+  unfold ZOdiv; simpl; destruct Pdiv_eucl; simpl; destruct n; simpl; auto with zarith.
+Qed.
+
+(** * Relations between usual operations and Zmod and Zdiv *)
+
+(** First, a result that used to be always valid with Zdiv, 
+    but must be restricted here. 
+    For instance, now (9+(-5)*2) mod 2 = -1 <> 1 = 9 mod 2 *)
+
+Lemma ZO_mod_plus : forall a b c:Z, 
+ 0 <= (a+b*c) * a -> 
+ (a + b * c) mod c = a mod c.
+Proof.
+  intros; destruct (Z_eq_dec a 0) as [Ha|Ha].
+  subst; simpl; rewrite ZOmod_0_l; apply ZO_mod_mult.
+  intros; destruct (Z_eq_dec c 0) as [Hc|Hc].
+  subst; do 2 rewrite ZOmod_0_r; romega.
+  symmetry; apply ZOmod_unique_full with (a/c+b); auto with zarith.
+  rewrite Remainder_equiv; split.
+  apply ZOmod_lt; auto.
+  apply Zmult_le_0_reg_r with (a*a); eauto.
+  destruct a; simpl; auto with zarith.
+  replace ((a mod c)*(a+b*c)*(a*a)) with (((a mod c)*a)*((a+b*c)*a)) by ring.
+  apply Zmult_le_0_compat; auto.
+  apply ZOmod_sgn2.
+  rewrite Zmult_plus_distr_r, Zmult_comm.
+  generalize (ZO_div_mod_eq a c); romega.
+Qed.
+
+Lemma ZO_div_plus : forall a b c:Z, 
+ 0 <= (a+b*c) * a -> c<>0 -> 
+ (a + b * c) / c = a / c + b.
+Proof.
+  intros; destruct (Z_eq_dec a 0) as [Ha|Ha].
+  subst; simpl; apply ZO_div_mult; auto.
+  symmetry.
+  apply ZOdiv_unique_full with (a mod c); auto with zarith.
+  rewrite Remainder_equiv; split.
+  apply ZOmod_lt; auto.
+  apply Zmult_le_0_reg_r with (a*a); eauto.
+  destruct a; simpl; auto with zarith.
+  replace ((a mod c)*(a+b*c)*(a*a)) with (((a mod c)*a)*((a+b*c)*a)) by ring.
+  apply Zmult_le_0_compat; auto.
+  apply ZOmod_sgn2.
+  rewrite Zmult_plus_distr_r, Zmult_comm.
+  generalize (ZO_div_mod_eq a c); romega.
+Qed.
+
+Theorem ZO_div_plus_l: forall a b c : Z, 
+ 0 <= (a*b+c)*c -> b<>0 -> 
+ b<>0 -> (a * b + c) / b = a + c / b.
+Proof.
+  intros a b c; rewrite Zplus_comm; intros; rewrite ZO_div_plus;
+  try apply Zplus_comm; auto with zarith. 
+Qed.
+
+(** Cancellations. *)
+
+Lemma ZOdiv_mult_cancel_r : forall a b c:Z, 
+ c<>0 -> (a*c)/(b*c) = a/b.
+Proof.
+ intros a b c Hc.
+ destruct (Z_eq_dec b 0).
+ subst; simpl; do 2 rewrite ZOdiv_0_r; auto.
+ symmetry.
+ apply ZOdiv_unique_full with ((a mod b)*c); auto with zarith.
+ rewrite Remainder_equiv.
+ split.
+ do 2 rewrite Zabs_Zmult.
+ apply Zmult_lt_compat_r.
+ romega with *.
+ apply ZOmod_lt; auto.
+ replace ((a mod b)*c*(a*c)) with (((a mod b)*a)*(c*c)) by ring.
+ apply Zmult_le_0_compat.
+ apply ZOmod_sgn2.
+ destruct c; simpl; auto with zarith.
+ pattern a at 1; rewrite (ZO_div_mod_eq a b); ring.
+Qed.
+
+Lemma ZOdiv_mult_cancel_l : forall a b c:Z, 
+ c<>0 -> (c*a)/(c*b) = a/b.
+Proof.
+  intros.
+  rewrite (Zmult_comm c a); rewrite (Zmult_comm c b).
+  apply ZOdiv_mult_cancel_r; auto.
+Qed.
+
+Lemma ZOmult_mod_distr_l: forall a b c, 
+  (c*a) mod (c*b) = c * (a mod b).
+Proof.
+  intros; destruct (Z_eq_dec c 0) as [Hc|Hc].
+  subst; simpl; rewrite ZOmod_0_r; auto.
+  destruct (Z_eq_dec b 0) as [Hb|Hb].
+  subst; repeat rewrite Zmult_0_r || rewrite ZOmod_0_r; auto.
+  assert (c*b <> 0).
+   contradict Hc; eapply Zmult_integral_l; eauto.
+  rewrite (Zplus_minus_eq _ _ _ (ZO_div_mod_eq (c*a) (c*b))).
+  rewrite (Zplus_minus_eq _ _ _ (ZO_div_mod_eq a b)).
+  rewrite ZOdiv_mult_cancel_l; auto with zarith.
+  ring.
+Qed.
+
+Lemma ZOmult_mod_distr_r: forall a b c, 
+  (a*c) mod (b*c) = (a mod b) * c.
+Proof.
+  intros; repeat rewrite (fun x => (Zmult_comm x c)).
+  apply ZOmult_mod_distr_l; auto.
+Qed.
+
+(** Operations modulo. *)
+
+Theorem ZOmod_mod: forall a n, (a mod n) mod n = a mod n.
+Proof.
+  intros.
+  generalize (ZOmod_sgn2 a n).
+  pattern a at 2 4; rewrite (ZO_div_mod_eq a n); auto with zarith.
+  rewrite Zplus_comm; rewrite (Zmult_comm n).
+  intros.
+  apply sym_equal; apply ZO_mod_plus; auto with zarith.
+  rewrite Zmult_comm; auto.
+Qed.
+
+Theorem ZOmult_mod: forall a b n,
+ (a * b) mod n = ((a mod n) * (b mod n)) mod n.
+Proof.
+  intros.
+  generalize (Zmult_le_0_compat _ _ (ZOmod_sgn2 a n) (ZOmod_sgn2 b n)).
+  pattern a at 2 3; rewrite (ZO_div_mod_eq a n); auto with zarith.
+  pattern b at 2 3; rewrite (ZO_div_mod_eq b n); auto with zarith.
+  set (A:=a mod n); set (B:=b mod n); set (A':=a/n); set (B':=b/n).
+  replace (A*(n*A'+A)*(B*(n*B'+B))) with (((n*A' + A) * (n*B' + B))*(A*B)) 
+   by ring.
+  replace ((n*A' + A) * (n*B' + B))
+   with (A*B + (A'*B+B'*A+n*A'*B')*n) by ring.
+  intros.
+  apply ZO_mod_plus; auto with zarith.
+Qed.
+
+(** addition and modulo
+  
+  Generally speaking, unlike with Zdiv, we don't have 
+       (a+b) mod n = (a mod n + b mod n) mod n 
+  for any a and b. 
+  For instance, take (8 + (-10)) mod 3 = -2 whereas 
+  (8 mod 3 + (-10 mod 3)) mod 3 = 1. *)
+
+Theorem ZOplus_mod: forall a b n,
+ 0 <= a * b -> 
+ (a + b) mod n = (a mod n + b mod n) mod n.
+Proof.
+  assert (forall a b n, 0<a -> 0<b ->
+           (a + b) mod n = (a mod n + b mod n) mod n).
+  intros a b n Ha Hb.
+  assert (H : 0<=a+b) by (romega with * ); revert H.
+  pattern a at 1 2; rewrite (ZO_div_mod_eq a n); auto with zarith.
+  pattern b at 1 2; rewrite (ZO_div_mod_eq b n); auto with zarith.
+  replace ((n * (a / n) + a mod n) + (n * (b / n) + b mod n))
+     with ((a mod n + b mod n) + (a / n + b / n) * n) by ring.
+  intros.
+  apply ZO_mod_plus; auto with zarith.
+  apply Zmult_le_0_compat; auto with zarith.
+  apply Zplus_le_0_compat.
+  apply Zmult_le_reg_r with a; auto with zarith.
+  simpl; apply ZOmod_sgn2; auto.
+  apply Zmult_le_reg_r with b; auto with zarith.
+  simpl; apply ZOmod_sgn2; auto.
+  (* general situation *)
+  intros a b n Hab.
+  destruct (Z_eq_dec a 0).
+  subst; simpl; symmetry; apply ZOmod_mod.
+  destruct (Z_eq_dec b 0).
+  subst; simpl; do 2 rewrite Zplus_0_r; symmetry; apply ZOmod_mod.
+  assert (0<a /\ 0<b \/ a<0 /\ b<0).
+   destruct a; destruct b; simpl in *; intuition; romega with *.
+  destruct H0.
+  apply H; intuition.
+  rewrite <-(Zopp_involutive a), <-(Zopp_involutive b).
+  rewrite <- Zopp_plus_distr; rewrite ZOmod_opp_l.
+  rewrite (ZOmod_opp_l (-a)),(ZOmod_opp_l (-b)).
+  match goal with |- _ = (-?x+-?y) mod n => 
+   rewrite <-(Zopp_plus_distr x y), ZOmod_opp_l end.
+  f_equal; apply H; auto with zarith.
+Qed.
+
+Lemma ZOplus_mod_idemp_l: forall a b n, 
+ 0 <= a * b -> 
+ (a mod n + b) mod n = (a + b) mod n.
+Proof.
+  intros. 
+  rewrite ZOplus_mod.
+  rewrite ZOmod_mod.
+  symmetry.
+  apply ZOplus_mod; auto.
+  destruct (Z_eq_dec a 0).
+  subst; rewrite ZOmod_0_l; auto.
+  destruct (Z_eq_dec b 0).
+  subst; rewrite Zmult_0_r; auto with zarith.
+  apply Zmult_le_reg_r with (a*b).
+  assert (a*b <> 0).
+   intro Hab.
+   rewrite (Zmult_integral_l _ _ n1 Hab) in n0; auto with zarith.
+  auto with zarith.
+  simpl.
+  replace (a mod n * b * (a*b)) with ((a mod n * a)*(b*b)) by ring.
+  apply Zmult_le_0_compat.
+  apply ZOmod_sgn2.
+  destruct b; simpl; auto with zarith.
+Qed.
+
+Lemma ZOplus_mod_idemp_r: forall a b n, 
+ 0 <= a*b -> 
+ (b + a mod n) mod n = (b + a) mod n.
+Proof.
+  intros.
+  rewrite Zplus_comm, (Zplus_comm b a).
+  apply ZOplus_mod_idemp_l; auto.
+Qed.
+
+Lemma ZOmult_mod_idemp_l: forall a b n, (a mod n * b) mod n = (a * b) mod n.
+Proof.
+  intros; rewrite ZOmult_mod, ZOmod_mod, <- ZOmult_mod; auto.
+Qed.
+
+Lemma ZOmult_mod_idemp_r: forall a b n, (b * (a mod n)) mod n = (b * a) mod n.
+Proof.
+  intros; rewrite ZOmult_mod, ZOmod_mod, <- ZOmult_mod; auto.
+Qed.
+
+(** Unlike with Zdiv, the following result is true without restrictions. *)
+
+Lemma ZOdiv_ZOdiv : forall a b c, (a/b)/c = a/(b*c).
+Proof.
+  (* particular case: a, b, c positive *)
+  assert (forall a b c, a>0 -> b>0 -> c>0 -> (a/b)/c = a/(b*c)).
+   intros a b c H H0 H1.
+   pattern a at 2;rewrite (ZO_div_mod_eq a b).
+   pattern (a/b) at 2;rewrite (ZO_div_mod_eq (a/b) c).
+   replace (b * (c * (a / b / c) + (a / b) mod c) + a mod b) with
+    ((a / b / c)*(b * c)  + (b * ((a / b) mod c) + a mod b)) by ring.
+   assert (b*c<>0).
+    intro H2; 
+    assert (H3: c <> 0) by auto with zarith; 
+    rewrite (Zmult_integral_l _ _ H3 H2) in H0; auto with zarith.
+   assert (0<=a/b) by (apply (ZO_div_pos a b); auto with zarith).
+   assert (0<=a mod b < b) by (apply ZOmod_lt_pos_pos; auto with zarith).
+   assert (0<=(a/b) mod c < c) by 
+    (apply ZOmod_lt_pos_pos; auto with zarith).
+   rewrite ZO_div_plus_l; auto with zarith.
+   rewrite (ZOdiv_small (b * ((a / b) mod c) + a mod b)).
+   ring.
+   split.
+   apply Zplus_le_0_compat;auto with zarith.
+   apply Zle_lt_trans with (b * ((a / b) mod c) + (b-1)).
+   apply Zplus_le_compat;auto with zarith.
+   apply Zle_lt_trans with (b * (c-1) + (b - 1)).
+   apply Zplus_le_compat;auto with zarith.
+   replace (b * (c - 1) + (b - 1)) with (b*c-1);try ring;auto with zarith.
+   repeat (apply Zmult_le_0_compat || apply Zplus_le_0_compat); auto with zarith.
+   apply (ZO_div_pos (a/b) c); auto with zarith.
+  (* b c positive, a general *)
+  assert (forall a b c, b>0 -> c>0 -> (a/b)/c = a/(b*c)).
+   intros; destruct a as [ |a|a]; try reflexivity.
+   apply H; auto with zarith.
+   change (Zneg a) with (-Zpos a); repeat rewrite ZOdiv_opp_l.
+   f_equal; apply H; auto with zarith.
+  (* c positive, a b general *)
+  assert (forall a b c, c>0 -> (a/b)/c = a/(b*c)).
+   intros; destruct b as [ |b|b].
+   repeat rewrite ZOdiv_0_r; reflexivity.
+   apply H0; auto with zarith.
+   change (Zneg b) with (-Zpos b); 
+   repeat (rewrite ZOdiv_opp_r || rewrite ZOdiv_opp_l || rewrite <- Zopp_mult_distr_l).
+   f_equal; apply H0; auto with zarith.
+  (* a b c general *)
+  intros; destruct c as [ |c|c].
+  rewrite Zmult_0_r; repeat rewrite ZOdiv_0_r; reflexivity.
+  apply H1; auto with zarith.
+  change (Zneg c) with (-Zpos c); 
+  rewrite <- Zopp_mult_distr_r; do 2 rewrite ZOdiv_opp_r.
+  f_equal; apply H1; auto with zarith.
+Qed.
+
+(** A last inequality: *)
+
+Theorem ZOdiv_mult_le:
+ forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b.
+Proof.
+  intros a b c Ha Hb Hc.
+  destruct (Zle_lt_or_eq _ _ Ha); 
+   [ | subst; rewrite ZOdiv_0_l, Zmult_0_r, ZOdiv_0_l; auto].
+  destruct (Zle_lt_or_eq _ _ Hb); 
+   [ | subst; rewrite ZOdiv_0_r, ZOdiv_0_r, Zmult_0_r; auto].
+  destruct (Zle_lt_or_eq _ _ Hc); 
+   [ | subst; rewrite ZOdiv_0_l; auto].
+  case (ZOmod_lt_pos_pos a b); auto with zarith; intros Hu1 Hu2.
+  case (ZOmod_lt_pos_pos c b); auto with zarith; intros Hv1 Hv2.
+  apply Zmult_le_reg_r with b; auto with zarith.
+  rewrite <- Zmult_assoc.
+  replace (a / b * b) with (a - a mod b).
+  replace (c * a / b * b) with (c * a - (c * a) mod b).
+  rewrite Zmult_minus_distr_l.
+  unfold Zminus; apply Zplus_le_compat_l.
+  match goal with |- - ?X <= -?Y => assert (Y <= X); auto with zarith end.
+  apply Zle_trans with ((c mod b) * (a mod b)); auto with zarith.
+  rewrite ZOmult_mod; auto with zarith.
+  apply (ZOmod_le ((c mod b) * (a mod b)) b); auto with zarith.
+  apply Zmult_le_compat_r; auto with zarith.
+  apply (ZOmod_le c b); auto.
+  pattern (c * a) at 1; rewrite (ZO_div_mod_eq (c * a) b); try ring; 
+    auto with zarith.
+  pattern a at 1; rewrite (ZO_div_mod_eq a b); try ring; auto with zarith.
+Qed.
+
+(** ZOmod is related to divisibility (see more in Znumtheory) *)
+
+Lemma ZOmod_divides : forall a b, 
+ a mod b = 0 <-> exists c, a = b*c.
+Proof.
+ split; intros.
+ exists (a/b).
+ pattern a at 1; rewrite (ZO_div_mod_eq a b).
+ rewrite H; auto with zarith.
+ destruct H as [c Hc].
+ destruct (Z_eq_dec b 0).
+ subst b; simpl in *; subst a; auto.
+ symmetry.
+ apply ZOmod_unique_full with c; auto with zarith.
+ red; romega with *.
+Qed.
+
+(** * Interaction with "historic" Zdiv *)
+
+(** They agree at least on positive numbers: *)
+
+Theorem ZOdiv_eucl_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b -> 
+  a/b = Zdiv.Zdiv a b /\ a mod b = Zdiv.Zmod a b.
+Proof.
+  intros.
+  apply Zdiv.Zdiv_mod_unique with b.
+  apply ZOmod_lt_pos; auto with zarith.
+  rewrite Zabs_eq; auto with *; apply Zdiv.Z_mod_lt; auto with *.
+  rewrite <- Zdiv.Z_div_mod_eq; auto with *.
+  symmetry; apply ZO_div_mod_eq; auto with *.
+Qed.
+
+Theorem ZOdiv_Zdiv_pos : forall a b, 0 <= a -> 0 <= b -> 
+  a/b = Zdiv.Zdiv a b.
+Proof.
+ intros a b Ha Hb.
+ destruct (Zle_lt_or_eq _ _ Hb).
+ generalize (ZOdiv_eucl_Zdiv_eucl_pos a b Ha H); intuition.
+ subst; rewrite ZOdiv_0_r, Zdiv.Zdiv_0_r; reflexivity.
+Qed.
+
+Theorem ZOmod_Zmod_pos : forall a b, 0 <= a -> 0 < b -> 
+  a mod b = Zdiv.Zmod a b.
+Proof.
+ intros a b Ha Hb; generalize (ZOdiv_eucl_Zdiv_eucl_pos a b Ha Hb);
+ intuition.
+Qed.
+
+(** Modulos are null at the same places *)
+
+Theorem ZOmod_Zmod_zero : forall a b, b<>0 -> 
+ (a mod b = 0 <-> Zdiv.Zmod a b = 0).
+Proof.
+ intros.
+ rewrite ZOmod_divides, Zdiv.Zmod_divides; intuition.
+Qed. 
diff --git a/theories/ZArith/ZOdiv_def.v b/theories/ZArith/ZOdiv_def.v
new file mode 100644
index 00000000..2c84765e
--- /dev/null
+++ b/theories/ZArith/ZOdiv_def.v
@@ -0,0 +1,136 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+
+Require Import BinPos BinNat Nnat ZArith_base.
+
+Open Scope Z_scope.
+
+Definition NPgeb (a:N)(b:positive) :=
+  match a with
+   | N0 => false
+   | Npos na => match Pcompare na b Eq with Lt => false | _ => true end
+  end.
+
+Fixpoint Pdiv_eucl (a b:positive) {struct a} : N * N :=
+  match a with
+    | xH => 
+       match b with xH => (1, 0)%N | _ => (0, 1)%N end
+    | xO a' =>
+       let (q, r) := Pdiv_eucl a' b in
+       let r' := (2 * r)%N in
+        if (NPgeb r' b) then (2 * q + 1, (Nminus r'  (Npos b)))%N
+        else  (2 * q, r')%N
+    | xI a' =>
+       let (q, r) := Pdiv_eucl a' b in
+       let r' := (2 * r + 1)%N in
+        if (NPgeb r' b) then (2 * q + 1, (Nminus r' (Npos b)))%N
+        else  (2 * q, r')%N
+  end.
+
+Definition ZOdiv_eucl (a b:Z) : Z * Z := 
+  match a, b with
+   | Z0,  _ => (Z0, Z0)
+   | _, Z0  => (Z0, a)
+   | Zpos na, Zpos nb => 
+         let (nq, nr) := Pdiv_eucl na nb in 
+         (Z_of_N nq, Z_of_N nr)
+   | Zneg na, Zpos nb => 
+         let (nq, nr) := Pdiv_eucl na nb in 
+         (Zopp (Z_of_N nq), Zopp (Z_of_N nr))
+   | Zpos na, Zneg nb => 
+         let (nq, nr) := Pdiv_eucl na nb in 
+         (Zopp (Z_of_N nq), Z_of_N nr)
+   | Zneg na, Zneg nb => 
+         let (nq, nr) := Pdiv_eucl na nb in 
+         (Z_of_N nq, Zopp (Z_of_N nr))
+  end.
+
+Definition ZOdiv a b := fst (ZOdiv_eucl a b).
+Definition ZOmod a b := snd (ZOdiv_eucl a b).
+
+
+Definition Ndiv_eucl (a b:N) : N * N := 
+  match a, b with
+   | N0,  _ => (N0, N0)
+   | _, N0  => (N0, a)
+   | Npos na, Npos nb => Pdiv_eucl na nb
+  end.
+
+Definition Ndiv a b := fst (Ndiv_eucl a b).
+Definition Nmod a b := snd (Ndiv_eucl a b).
+
+
+(* Proofs of specifications for these euclidean divisions. *)
+
+Theorem NPgeb_correct: forall (a:N)(b:positive), 
+  if NPgeb a b then a = (Nminus a (Npos b) + Npos b)%N else True.
+Proof.
+  destruct a; intros; simpl; auto.
+  generalize (Pcompare_Eq_eq p b).
+  case_eq (Pcompare p b Eq); intros; auto.
+  rewrite H0; auto. 
+  now rewrite Pminus_mask_diag.
+  destruct (Pminus_mask_Gt p b H) as [d [H2 [H3 _]]].
+  rewrite H2. rewrite <- H3.
+  simpl; f_equal; apply Pplus_comm.
+Qed.
+
+Hint Rewrite Z_of_N_plus Z_of_N_mult Z_of_N_minus Zmult_1_l Zmult_assoc
+ Zmult_plus_distr_l Zmult_plus_distr_r : zdiv. 
+Hint Rewrite <- Zplus_assoc : zdiv. 
+
+Theorem Pdiv_eucl_correct: forall a b,
+  let (q,r) := Pdiv_eucl a b in 
+  Zpos a = Z_of_N q * Zpos b + Z_of_N r.
+Proof.
+  induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta.
+  intros b; generalize (IHa b); case Pdiv_eucl.
+    intros q1 r1 Hq1.
+     generalize (NPgeb_correct (2 * r1 + 1) b); case NPgeb; intros H.
+     set (u := Nminus (2 * r1 + 1) (Npos b)) in * |- *.
+     assert (HH: Z_of_N u = (Z_of_N (2 * r1 + 1) - Zpos b)%Z).
+        rewrite H; autorewrite with zdiv; simpl.
+        rewrite Zplus_comm, Zminus_plus; trivial.
+     rewrite HH; autorewrite with zdiv; simpl Z_of_N.
+     rewrite Zpos_xI, Hq1.
+     autorewrite with zdiv; f_equal; rewrite Zplus_minus; trivial.
+     rewrite Zpos_xI, Hq1; autorewrite with zdiv; auto.
+  intros b; generalize (IHa b); case Pdiv_eucl.
+    intros q1 r1 Hq1.
+     generalize (NPgeb_correct (2 * r1) b); case NPgeb; intros H.
+     set (u := Nminus (2 * r1) (Npos b)) in * |- *.
+     assert (HH: Z_of_N u = (Z_of_N (2 * r1) - Zpos b)%Z).
+        rewrite H; autorewrite with zdiv; simpl.
+        rewrite Zplus_comm, Zminus_plus; trivial.
+     rewrite HH; autorewrite with zdiv; simpl Z_of_N.
+     rewrite Zpos_xO, Hq1.
+     autorewrite with zdiv; f_equal; rewrite Zplus_minus; trivial.
+     rewrite Zpos_xO, Hq1; autorewrite with zdiv; auto.
+  destruct b; auto.
+Qed.
+
+Theorem ZOdiv_eucl_correct: forall a b,
+  let (q,r) := ZOdiv_eucl a b in a = q * b + r.
+Proof.
+  destruct a; destruct b; simpl; auto;
+  generalize (Pdiv_eucl_correct p p0); case Pdiv_eucl; auto; intros;
+  try change (Zneg p) with (Zopp (Zpos p)); rewrite H.
+    destruct n; auto.
+  repeat (rewrite Zopp_plus_distr || rewrite Zopp_mult_distr_l); trivial.
+  repeat (rewrite Zopp_plus_distr || rewrite Zopp_mult_distr_r); trivial.
+Qed.
+
+Theorem Ndiv_eucl_correct: forall a b,
+  let (q,r) := Ndiv_eucl a b in a = (q * b + r)%N.
+Proof.
+  destruct a; destruct b; simpl; auto;
+  generalize (Pdiv_eucl_correct p p0); case Pdiv_eucl; auto; intros;
+  destruct n; destruct n0; simpl; simpl in H; try discriminate;
+  injection H; intros; subst; trivial.
+Qed.
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index ed641358..c15493e3 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -5,14 +5,16 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*i $Id: Zabs.v 9302 2006-10-27 21:21:17Z barras $ i*)
+(*i $Id: Zabs.v 10302 2007-11-08 09:54:31Z letouzey $ i*)
 
-(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
 
 Require Import Arith_base.
 Require Import BinPos.
 Require Import BinInt.
 Require Import Zorder.
+Require Import Zmax.
+Require Import Znat.
 Require Import ZArith_dec.
 
 Open Local Scope Z_scope.
@@ -63,6 +65,11 @@ Lemma Zabs_pos : forall n:Z, 0 <= Zabs n.
   intro x; destruct x; auto with arith; compute in |- *; intros H; inversion H.
 Qed.
 
+Lemma Zabs_involutive : forall x:Z, Zabs (Zabs x) = Zabs x.
+Proof.
+  intros; apply Zabs_eq; apply Zabs_pos.
+Qed.
+
 Theorem Zabs_eq_case : forall n m:Z, Zabs n = Zabs m -> n = m \/ n = - m.
 Proof.
   intros z1 z2; case z1; case z2; simpl in |- *; auto;
@@ -70,6 +77,13 @@ Proof.
       (intros H2; rewrite H2); auto.
 Qed.
 
+Lemma Zabs_spec : forall x:Z, 
+  0 <= x /\ Zabs x = x \/ 
+  0 > x /\ Zabs x = -x. 
+Proof.
+ intros; unfold Zabs, Zle, Zgt; destruct x; simpl; intuition discriminate.
+Qed.
+
 (** * Triangular inequality *)
 
 Hint Local Resolve Zle_neg_pos: zarith.
@@ -106,25 +120,106 @@ Proof.
   intros z1 z2; case z1; case z2; simpl in |- *; auto.
 Qed.
 
-(** * Absolute value in nat is compatible with order *)
+Theorem Zabs_square : forall a, Zabs a * Zabs a = a * a.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+(** * Results about absolute value in nat. *)
+
+Theorem inj_Zabs_nat : forall z:Z, Z_of_nat (Zabs_nat z) = Zabs z.
+Proof.
+  destruct z; simpl; auto; symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P.
+Qed.
+
+Theorem Zabs_nat_Z_of_nat: forall n, Zabs_nat (Z_of_nat n) = n.
+Proof.
+  destruct n; simpl; auto.
+  apply nat_of_P_o_P_of_succ_nat_eq_succ.
+Qed.
+
+Lemma Zabs_nat_mult: forall n m:Z, Zabs_nat (n*m) = (Zabs_nat n * Zabs_nat m)%nat.
+Proof.
+  intros; apply inj_eq_rev.
+  rewrite inj_mult; repeat rewrite inj_Zabs_nat; apply Zabs_Zmult.
+Qed. 
+
+Lemma Zabs_nat_Zsucc:
+ forall p, 0 <= p ->  Zabs_nat (Zsucc p) = S (Zabs_nat p).
+Proof.
+  intros; apply inj_eq_rev.
+  rewrite inj_S; repeat rewrite inj_Zabs_nat, Zabs_eq; auto with zarith.
+Qed.
+
+Lemma Zabs_nat_Zplus: 
+ forall x y, 0<=x -> 0<=y -> Zabs_nat (x+y) = (Zabs_nat x + Zabs_nat y)%nat.
+Proof.
+  intros; apply inj_eq_rev.
+  rewrite inj_plus; repeat rewrite inj_Zabs_nat, Zabs_eq; auto with zarith.
+  apply Zplus_le_0_compat; auto.
+Qed.  
+
+Lemma Zabs_nat_Zminus:
+ forall x y, 0 <= x <= y ->  Zabs_nat (y - x) = (Zabs_nat y - Zabs_nat x)%nat.
+Proof.
+  intros x y (H,H').
+  assert (0 <= y) by (apply Zle_trans with x; auto).
+  assert (0 <= y-x) by (apply Zle_minus_le_0; auto).
+  apply inj_eq_rev.
+  rewrite inj_minus; repeat rewrite inj_Zabs_nat, Zabs_eq; auto.
+  rewrite Zmax_right; auto.
+Qed.
+
+Lemma Zabs_nat_le :
+  forall n m:Z, 0 <= n <= m -> (Zabs_nat n <= Zabs_nat m)%nat.
+Proof.
+  intros n m (H,H'); apply inj_le_rev.
+  repeat rewrite inj_Zabs_nat, Zabs_eq; auto.
+  apply Zle_trans with n; auto.
+Qed.
 
 Lemma Zabs_nat_lt :
-  forall n m:Z, 0 <= n /\ n < m -> (Zabs_nat n < Zabs_nat m)%nat.
+  forall n m:Z, 0 <= n < m -> (Zabs_nat n < Zabs_nat m)%nat.
+Proof.
+  intros n m (H,H'); apply inj_lt_rev.
+  repeat rewrite inj_Zabs_nat, Zabs_eq; auto.
+  apply Zlt_le_weak; apply Zle_lt_trans with n; auto.
+Qed.
+
+(** * Some results about the sign function. *)
+
+Lemma Zsgn_Zmult : forall a b, Zsgn (a*b) = Zsgn a * Zsgn b.
+Proof.
+  destruct a; destruct b; simpl; auto.
+Qed.
+
+Lemma Zsgn_Zopp : forall a, Zsgn (-a) = - Zsgn a.
 Proof.
-  intros x y. case x; simpl in |- *. case y; simpl in |- *.
+  destruct a; simpl; auto.
+Qed.
 
-  intro. absurd (0 < 0). compute in |- *. 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 in |- *.
-  intros. absurd (Zpos p < 0). compute in |- *. intro H0. discriminate H0. intuition.
-  intros. change (nat_of_P p > nat_of_P p0)%nat in |- *.
-  apply nat_of_P_gt_Gt_compare_morphism.
-  elim H; auto with arith. intro. exact (ZC2 p0 p).
+(** A characterization of the sign function: *)
 
-  intros. absurd (Zpos p0 < Zneg p).
-  compute in |- *. intro H0. discriminate H0. intuition.
+Lemma Zsgn_spec : forall x:Z, 
+  0 < x /\ Zsgn x = 1 \/ 
+  0 = x /\ Zsgn x = 0 \/ 
+  0 > x /\ Zsgn x = -1.
+Proof. 
+ intros; unfold Zsgn, Zle, Zgt; destruct x; compute; intuition.
+Qed.
 
-  intros. absurd (0 <= Zneg p). compute in |- *. auto with arith. intuition.
+Lemma Zsgn_pos : forall x:Z, Zsgn x = 1 <-> 0 < x.
+Proof.
+ destruct x; now intuition.
 Qed.
+
+Lemma Zsgn_neg : forall x:Z, Zsgn x = -1 <-> x < 0.
+Proof.
+ destruct x; now intuition.
+Qed.
+
+Lemma Zsgn_null : forall x:Z, Zsgn x = 0 <-> x = 0.
+Proof.
+ destruct x; now intuition.
+Qed.
+
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index 7da91c44..34114d46 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Zbool.v 9245 2006-10-17 12:53:34Z notin $ *)
+(* $Id: Zbool.v 10063 2007-08-08 14:21:03Z emakarov $ *)
 
 Require Import BinInt.
 Require Import Zeven.
@@ -104,7 +104,7 @@ Qed.
 
 Lemma Zle_bool_imp_le : forall n m:Z, Zle_bool n m = true -> (n <= m)%Z.
 Proof.
-  unfold Zle_bool, Zle in |- *. intros x y. unfold not in |- *. 
+  unfold Zle_bool, Zle in |- *. intros x y. unfold not in |- *.
   case (x ?= y)%Z; intros; discriminate.
 Qed.
 
@@ -178,6 +178,18 @@ Proof.
   intro. apply Zle_ge. apply Zle_bool_imp_le. assumption.
 Qed.
 
+Lemma Zlt_is_lt_bool : forall n m:Z, (n < m)%Z <-> Zlt_bool n m = true.
+Proof.
+intros n m; unfold Zlt_bool, Zlt.
+destruct (n ?= m)%Z; simpl; split; now intro.
+Qed.
+
+Lemma Zgt_is_gt_bool : forall n m:Z, (n > m)%Z <-> Zgt_bool n m = true.
+Proof.
+intros n m; unfold Zgt_bool, Zgt.
+destruct (n ?= m)%Z; simpl; split; now intro.
+Qed.
+
 Lemma Zlt_is_le_bool :
   forall n m:Z, (n < m)%Z <-> Zle_bool n (m - 1) = true.
 Proof.
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 78c8a976..c6ade934 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Zcomplements.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Zcomplements.v 10617 2008-03-04 18:07:16Z letouzey $ i*)
 
 Require Import ZArithRing.
 Require Import ZArith_base.
-Require Import Omega.
+Require Export Omega.
 Require Import Wf_nat.
 Open Local Scope Z_scope.
 
@@ -160,7 +160,7 @@ Qed.
 
 Require Import List.
 
-Fixpoint Zlength_aux (acc:Z) (A:Set) (l:list A) {struct l} : Z :=
+Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) {struct l} : Z :=
   match l with
     | nil => acc
     | _ :: l => Zlength_aux (Zsucc acc) A l
@@ -171,7 +171,7 @@ Implicit Arguments Zlength [A].
 
 Section Zlength_properties.
 
-  Variable A : Set.
+  Variable A : Type.
 
   Implicit Type l : list A.
 
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 31f68207..4c560c6b 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Zdiv.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Zdiv.v 10999 2008-05-27 15:55:22Z letouzey $ i*)
 
-(* Contribution by Claude Marché and Xavier Urbain *)
+(* Contribution by Claude Marché and Xavier Urbain *)
 
 (** Euclidean Division
 
@@ -21,6 +21,7 @@ Require Import Zbool.
 Require Import Omega.
 Require Import ZArithRing.
 Require Import Zcomplements.
+Require Export Setoid.
 Open Local Scope Z_scope.
 
 (** * Definitions of Euclidian operations *)
@@ -70,8 +71,21 @@ Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} :
                        if r = 0 then (-q,0) else (-(q+1),b+r)
 
   In other word, when b is non-zero, q is chosen to be the greatest integer 
-  smaller or equal to a/b. And sgn(r)=sgn(b) and |r| < |b|.
+  smaller or equal to a/b. And sgn(r)=sgn(b) and |r| < |b| (at least when 
+  r is not null). 
+*)
+
+(* Nota: At least two others conventions also exist for euclidean division.
+   They all satify the equation a=b*q+r, but differ on the choice of (q,r) 
+   on negative numbers.
+
+   * Ocaml uses Round-Toward-Zero division: (-a)/b = a/(-b) = -(a/b).
+     Hence (-a) mod b = - (a mod b)
+           a mod (-b) = a mod b
+     And: |r| < |b| and sgn(r) = sgn(a)  (notice the a here instead of b). 
 
+   * Another solution is to always pick a non-negative remainder: 
+     a=b*q+r with 0 <= r < |b|
 *)
 
 Definition Zdiv_eucl (a b:Z) : Z * Z :=
@@ -96,7 +110,7 @@ Definition Zdiv_eucl (a b:Z) : Z * Z :=
 
 
 (** Division and modulo are projections of [Zdiv_eucl] *)
-     
+
 Definition Zdiv (a b:Z) : Z := let (q, _) := Zdiv_eucl a b in q.
 
 Definition Zmod (a b:Z) : Z := let (_, r) := Zdiv_eucl a b in r. 
@@ -108,20 +122,20 @@ Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
 
 (* Tests:
 
-Eval Compute in `(Zdiv_eucl 7 3)`. 
+Eval compute in (Zdiv_eucl 7 3). 
 
-Eval Compute in `(Zdiv_eucl (-7) 3)`.
+Eval compute in (Zdiv_eucl (-7) 3).
 
-Eval Compute in `(Zdiv_eucl 7 (-3))`.
+Eval compute in (Zdiv_eucl 7 (-3)).
 
-Eval Compute in `(Zdiv_eucl (-7) (-3))`.
+Eval compute in (Zdiv_eucl (-7) (-3)).
 
 *)
 
 
 (** * Main division theorem *) 
 
-(** First a lemma for positive *)
+(** First a lemma for two positive arguments *)
 
 Lemma Z_div_mod_POS :
   forall b:Z,
@@ -129,7 +143,8 @@ Lemma Z_div_mod_POS :
     forall a:positive,
       let (q, r) := Zdiv_eucl_POS a b in Zpos a = b * q + r /\ 0 <= r < b.
 Proof.
-simple induction a; unfold Zdiv_eucl_POS in |- *; fold Zdiv_eucl_POS in |- *.
+simple induction a; cbv beta iota delta [Zdiv_eucl_POS] in |- *;
+  fold Zdiv_eucl_POS in |- *; cbv zeta.
 
 intro p; case (Zdiv_eucl_POS p b); intros q r [H0 H1].
 generalize (Zgt_cases b (2 * r + 1)).
@@ -147,6 +162,7 @@ case (Zge_bool b 2); (intros; split; [ try ring | omega ]).
 omega.
 Qed.
 
+(** Then the usual situation of a positive [b] and no restriction on [a] *)
 
 Theorem Z_div_mod :
   forall a b:Z,
@@ -166,27 +182,131 @@ Proof.
   
   intros [H1 H2].
   split; trivial.
-  replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ].
+  change (Zneg p0) with (- Zpos p0); rewrite H1; ring.
   
   intros p1 [H1 H2].
   split; trivial.
-  replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ].
+  change (Zneg p0) with (- Zpos p0); rewrite H1; ring.
   generalize (Zorder.Zgt_pos_0 p1); omega.
   
   intros p1 [H1 H2].
   split; trivial.
-  replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ].
+  change (Zneg p0) with (- Zpos p0); rewrite H1; ring.
   generalize (Zorder.Zlt_neg_0 p1); omega.
   
   intros; discriminate.
 Qed.
 
-(** Existence theorems *)
+(** For stating the fully general result, let's give a short name 
+    to the condition on the remainder. *)
 
-Theorem Zdiv_eucl_exist :
-  forall b:Z,
-    b > 0 ->
-    forall a:Z, {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < b}.
+Definition Remainder r b :=  0 <= r < b \/ b < r <= 0.
+
+(** Another equivalent formulation: *)
+
+Definition Remainder_alt r b :=  Zabs r < Zabs b /\ Zsgn r <> - Zsgn b.
+
+(* In the last formulation, [ Zsgn r <> - Zsgn b ] is less nice than saying 
+    [ Zsgn r = Zsgn b ], but at least it works even when [r] is null. *)
+
+Lemma Remainder_equiv : forall r b, Remainder r b <-> Remainder_alt r b.
+Proof.
+ intros; unfold Remainder, Remainder_alt; omega with *.
+Qed.
+
+Hint Unfold Remainder.
+
+(** Now comes the fully general result about Euclidean division. *)
+
+Theorem Z_div_mod_full :
+  forall a b:Z,
+    b <> 0 -> let (q, r) := Zdiv_eucl a b in a = b * q + r /\ Remainder r b.
+Proof.
+  destruct b as [|b|b].
+  (* b = 0 *)
+  intro H; elim H; auto.
+  (* b > 0 *)
+  intros _.
+  assert (Zpos b > 0) by auto with zarith.
+  generalize (Z_div_mod a (Zpos b) H).
+  destruct Zdiv_eucl as (q,r); intuition; simpl; auto.
+  (* b < 0 *)
+  intros _.
+  assert (Zpos b > 0) by auto with zarith.
+  generalize (Z_div_mod a (Zpos b) H).
+  unfold Remainder.
+  destruct a as [|a|a].
+  (* a = 0 *)
+  simpl; intuition.
+  (* a > 0 *)
+  unfold Zdiv_eucl; destruct Zdiv_eucl_POS as (q,r).
+  destruct r as [|r|r]; [ | | omega with *].
+  rewrite <- Zmult_opp_comm; simpl Zopp; intuition.
+  rewrite <- Zmult_opp_comm; simpl Zopp.
+  rewrite Zmult_plus_distr_r; omega with *.
+  (* a < 0 *)
+  unfold Zdiv_eucl.
+  generalize (Z_div_mod_POS (Zpos b) H a).
+  destruct Zdiv_eucl_POS as (q,r).
+  destruct r as [|r|r]; change (Zneg b) with (-Zpos b).
+  rewrite Zmult_opp_comm; omega with *.
+  rewrite <- Zmult_opp_comm, Zmult_plus_distr_r; 
+   repeat rewrite Zmult_opp_comm; omega.
+  rewrite Zmult_opp_comm; omega with *.
+Qed.
+
+(** The same results as before, stated separately in terms of Zdiv and Zmod *)
+
+Lemma Z_mod_remainder : forall a b:Z, b<>0 -> Remainder (a mod b) b.
+Proof.
+  unfold Zmod; intros a b Hb; generalize (Z_div_mod_full a b Hb); auto.
+  destruct Zdiv_eucl; tauto.
+Qed.
+
+Lemma Z_mod_lt : forall a b:Z, b > 0 -> 0 <= a mod b < b.
+Proof.
+  unfold Zmod; intros a b Hb; generalize (Z_div_mod a b Hb).
+  destruct Zdiv_eucl; tauto.
+Qed.
+
+Lemma Z_mod_neg : forall a b:Z, b < 0 -> b < a mod b <= 0.
+Proof.
+  unfold Zmod; intros a b Hb.
+  assert (Hb' : b<>0) by (auto with zarith).
+  generalize (Z_div_mod_full a b Hb').
+  destruct Zdiv_eucl.
+  unfold Remainder; intuition.
+Qed.
+
+Lemma Z_div_mod_eq_full : forall a b:Z, b <> 0 -> a = b*(a/b) + (a mod b).
+Proof.
+  unfold Zdiv, Zmod; intros a b Hb; generalize (Z_div_mod_full a b Hb).
+  destruct Zdiv_eucl; tauto.
+Qed.
+
+Lemma Z_div_mod_eq : forall a b:Z, b > 0 -> a = b*(a/b) + (a mod b).
+Proof.
+  intros; apply Z_div_mod_eq_full; auto with zarith.
+Qed.
+
+Lemma Zmod_eq_full : forall a b:Z, b<>0 -> a mod b = a - (a/b)*b.
+Proof.
+  intros.
+  rewrite <- Zeq_plus_swap, Zplus_comm, Zmult_comm; symmetry.
+  apply Z_div_mod_eq_full; auto.
+Qed.
+
+Lemma Zmod_eq : forall a b:Z, b>0 -> a mod b = a - (a/b)*b.
+Proof.
+  intros.
+  rewrite <- Zeq_plus_swap, Zplus_comm, Zmult_comm; symmetry.
+  apply Z_div_mod_eq; auto.
+Qed.
+
+(** Existence theorem *)
+
+Theorem Zdiv_eucl_exist : forall (b:Z)(Hb:b>0)(a:Z),
+ {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < b}.
 Proof.
   intros b Hb a.
   exists (Zdiv_eucl a b).
@@ -195,70 +315,180 @@ Qed.
 
 Implicit Arguments Zdiv_eucl_exist.
 
-Theorem Zdiv_eucl_extended :
-  forall b:Z,
-    b <> 0 ->
-    forall a:Z,
-      {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Zabs b}.
+
+(** Uniqueness theorems *)
+
+Theorem Zdiv_mod_unique :
+ forall b q1 q2 r1 r2:Z,
+  0 <= r1 < Zabs b -> 0 <= r2 < Zabs b ->
+  b*q1+r1 = b*q2+r2 -> q1=q2 /\ r1=r2.
 Proof.
-  intros b Hb a.
-  elim (Z_le_gt_dec 0 b); intro Hb'.
-  cut (b > 0); [ intro Hb'' | omega ].
-  rewrite Zabs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ].
-  cut (- b > 0); [ intro Hb'' | omega ].
-  elim (Zdiv_eucl_exist Hb'' a); intros qr.
-  elim qr; intros q r Hqr.
-  exists (- q, r).
-  elim Hqr; intros.
-  split.
-  rewrite <- Zmult_opp_comm; assumption.
-  rewrite Zabs_non_eq; [ assumption | omega ].
+intros b q1 q2 r1 r2 Hr1 Hr2 H.
+destruct (Z_eq_dec q1 q2) as [Hq|Hq].
+split; trivial.
+rewrite Hq in H; omega.
+elim (Zlt_not_le (Zabs (r2 - r1)) (Zabs b)).
+omega with *.
+replace (r2-r1) with (b*(q1-q2)) by (rewrite Zmult_minus_distr_l; omega).
+replace (Zabs b) with ((Zabs b)*1) by ring.
+rewrite Zabs_Zmult. 
+apply Zmult_le_compat_l; auto with *.
+omega with *.
 Qed.
 
-Implicit Arguments Zdiv_eucl_extended.
+Theorem Zdiv_mod_unique_2 :
+ forall b q1 q2 r1 r2:Z,
+  Remainder r1 b -> Remainder r2 b -> 
+  b*q1+r1 = b*q2+r2 -> q1=q2 /\ r1=r2.
+Proof.
+unfold Remainder.
+intros b q1 q2 r1 r2 Hr1 Hr2 H.
+destruct (Z_eq_dec q1 q2) as [Hq|Hq].
+split; trivial.
+rewrite Hq in H; omega.
+elim (Zlt_not_le (Zabs (r2 - r1)) (Zabs b)).
+omega with *.
+replace (r2-r1) with (b*(q1-q2)) by (rewrite Zmult_minus_distr_l; omega).
+replace (Zabs b) with ((Zabs b)*1) by ring.
+rewrite Zabs_Zmult.
+apply Zmult_le_compat_l; auto with *.
+omega with *.
+Qed.
 
-(** * Auxiliary lemmas about [Zdiv] and [Zmod] *)
+Theorem Zdiv_unique_full:
+ forall a b q r, Remainder r b -> 
+   a = b*q + r -> q = a/b.
+Proof.
+  intros.
+  assert (b <> 0) by (unfold Remainder in *; omega with *).
+  generalize (Z_div_mod_full a b H1).
+  unfold Zdiv; destruct Zdiv_eucl as (q',r').
+  intros (H2,H3); rewrite H2 in H0.
+  destruct (Zdiv_mod_unique_2 b q q' r r'); auto.
+Qed.
 
-Lemma Z_div_mod_eq : forall a b:Z, b > 0 -> a = b * Zdiv a b + Zmod a b.
+Theorem Zdiv_unique:
+ forall a b q r, 0 <= r < b -> 
+   a = b*q + r -> q = a/b.
 Proof.
-  unfold Zdiv, Zmod in |- *.
-  intros a b Hb.
-  generalize (Z_div_mod a b Hb).
-  case Zdiv_eucl; tauto.
+  intros; eapply Zdiv_unique_full; eauto.
 Qed.
 
-Lemma Z_mod_lt : forall a b:Z, b > 0 -> 0 <= Zmod a b < b.
+Theorem Zmod_unique_full:
+ forall a b q r, Remainder r b ->
+  a = b*q + r ->  r = a mod b.
 Proof.
-  unfold Zmod in |- *.
-  intros a b Hb.
-  generalize (Z_div_mod a b Hb).
-  case (Zdiv_eucl a b); tauto.
+  intros.
+  assert (b <> 0) by (unfold Remainder in *; omega with *).
+  generalize (Z_div_mod_full a b H1).
+  unfold Zmod; destruct Zdiv_eucl as (q',r').
+  intros (H2,H3); rewrite H2 in H0.
+  destruct (Zdiv_mod_unique_2 b q q' r r'); auto.
 Qed.
 
-Lemma Z_div_POS_ge0 :
-  forall (b:Z) (a:positive), let (q, _) := Zdiv_eucl_POS a b in q >= 0.
+Theorem Zmod_unique:
+ forall a b q r, 0 <= r < b ->
+  a = b*q + r -> r = a mod b.
 Proof.
-  simple induction a; unfold Zdiv_eucl_POS in |- *; fold Zdiv_eucl_POS in |- *.
-  intro p; case (Zdiv_eucl_POS p b).
-  intros; case (Zgt_bool b (2 * z0 + 1)); intros; omega.
-  intro p; case (Zdiv_eucl_POS p b).
-  intros; case (Zgt_bool b (2 * z0)); intros; omega.
-  case (Zge_bool b 2); simpl in |- *; omega.
+  intros; eapply Zmod_unique_full; eauto.
 Qed.
 
-Lemma Z_div_ge0 : forall a b:Z, b > 0 -> a >= 0 -> Zdiv a b >= 0.
+(** * Basic values of divisions and modulo. *)
+
+Lemma Zmod_0_l: forall a, 0 mod a = 0.
 Proof.
-  intros a b Hb; unfold Zdiv, Zdiv_eucl in |- *; case a; simpl in |- *; intros.
-  case b; simpl in |- *; trivial.
-  generalize Hb; case b; try trivial.
-  auto with zarith.
-  intros p0 Hp0; generalize (Z_div_POS_ge0 (Zpos p0) p).
-  case (Zdiv_eucl_POS p (Zpos p0)); simpl in |- *; tauto.
-  intros; discriminate.
-  elim H; trivial.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zmod_0_r: forall a, a mod 0 = 0.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zdiv_0_l: forall a, 0/a = 0.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zdiv_0_r: forall a, a/0 = 0.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zmod_1_r: forall a, a mod 1 = 0.
+Proof.
+  intros; symmetry; apply Zmod_unique with a; auto with zarith.
 Qed.
 
-Lemma Z_div_lt : forall a b:Z, b >= 2 -> a > 0 -> Zdiv a b < a.
+Lemma Zdiv_1_r: forall a, a/1 = a.
+Proof.
+  intros; symmetry; apply Zdiv_unique with 0; auto with zarith.
+Qed.
+
+Hint Resolve Zmod_0_l Zmod_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_1_r 
+ : zarith.
+
+Lemma Zdiv_1_l: forall a, 1 < a -> 1/a = 0.
+Proof.
+  intros; symmetry; apply Zdiv_unique with 1; auto with zarith.
+Qed.
+
+Lemma Zmod_1_l: forall a, 1 < a ->  1 mod a = 1.
+Proof.
+  intros; symmetry; apply Zmod_unique with 0; auto with zarith.
+Qed.
+
+Lemma Z_div_same_full : forall a:Z, a<>0 -> a/a = 1.
+Proof.
+  intros; symmetry; apply Zdiv_unique_full with 0; auto with *; red; omega.
+Qed.
+
+Lemma Z_mod_same_full : forall a, a mod a = 0.
+Proof.
+  destruct a; intros; symmetry.
+  compute; auto.
+  apply Zmod_unique with 1; auto with *; omega with *.
+  apply Zmod_unique_full with 1; auto with *; red; omega with *.
+Qed.
+
+Lemma Z_mod_mult : forall a b, (a*b) mod b = 0.
+Proof.
+  intros a b; destruct (Z_eq_dec b 0) as [Hb|Hb].
+  subst; simpl; rewrite Zmod_0_r; auto.
+  symmetry; apply Zmod_unique_full with a; [ red; omega | ring ].
+Qed.
+
+Lemma Z_div_mult_full : forall a b:Z, b <> 0 -> (a*b)/b = a.
+Proof.
+  intros; symmetry; apply Zdiv_unique_full with 0; auto with zarith; 
+   [ red; omega | ring].
+Qed.
+
+(** * Order results about Zmod and Zdiv *)
+
+(* Division of positive numbers is positive. *)
+
+Lemma Z_div_pos: forall a b, b > 0 -> 0 <= a -> 0 <= a/b.
+Proof.
+  intros.
+  rewrite (Z_div_mod_eq a b H) in H0.
+  assert (H1:=Z_mod_lt a b H).
+  destruct (Z_lt_le_dec (a/b) 0); auto.
+  assert (b*(a/b) <= -b).
+   replace (-b) with (b*-1); [ | ring].
+   apply Zmult_le_compat_l; auto with zarith.
+  omega.
+Qed.
+
+Lemma Z_div_ge0: forall a b, b > 0 -> a >= 0 -> a/b >=0.
+Proof.
+  intros; generalize (Z_div_pos a b H); auto with zarith.
+Qed.
+
+(** As soon as the divisor is greater or equal than 2, 
+    the division is strictly decreasing. *)
+
+Lemma Z_div_lt : forall a b:Z, b >= 2 -> a > 0 -> a/b < a.
 Proof.
   intros. cut (b > 0); [ intro Hb | omega ].
   generalize (Z_div_mod a b Hb).
@@ -271,9 +501,24 @@ Proof.
   auto with zarith.
 Qed.
 
-(** * Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *)
 
-Lemma Z_div_ge : forall a b c:Z, c > 0 -> a >= b -> a / c >= b / c.
+(** A division of a small number by a bigger one yields zero. *)
+
+Theorem Zdiv_small: forall a b, 0 <= a < b -> a/b = 0.
+Proof.
+  intros a b H; apply sym_equal; apply Zdiv_unique with a; auto with zarith.
+Qed.
+
+(** Same situation, in term of modulo: *)
+
+Theorem Zmod_small: forall a n, 0 <= a < n -> a mod n = a.
+Proof.
+  intros a b H; apply sym_equal; apply Zmod_unique with 0; auto with zarith.
+Qed.
+
+(** [Zge] is compatible with a positive division. *)
+
+Lemma Z_div_ge : forall a b c:Z, c > 0 -> a >= b -> a/c >= b/c.
 Proof.
   intros a b c cPos aGeb.
   generalize (Z_div_mod_eq a c cPos).
@@ -285,13 +530,8 @@ Proof.
   intro.
   absurd (b - a >= 1).
   omega.
-  rewrite H0.
-  rewrite H2.
-  assert
-    (c * (b / c) + b mod c - (c * (a / c) + a mod c) =
-      c * (b / c - a / c) + b mod c - a mod c).
-  ring.
-  rewrite H3.
+  replace (b-a) with (c * (b/c-a/c) + b mod c - a mod c) by 
+    (symmetry; pattern a at 1; rewrite H2; pattern b at 1; rewrite H0; ring).
   assert (c * (b / c - a / c) >= c * 1).
   apply Zmult_ge_compat_l.
   omega.
@@ -301,111 +541,639 @@ Proof.
   omega.
 Qed.
 
-Lemma Z_mod_plus : forall a b c:Z, c > 0 -> (a + b * c) mod c = a mod c.
+(** Same, with [Zle]. *)
+
+Lemma Z_div_le : forall a b c:Z, c > 0 -> a <= b -> a/c <= b/c.
 Proof.
-  intros a b c cPos.
-  generalize (Z_div_mod_eq a c cPos).
-  generalize (Z_mod_lt a c cPos).
-  generalize (Z_div_mod_eq (a + b * c) c cPos).
-  generalize (Z_mod_lt (a + b * c) c cPos).
-  intros.
+  intros a b c H H0.
+  apply Zge_le.
+  apply Z_div_ge; auto with *.
+Qed.
 
-  assert ((a + b * c) mod c - a mod c = c * (b + a / c - (a + b * c) / c)).
-  replace ((a + b * c) mod c) with (a + b * c - c * ((a + b * c) / c)).
-  replace (a mod c) with (a - c * (a / c)).
-  ring.
-  omega.
-  omega.
-  set (q := b + a / c - (a + b * c) / c) in *.
-  apply (Zcase_sign q); intros.
-  assert (c * q = 0).
-  rewrite H4; ring.
-  rewrite H5 in H3.
-  omega.
+(** With our choice of division, rounding of (a/b) is always done toward bottom: *)
 
-  assert (c * q >= c).
-  pattern c at 2 in |- *; replace c with (c * 1).
-  apply Zmult_ge_compat_l; omega.
-  ring.
-  omega.
+Lemma Z_mult_div_ge : forall a b:Z, b > 0 -> b*(a/b) <= a.
+Proof.
+  intros a b H; generalize (Z_div_mod_eq a b H) (Z_mod_lt a b H); omega.
+Qed.
+
+Lemma Z_mult_div_ge_neg : forall a b:Z, b < 0 -> b*(a/b) >= a.
+Proof.
+  intros a b H.
+  generalize (Z_div_mod_eq_full a _ (Zlt_not_eq _ _ H)) (Z_mod_neg a _ H); omega.
+Qed.
+
+(** The previous inequalities are exact iff the modulo is zero. *)
+
+Lemma Z_div_exact_full_1 : forall a b:Z, a = b*(a/b) -> a mod b = 0.
+Proof.
+  intros; destruct (Z_eq_dec b 0) as [Hb|Hb].
+  subst b; simpl in *; subst; auto.
+  generalize (Z_div_mod_eq_full a b Hb); omega.
+Qed.
+
+Lemma Z_div_exact_full_2 : forall a b:Z, b <> 0 -> a mod b = 0 -> a = b*(a/b).
+Proof.
+  intros; generalize (Z_div_mod_eq_full a b H); omega.
+Qed.
+
+(** A modulo cannot grow beyond its starting point. *)
+
+Theorem Zmod_le: forall a b, 0 < b -> 0 <= a -> a mod b <= a.
+Proof. 
+  intros a b H1 H2; case (Zle_or_lt b a); intros H3.
+  case (Z_mod_lt a b); auto with zarith.
+  rewrite Zmod_small; auto with zarith.
+Qed.
+
+(** Some additionnal inequalities about Zdiv. *)
+
+Theorem Zdiv_le_upper_bound: 
+  forall a b q, 0 <= a -> 0 < b -> a <= q*b -> a/b <= q.
+Proof.
+  intros a b q H1 H2 H3.
+  apply Zmult_le_reg_r with b; auto with zarith.
+  apply Zle_trans with (2 := H3).
+  pattern a at 2; rewrite (Z_div_mod_eq a b); auto with zarith.
+  rewrite (Zmult_comm b); case (Z_mod_lt a b); auto with zarith.
+Qed.
+
+Theorem Zdiv_lt_upper_bound: 
+  forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q.
+Proof.
+  intros a b q H1 H2 H3.
+  apply Zmult_lt_reg_r with b; auto with zarith.
+  apply Zle_lt_trans with (2 := H3).
+  pattern a at 2; rewrite (Z_div_mod_eq a b); auto with zarith.
+  rewrite (Zmult_comm b); case (Z_mod_lt a b); auto with zarith.
+Qed.
+
+Theorem Zdiv_le_lower_bound: 
+  forall a b q, 0 <= a -> 0 < b -> q*b <= a -> q <= a/b.
+Proof.
+  intros a b q H1 H2 H3.
+  assert (q < a / b + 1); auto with zarith.
+  apply Zmult_lt_reg_r with b; auto with zarith.
+  apply Zle_lt_trans with (1 := H3).
+  pattern a at 1; rewrite (Z_div_mod_eq a b); auto with zarith.
+  rewrite Zmult_plus_distr_l; rewrite (Zmult_comm b); case (Z_mod_lt a b);
+   auto with zarith.
+Qed.
+
+
+(** A division of respect opposite monotonicity for the divisor *)
+
+Lemma Zdiv_le_compat_l: forall p q r, 0 <= p -> 0 < q < r ->
+    p / r <= p / q.
+Proof.
+  intros p q r H H1. 
+  apply Zdiv_le_lower_bound; auto with zarith.
+  rewrite Zmult_comm.
+  pattern p at 2; rewrite (Z_div_mod_eq p r); auto with zarith.
+  apply Zle_trans with (r * (p / r)); auto with zarith.
+  apply Zmult_le_compat_r; auto with zarith.
+  apply Zdiv_le_lower_bound; auto with zarith.
+  case (Z_mod_lt p r); auto with zarith.
+Qed.
+
+Theorem Zdiv_sgn: forall a b, 
+  0 <= Zsgn (a/b) * Zsgn a * Zsgn b.
+Proof.
+  destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith; 
+  generalize (Z_div_pos (Zpos a) (Zpos b)); unfold Zdiv, Zdiv_eucl; 
+  destruct Zdiv_eucl_POS as (q,r); destruct r; omega with *.
+Qed.
+
+(** * Relations between usual operations and Zmod and Zdiv *)
+
+Lemma Z_mod_plus_full : forall a b c:Z, (a + b * c) mod c = a mod c.
+Proof.
+  intros; destruct (Z_eq_dec c 0) as [Hc|Hc].
+  subst; do 2 rewrite Zmod_0_r; auto.
+  symmetry; apply Zmod_unique_full with (a/c+b); auto with zarith.
+  red; generalize (Z_mod_lt a c)(Z_mod_neg a c); omega.
+  rewrite Zmult_plus_distr_r, Zmult_comm.
+  generalize (Z_div_mod_eq_full a c Hc); omega.
+Qed.
+
+Lemma Z_div_plus_full : forall a b c:Z, c <> 0 -> (a + b * c) / c = a / c + b.
+Proof.
+  intro; symmetry.
+  apply Zdiv_unique_full with (a mod c); auto with zarith.
+  red; generalize (Z_mod_lt a c)(Z_mod_neg a c); omega.
+  rewrite Zmult_plus_distr_r, Zmult_comm.
+  generalize (Z_div_mod_eq_full a c H); omega.
+Qed.
+
+Theorem Z_div_plus_full_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b.
+Proof.
+  intros a b c H; rewrite Zplus_comm; rewrite Z_div_plus_full;
+  try apply Zplus_comm; auto with zarith. 
+Qed.
 
-  assert (c * q <= - c).
-  replace (- c) with (c * -1).
-  apply Zmult_le_compat_l; omega.
+(** [Zopp] and [Zdiv], [Zmod].
+    Due to the choice of convention for our Euclidean division, 
+    some of the relations about [Zopp] and divisions are rather complex. *) 
+
+Lemma Zdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b.
+Proof.
+  intros [|a|a] [|b|b]; try reflexivity; unfold Zdiv; simpl;
+  destruct (Zdiv_eucl_POS a (Zpos b)); destruct z0; try reflexivity.
+Qed.
+
+Lemma Zmod_opp_opp : forall a b:Z, (-a) mod (-b) = - (a mod b).
+Proof.
+  intros; destruct (Z_eq_dec b 0) as [Hb|Hb].
+  subst; do 2 rewrite Zmod_0_r; auto.
+  intros; symmetry.
+  apply Zmod_unique_full with ((-a)/(-b)); auto.
+  generalize (Z_mod_remainder a b Hb); destruct 1; [right|left]; omega.
+  rewrite Zdiv_opp_opp.
+  pattern a at 1; rewrite (Z_div_mod_eq_full a b Hb); ring.
+Qed.
+
+Lemma Z_mod_zero_opp_full : forall a b:Z, a mod b = 0 -> (-a) mod b = 0.
+Proof.
+  intros; destruct (Z_eq_dec b 0) as [Hb|Hb].
+  subst; rewrite Zmod_0_r; auto.
+  rewrite Z_div_exact_full_2 with a b; auto.
+  replace (- (b * (a / b))) with (0 + - (a / b) * b).
+  rewrite Z_mod_plus_full; auto.
   ring.
-  omega.
 Qed.
 
-Lemma Z_div_plus : forall a b c:Z, c > 0 -> (a + b * c) / c = a / c + b.
+Lemma Z_mod_nz_opp_full : forall a b:Z, a mod b <> 0 -> 
+ (-a) mod b = b - (a mod b).
 Proof.
-  intros a b c cPos.
-  generalize (Z_div_mod_eq a c cPos).
-  generalize (Z_mod_lt a c cPos).
-  generalize (Z_div_mod_eq (a + b * c) c cPos).
-  generalize (Z_mod_lt (a + b * c) c cPos).
   intros.
-  apply Zmult_reg_l with c. omega.
-  replace (c * ((a + b * c) / c)) with (a + b * c - (a + b * c) mod c).
-  rewrite (Z_mod_plus a b c cPos).
-  pattern a at 1 in |- *; rewrite H2.
-  ring.
-  pattern (a + b * c) at 1 in |- *; rewrite H0.
-  ring.
+  assert (b<>0) by (contradict H; subst; rewrite Zmod_0_r; auto).
+  symmetry; apply Zmod_unique_full with (-1-a/b); auto.
+  generalize (Z_mod_remainder a b H0); destruct 1; [left|right]; omega.
+  rewrite Zmult_minus_distr_l.
+  pattern a at 1; rewrite (Z_div_mod_eq_full a b H0); ring.
 Qed.
 
-Lemma Z_div_mult : forall a b:Z, b > 0 -> a * b / b = a.
-  intros; replace (a * b) with (0 + a * b); auto.
-  rewrite Z_div_plus; auto.
+Lemma Z_mod_zero_opp_r : forall a b:Z, a mod b = 0 -> a mod (-b) = 0.
+Proof.
+  intros.
+  rewrite <- (Zopp_involutive a).
+  rewrite Zmod_opp_opp.
+  rewrite Z_mod_zero_opp_full; auto.
 Qed.
 
-Lemma Z_mult_div_ge : forall a b:Z, b > 0 -> b * (a / b) <= a.
+Lemma Z_mod_nz_opp_r : forall a b:Z, a mod b <> 0 -> 
+ a mod (-b) = (a mod b) - b.
 Proof.
-  intros a b bPos.
-  generalize (Z_div_mod_eq a _ bPos); intros.
-  generalize (Z_mod_lt a _ bPos); intros.
-  pattern a at 2 in |- *; rewrite H.
-  omega.
+  intros.
+  pattern a at 1; rewrite <- (Zopp_involutive a).
+  rewrite Zmod_opp_opp.
+  rewrite Z_mod_nz_opp_full; auto; omega.
+Qed.
+
+Lemma Z_div_zero_opp_full : forall a b:Z, a mod b = 0 -> (-a)/b = -(a/b).
+Proof.
+  intros; destruct (Z_eq_dec b 0) as [Hb|Hb].
+  subst; do 2 rewrite Zdiv_0_r; auto.
+  symmetry; apply Zdiv_unique_full with 0; auto.
+  red; omega.
+  pattern a at 1; rewrite (Z_div_mod_eq_full a b Hb).
+  rewrite H; ring.
 Qed.
 
-Lemma Z_mod_same : forall a:Z, a > 0 -> a mod a = 0.
+Lemma Z_div_nz_opp_full : forall a b:Z, a mod b <> 0 -> 
+ (-a)/b = -(a/b)-1.
 Proof.
-  intros a aPos.
-  generalize (Z_mod_plus 0 1 a aPos).
-  replace (0 + 1 * a) with a.
   intros.
-  rewrite H.
-  compute in |- *.
-  trivial.
-  ring.
+  assert (b<>0) by (contradict H; subst; rewrite Zmod_0_r; auto).
+  symmetry; apply Zdiv_unique_full with (b-a mod b); auto.
+  generalize (Z_mod_remainder a b H0); destruct 1; [left|right]; omega.
+  pattern a at 1; rewrite (Z_div_mod_eq_full a b H0); ring.
+Qed.
+
+Lemma Z_div_zero_opp_r : forall a b:Z, a mod b = 0 -> a/(-b) = -(a/b).
+Proof.
+  intros.
+  pattern a at 1; rewrite <- (Zopp_involutive a).
+  rewrite Zdiv_opp_opp.
+  rewrite Z_div_zero_opp_full; auto.
+Qed.
+
+Lemma Z_div_nz_opp_r : forall a b:Z, a mod b <> 0 -> 
+ a/(-b) = -(a/b)-1.
+Proof.
+  intros.
+  pattern a at 1; rewrite <- (Zopp_involutive a).
+  rewrite Zdiv_opp_opp.
+  rewrite Z_div_nz_opp_full; auto; omega.
+Qed.
+
+(** Cancellations. *)
+
+Lemma Zdiv_mult_cancel_r : forall a b c:Z, 
+ c <> 0 -> (a*c)/(b*c) = a/b.
+Proof.
+assert (X: forall a b c, b > 0 -> c > 0 -> (a*c) / (b*c) = a / b).
+ intros a b c Hb Hc.
+ symmetry.
+ apply Zdiv_unique with ((a mod b)*c); auto with zarith.
+ destruct (Z_mod_lt a b Hb); split.
+ apply Zmult_le_0_compat; auto with zarith.
+ apply Zmult_lt_compat_r; auto with zarith.
+ pattern a at 1; rewrite (Z_div_mod_eq a b Hb); ring.
+intros a b c Hc.
+destruct (Z_dec b 0) as [Hb|Hb]. 
+destruct Hb as [Hb|Hb]; destruct (not_Zeq_inf _ _ Hc); auto with *.
+rewrite <- (Zdiv_opp_opp a), <- (Zmult_opp_opp b), <-(Zmult_opp_opp a); 
+ auto with *.
+rewrite <- (Zdiv_opp_opp a), <- Zdiv_opp_opp, Zopp_mult_distr_l, 
+ Zopp_mult_distr_l; auto with *.
+rewrite <- Zdiv_opp_opp, Zopp_mult_distr_r, Zopp_mult_distr_r; auto with *.
+rewrite Hb; simpl; do 2 rewrite Zdiv_0_r; auto.
 Qed.
 
-Lemma Z_div_same : forall a:Z, a > 0 -> a / a = 1.
+Lemma Zdiv_mult_cancel_l : forall a b c:Z, 
+ c<>0 -> (c*a)/(c*b) = a/b.
 Proof.
-  intros a aPos.
-  generalize (Z_div_plus 0 1 a aPos).
-  replace (0 + 1 * a) with a.
   intros.
-  rewrite H.
-  compute in |- *.
-  trivial.
+  rewrite (Zmult_comm c a); rewrite (Zmult_comm c b).
+  apply Zdiv_mult_cancel_r; auto.
+Qed.
+
+Lemma Zmult_mod_distr_l: forall a b c, 
+  (c*a) mod (c*b) = c * (a mod b).
+Proof.
+  intros; destruct (Z_eq_dec c 0) as [Hc|Hc].
+  subst; simpl; rewrite Zmod_0_r; auto.
+  destruct (Z_eq_dec b 0) as [Hb|Hb].
+  subst; repeat rewrite Zmult_0_r || rewrite Zmod_0_r; auto.
+  assert (c*b <> 0).
+   contradict Hc; eapply Zmult_integral_l; eauto.
+  rewrite (Zplus_minus_eq _ _ _ (Z_div_mod_eq_full (c*a) (c*b) H)).
+  rewrite (Zplus_minus_eq _ _ _ (Z_div_mod_eq_full a b Hb)).
+  rewrite Zdiv_mult_cancel_l; auto with zarith.
   ring.
 Qed.
 
-Lemma Z_div_exact_1 : forall a b:Z, b > 0 -> a = b * (a / b) -> a mod b = 0.
-  intros a b Hb; generalize (Z_div_mod a b Hb); unfold Zmod, Zdiv in |- *.
-  case (Zdiv_eucl a b); intros q r; omega.
+Lemma Zmult_mod_distr_r: forall a b c, 
+  (a*c) mod (b*c) = (a mod b) * c.
+Proof.
+  intros; repeat rewrite (fun x => (Zmult_comm x c)).
+  apply Zmult_mod_distr_l; auto.
+Qed.
+
+(** Operations modulo. *)
+
+Theorem Zmod_mod: forall a n, (a mod n) mod n = a mod n.
+Proof.
+  intros; destruct (Z_eq_dec n 0) as [Hb|Hb].
+  subst; do 2 rewrite Zmod_0_r; auto.
+  pattern a at 2; rewrite (Z_div_mod_eq_full a n); auto with zarith.
+  rewrite Zplus_comm; rewrite Zmult_comm.
+  apply sym_equal; apply Z_mod_plus_full; auto with zarith.
+Qed.
+
+Theorem Zmult_mod: forall a b n,
+ (a * b) mod n = ((a mod n) * (b mod n)) mod n.
+Proof.
+  intros; destruct (Z_eq_dec n 0) as [Hb|Hb].
+  subst; do 2 rewrite Zmod_0_r; auto.
+  pattern a at 1; rewrite (Z_div_mod_eq_full a n); auto with zarith.
+  pattern b at 1; rewrite (Z_div_mod_eq_full b n); auto with zarith.
+  set (A:=a mod n); set (B:=b mod n); set (A':=a/n); set (B':=b/n).
+  replace ((n*A' + A) * (n*B' + B))
+   with (A*B + (A'*B+B'*A+n*A'*B')*n) by ring.
+  apply Z_mod_plus_full; auto with zarith.
 Qed.
 
-Lemma Z_div_exact_2 : forall a b:Z, b > 0 -> a mod b = 0 -> a = b * (a / b).
-  intros a b Hb; generalize (Z_div_mod a b Hb); unfold Zmod, Zdiv in |- *.
-  case (Zdiv_eucl a b); intros q r; omega.
+Theorem Zplus_mod: forall a b n,
+ (a + b) mod n = (a mod n + b mod n) mod n.
+Proof.
+  intros; destruct (Z_eq_dec n 0) as [Hb|Hb].
+  subst; do 2 rewrite Zmod_0_r; auto.
+  pattern a at 1; rewrite (Z_div_mod_eq_full a n); auto with zarith.
+  pattern b at 1; rewrite (Z_div_mod_eq_full b n); auto with zarith.
+  replace ((n * (a / n) + a mod n) + (n * (b / n) + b mod n))
+     with ((a mod n + b mod n) + (a / n + b / n) * n) by ring.
+  apply Z_mod_plus_full; auto with zarith.
 Qed.
 
-Lemma Z_mod_zero_opp : forall a b:Z, b > 0 -> a mod b = 0 -> - a mod b = 0.
-  intros a b Hb.
+Theorem Zminus_mod: forall a b n,
+ (a - b) mod n = (a mod n - b mod n) mod n.
+Proof.
   intros.
-  rewrite Z_div_exact_2 with a b; auto.
-  replace (- (b * (a / b))) with (0 + - (a / b) * b).
-  rewrite Z_mod_plus; auto.
+  replace (a - b) with (a + (-1) * b); auto with zarith.
+  replace (a mod n - b mod n) with (a mod n + (-1) * (b mod n)); auto with zarith.
+  rewrite Zplus_mod.
+  rewrite Zmult_mod.
+  rewrite Zplus_mod with (b:=(-1) * (b mod n)).
+  rewrite Zmult_mod.
+  rewrite Zmult_mod with (b:= b mod n).
+  repeat rewrite Zmod_mod; auto.
+Qed.
+
+Lemma Zplus_mod_idemp_l: forall a b n, (a mod n + b) mod n = (a + b) mod n.
+Proof.
+  intros; rewrite Zplus_mod, Zmod_mod, <- Zplus_mod; auto.
+Qed.
+
+Lemma Zplus_mod_idemp_r: forall a b n, (b + a mod n) mod n = (b + a) mod n.
+Proof.
+  intros; rewrite Zplus_mod, Zmod_mod, <- Zplus_mod; auto.
+Qed.
+
+Lemma Zminus_mod_idemp_l: forall a b n, (a mod n - b) mod n = (a - b) mod n.
+Proof.
+  intros; rewrite Zminus_mod, Zmod_mod, <- Zminus_mod; auto.
+Qed.
+
+Lemma Zminus_mod_idemp_r: forall a b n, (a - b mod n) mod n = (a - b) mod n.
+Proof.
+  intros; rewrite Zminus_mod, Zmod_mod, <- Zminus_mod; auto.
+Qed.
+
+Lemma Zmult_mod_idemp_l: forall a b n, (a mod n * b) mod n = (a * b) mod n.
+Proof.
+  intros; rewrite Zmult_mod, Zmod_mod, <- Zmult_mod; auto.
+Qed.
+
+Lemma Zmult_mod_idemp_r: forall a b n, (b * (a mod n)) mod n = (b * a) mod n.
+Proof.
+  intros; rewrite Zmult_mod, Zmod_mod, <- Zmult_mod; auto.
+Qed.
+
+(** For a specific number n, equality modulo n is hence a nice setoid
+   equivalence, compatible with the usual operations. Due to restrictions 
+   with Coq setoids, we cannot state this in a section, but it works
+   at least with a module. *)
+
+Module Type SomeNumber.
+ Parameter n:Z.
+End SomeNumber.
+
+Module EqualityModulo (M:SomeNumber).
+
+ Definition eqm a b := (a mod M.n = b mod M.n).
+ Infix "==" := eqm (at level 70).
+
+ Lemma eqm_refl : forall a, a == a.
+ Proof. unfold eqm; auto. Qed.
+
+ Lemma eqm_sym : forall a b, a == b -> b == a.
+ Proof. unfold eqm; auto. Qed.
+
+ Lemma eqm_trans : forall a b c, a == b -> b == c -> a == c.
+ Proof. unfold eqm; eauto with *. Qed.
+
+ Add Relation Z eqm
+ reflexivity proved by eqm_refl
+ symmetry proved by eqm_sym
+ transitivity proved by eqm_trans as eqm_setoid.
+
+ Add Morphism Zplus : Zplus_eqm.
+ Proof.
+  unfold eqm; intros; rewrite Zplus_mod, H, H0, <- Zplus_mod; auto.
+ Qed.
+
+ Add Morphism Zminus : Zminus_eqm.
+ Proof.
+  unfold eqm; intros; rewrite Zminus_mod, H, H0, <- Zminus_mod; auto.
+ Qed.
+
+ Add Morphism Zmult : Zmult_eqm.
+ Proof.
+  unfold eqm; intros; rewrite Zmult_mod, H, H0, <- Zmult_mod; auto.
+ Qed.
+
+ Add Morphism Zopp : Zopp_eqm.
+ Proof.
+  intros; change (-x == -y) with (0-x == 0-y).
+  rewrite H; red; auto.
+ Qed.
+
+ Lemma Zmod_eqm : forall a, a mod M.n == a.
+ Proof. 
+  unfold eqm; intros; apply Zmod_mod.
+ Qed.
+
+ (* Zmod and Zdiv are not full morphisms with respect to eqm. 
+    For instance, take n=2. Then 3 == 1 but we don't have 
+    1 mod 3 == 1 mod 1 nor 1/3 == 1/1.
+ *)
+
+End EqualityModulo.
+
+Lemma Zdiv_Zdiv : forall a b c, 0<=b -> 0<=c -> (a/b)/c = a/(b*c).
+Proof.
+  intros a b c Hb Hc.
+  destruct (Zle_lt_or_eq _ _ Hb); [ | subst; rewrite Zdiv_0_r, Zdiv_0_r, Zdiv_0_l; auto].
+  destruct (Zle_lt_or_eq _ _ Hc); [ | subst; rewrite Zmult_0_r, Zdiv_0_r, Zdiv_0_r; auto].
+  pattern a at 2;rewrite (Z_div_mod_eq_full a b);auto with zarith.
+  pattern (a/b) at 2;rewrite (Z_div_mod_eq_full (a/b) c);auto with zarith.
+  replace (b * (c * (a / b / c) + (a / b) mod c) + a mod b) with
+    ((a / b / c)*(b * c)  + (b * ((a / b) mod c) + a mod b)) by ring.
+  rewrite Z_div_plus_full_l; auto with zarith.
+  rewrite (Zdiv_small (b * ((a / b) mod c) + a mod b)).
   ring.
+  split.
+  apply Zplus_le_0_compat;auto with zarith.
+  apply Zmult_le_0_compat;auto with zarith.
+  destruct (Z_mod_lt (a/b) c);auto with zarith.
+  destruct (Z_mod_lt a b);auto with zarith.
+  apply Zle_lt_trans with (b * ((a / b) mod c) + (b-1)).
+  destruct (Z_mod_lt a b);auto with zarith.
+  apply Zle_lt_trans with (b * (c-1) + (b - 1)).
+  apply Zplus_le_compat;auto with zarith.
+  destruct (Z_mod_lt (a/b) c);auto with zarith.
+  replace (b * (c - 1) + (b - 1)) with (b*c-1);try ring;auto with zarith.
+  intro H1; 
+  assert (H2: c <> 0) by auto with zarith; 
+  rewrite (Zmult_integral_l _ _ H2 H1) in H; auto with zarith.
+Qed.
+
+(** Unfortunately, the previous result isn't always true on negative numbers.
+    For instance: 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) *)
+
+(** A last inequality: *)
+
+Theorem Zdiv_mult_le:
+ forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b.
+Proof.
+  intros a b c H1 H2 H3.
+  destruct (Zle_lt_or_eq _ _ H2); 
+   [ | subst; rewrite Zdiv_0_r, Zdiv_0_r, Zmult_0_r; auto].
+  case (Z_mod_lt a b); auto with zarith; intros Hu1 Hu2.
+  case (Z_mod_lt c b); auto with zarith; intros Hv1 Hv2.
+  apply Zmult_le_reg_r with b; auto with zarith.
+  rewrite <- Zmult_assoc.
+  replace (a / b * b) with (a - a mod b).
+  replace (c * a / b * b) with (c * a - (c * a) mod b).
+  rewrite Zmult_minus_distr_l.
+  unfold Zminus; apply Zplus_le_compat_l.
+  match goal with |- - ?X <= -?Y => assert (Y <= X); auto with zarith end.
+  apply Zle_trans with ((c mod b) * (a mod b)); auto with zarith.
+  rewrite Zmult_mod; auto with zarith.
+  apply (Zmod_le ((c mod b) * (a mod b)) b); auto with zarith.
+  apply Zmult_le_compat_r; auto with zarith.
+  apply (Zmod_le c b); auto.
+  pattern (c * a) at 1; rewrite (Z_div_mod_eq (c * a) b); try ring; 
+    auto with zarith.
+  pattern a at 1; rewrite (Z_div_mod_eq a b); try ring; auto with zarith.
+Qed.
+
+(** Zmod is related to divisibility (see more in Znumtheory) *)
+
+Lemma Zmod_divides : forall a b, b<>0 -> 
+ (a mod b = 0 <-> exists c, a = b*c).
+Proof.
+ split; intros.
+ exists (a/b).
+ pattern a at 1; rewrite (Z_div_mod_eq_full a b); auto with zarith.
+ destruct H0 as [c Hc].
+ symmetry.
+ apply Zmod_unique_full with c; auto with zarith.
+ red; omega with *.
+Qed.
+
+(** * Compatibility *)
+
+(** Weaker results kept only for compatibility *)
+
+Lemma Z_mod_same : forall a, a > 0 -> a mod a = 0.
+Proof.
+  intros; apply Z_mod_same_full.
+Qed.
+
+Lemma Z_div_same : forall a, a > 0 -> a/a = 1.
+Proof.
+  intros; apply Z_div_same_full; auto with zarith.
+Qed.
+
+Lemma Z_div_plus : forall a b c:Z, c > 0 -> (a + b * c) / c = a / c + b.
+Proof.
+  intros; apply Z_div_plus_full; auto with zarith.
+Qed.
+
+Lemma Z_div_mult : forall a b:Z, b > 0 -> (a*b)/b = a.
+Proof.
+  intros; apply Z_div_mult_full; auto with zarith.
 Qed.
+
+Lemma Z_mod_plus : forall a b c:Z, c > 0 -> (a + b * c) mod c = a mod c.
+Proof.
+  intros; apply Z_mod_plus_full; auto with zarith.
+Qed.
+
+Lemma Z_div_exact_1 : forall a b:Z, b > 0 -> a = b*(a/b) -> a mod b = 0.
+Proof.
+  intros; apply Z_div_exact_full_1; auto with zarith.
+Qed.
+
+Lemma Z_div_exact_2 : forall a b:Z, b > 0 -> a mod b = 0 -> a = b*(a/b).
+Proof.
+  intros; apply Z_div_exact_full_2; auto with zarith.
+Qed.
+
+Lemma Z_mod_zero_opp : forall a b:Z, b > 0 -> a mod b = 0 -> (-a) mod b = 0.
+Proof.
+  intros; apply Z_mod_zero_opp_full; auto with zarith.
+Qed.
+
+(** * A direct way to compute Zmod *)
+
+Fixpoint Zmod_POS (a : positive) (b : Z) {struct a} : Z  :=
+  match a with
+   | xI a' =>
+      let r := Zmod_POS a' b in
+      let r' := (2 * r + 1) in
+      if Zgt_bool b r' then r' else (r' - b)
+   | xO a' =>
+      let r := Zmod_POS a' b in
+      let r' := (2 * r) in
+      if Zgt_bool b r' then r' else (r' - b)
+   | xH => if Zge_bool b 2 then 1 else 0
+  end.
+
+Definition Zmod' a b :=
+  match a with
+   | Z0 => 0
+   | Zpos a' =>
+      match b with
+       | Z0 => 0
+       | Zpos _ => Zmod_POS a' b
+       | Zneg b' =>
+          let r := Zmod_POS a' (Zpos b') in
+          match r  with Z0 =>  0 |  _  =>   b + r end
+      end
+   | Zneg a' =>
+      match b with
+       | Z0 => 0
+       | Zpos _ =>
+          let r := Zmod_POS a' b in
+          match r with Z0 =>  0 | _  =>  b - r end
+       | Zneg b' => - (Zmod_POS a' (Zpos b'))
+      end
+  end.
+
+
+Theorem Zmod_POS_correct: forall a b, Zmod_POS a b = (snd (Zdiv_eucl_POS a b)).
+Proof.
+  intros a b; elim a; simpl; auto.
+  intros p Rec; rewrite  Rec.
+  case (Zdiv_eucl_POS p b); intros z1 z2; simpl; auto.
+  match goal with |- context [Zgt_bool _ ?X] => case (Zgt_bool b X) end; auto.
+  intros p Rec; rewrite  Rec.
+  case (Zdiv_eucl_POS p b); intros z1 z2; simpl; auto.
+  match goal with |- context [Zgt_bool _ ?X] => case (Zgt_bool b X) end; auto.
+  case (Zge_bool b 2); auto.
+Qed.
+
+Theorem Zmod'_correct: forall a b, Zmod' a b = Zmod a b.
+Proof.
+  intros a b; unfold Zmod; case a; simpl; auto.
+  intros p; case b; simpl; auto.
+  intros p1; refine (Zmod_POS_correct _ _); auto.
+  intros p1; rewrite Zmod_POS_correct; auto.
+  case (Zdiv_eucl_POS p (Zpos p1)); simpl; intros z1 z2; case z2; auto.
+  intros p; case b; simpl; auto.
+  intros p1; rewrite Zmod_POS_correct; auto.
+  case (Zdiv_eucl_POS p (Zpos p1)); simpl; intros z1 z2; case z2; auto.
+  intros p1; rewrite Zmod_POS_correct; simpl; auto.
+  case (Zdiv_eucl_POS p (Zpos p1)); auto.
+Qed.
+
+
+(** Another convention is possible for division by negative numbers:
+    * quotient is always the biggest integer smaller than or equal to a/b
+    * remainder is hence always positive or null. *)
+
+Theorem Zdiv_eucl_extended :
+  forall b:Z,
+    b <> 0 ->
+    forall a:Z,
+      {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Zabs b}.
+Proof.
+  intros b Hb a.
+  elim (Z_le_gt_dec 0 b); intro Hb'.
+  cut (b > 0); [ intro Hb'' | omega ].
+  rewrite Zabs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ].
+  cut (- b > 0); [ intro Hb'' | omega ].
+  elim (Zdiv_eucl_exist Hb'' a); intros qr.
+  elim qr; intros q r Hqr.
+  exists (- q, r).
+  elim Hqr; intros.
+  split.
+  rewrite <- Zmult_opp_comm; assumption.
+  rewrite Zabs_non_eq; [ assumption | omega ].
+Qed.
+
+Implicit Arguments Zdiv_eucl_extended.
+
+(** A third convention: Ocaml.
+   
+     See files ZOdiv_def.v and ZOdiv.v.
+     
+     Ocaml uses Round-Toward-Zero division: (-a)/b = a/(-b) = -(a/b).
+     Hence (-a) mod b = - (a mod b)
+           a mod (-b) = a mod b
+     And: |r| < |b| and sgn(r) = sgn(a)  (notice the a here instead of b). 
+*)
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 6fab4461..4a402c61 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -6,10 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Zeven.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Zeven.v 10291 2007-11-06 02:18:53Z letouzey $ i*)
 
 Require Import BinInt.
 
+Open Scope Z_scope.
+
 (*******************************************************************)
 (** About parity: even and odd predicates on Z, division by 2 on Z *)
 
@@ -135,14 +137,14 @@ Hint Unfold Zeven Zodd: zarith.
 
 Definition Zdiv2 (z:Z) :=
   match z with
-    | Z0 => 0%Z
-    | Zpos xH => 0%Z
+    | Z0 => 0
+    | Zpos xH => 0
     | Zpos p => Zpos (Pdiv2 p)
-    | Zneg xH => 0%Z
+    | Zneg xH => 0
     | Zneg p => Zneg (Pdiv2 p)
   end.
 
-Lemma Zeven_div2 : forall n:Z, Zeven n -> n = (2 * Zdiv2 n)%Z.
+Lemma Zeven_div2 : forall n:Z, Zeven n -> n = 2 * Zdiv2 n.
 Proof.
   intro x; destruct x.
   auto with arith.
@@ -154,27 +156,27 @@ Proof.
   intros. absurd (Zeven (-1)); red in |- *; auto with arith.
 Qed.
 
-Lemma Zodd_div2 : forall n:Z, (n >= 0)%Z -> Zodd n -> n = (2 * Zdiv2 n + 1)%Z.
+Lemma Zodd_div2 : forall n:Z, n >= 0 -> Zodd n -> n = 2 * Zdiv2 n + 1.
 Proof.
   intro x; destruct x.
   intros. absurd (Zodd 0); red in |- *; auto with arith.
   destruct p; auto with arith.
   intros. absurd (Zodd (Zpos (xO p))); red in |- *; auto with arith.
-  intros. absurd (Zneg p >= 0)%Z; red in |- *; auto with arith.
+  intros. absurd (Zneg p >= 0); red in |- *; auto with arith.
 Qed.
 
 Lemma Zodd_div2_neg :
-  forall n:Z, (n <= 0)%Z -> Zodd n -> n = (2 * Zdiv2 n - 1)%Z.
+  forall n:Z, n <= 0 -> Zodd n -> n = 2 * Zdiv2 n - 1.
 Proof.
   intro x; destruct x.
   intros. absurd (Zodd 0); red in |- *; auto with arith.
-  intros. absurd (Zneg p >= 0)%Z; red in |- *; auto with arith.
+  intros. absurd (Zneg p >= 0); red in |- *; auto with arith.
   destruct p; auto with arith.
   intros. absurd (Zodd (Zneg (xO p))); red in |- *; auto with arith.
 Qed.
 
 Lemma Z_modulo_2 :
-  forall n:Z, {y : Z | n = (2 * y)%Z} + {y : Z | n = (2 * y + 1)%Z}.
+  forall n:Z, {y : Z | n = 2 * y} + {y : Z | n = 2 * y + 1}.
 Proof.
   intros x.
   elim (Zeven_odd_dec x); intro.
@@ -193,7 +195,7 @@ Qed.
 Lemma Zsplit2 :
   forall n:Z,
     {p : Z * Z |
-      let (x1, x2) := p in n = (x1 + x2)%Z /\ (x1 = x2 \/ x2 = (x1 + 1)%Z)}.
+      let (x1, x2) := p in n = x1 + x2 /\ (x1 = x2 \/ x2 = x1 + 1)}.
 Proof.
   intros x.
   elim (Z_modulo_2 x); intros [y Hy]; rewrite Zmult_comm in Hy;
@@ -206,3 +208,109 @@ Proof.
   right; reflexivity.
 Qed.
 
+
+Theorem Zeven_ex: forall n, Zeven n -> exists m, n = 2 * m.
+Proof.
+  intro n; exists (Zdiv2 n); apply Zeven_div2; auto.
+Qed.
+
+Theorem Zodd_ex: forall n, Zodd n -> exists m, n = 2 * m + 1.
+Proof.
+  destruct n; intros.
+  inversion H.
+  exists (Zdiv2 (Zpos p)).
+  apply Zodd_div2; simpl; auto; compute; inversion 1.
+  exists (Zdiv2 (Zneg p) - 1).
+  unfold Zminus.
+  rewrite Zmult_plus_distr_r.
+  rewrite <- Zplus_assoc.
+  assert (Zneg p <= 0) by (compute; inversion 1).
+  exact (Zodd_div2_neg _ H0 H).
+Qed.
+
+Theorem Zeven_2p: forall p, Zeven (2 * p).
+Proof.
+  destruct p; simpl; auto.
+Qed.
+
+Theorem Zodd_2p_plus_1: forall p, Zodd (2 * p + 1).
+Proof.
+  destruct p; simpl; auto.
+  destruct p; simpl; auto.
+Qed.
+
+Theorem Zeven_plus_Zodd: forall a b, 
+ Zeven a -> Zodd b -> Zodd (a + b).
+Proof.
+  intros a b H1 H2; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto.
+  case Zodd_ex with (1 := H2); intros y H4; try rewrite H4; auto.
+  replace (2 * x + (2 * y + 1)) with (2 * (x + y) + 1); try apply Zodd_2p_plus_1; auto with zarith.
+  rewrite Zmult_plus_distr_r, Zplus_assoc; auto.
+Qed.
+
+Theorem Zeven_plus_Zeven: forall a b,
+ Zeven a -> Zeven b -> Zeven (a + b).
+Proof.
+  intros a b H1 H2; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto.
+  case Zeven_ex with (1 := H2); intros y H4; try rewrite H4; auto.
+  replace (2 * x + 2 * y) with (2 * (x + y)); try apply Zeven_2p; auto with zarith.
+  apply Zmult_plus_distr_r; auto.
+Qed.
+
+Theorem Zodd_plus_Zeven: forall a b, 
+ Zodd a -> Zeven b -> Zodd (a + b).
+Proof.
+  intros a b H1 H2; rewrite Zplus_comm; apply Zeven_plus_Zodd; auto.
+Qed.
+
+Theorem Zodd_plus_Zodd: forall a b, 
+ Zodd a -> Zodd b -> Zeven (a + b).
+Proof.
+  intros a b H1 H2; case Zodd_ex with (1 := H1); intros x H3; try rewrite H3; auto.
+  case Zodd_ex with (1 := H2); intros y H4; try rewrite H4; auto.
+  replace ((2 * x + 1) + (2 * y + 1)) with (2 * (x + y + 1)); try apply Zeven_2p; auto.
+  (* ring part *)
+  do 2 rewrite Zmult_plus_distr_r; auto.
+  repeat rewrite <- Zplus_assoc; f_equal.
+  rewrite (Zplus_comm 1).
+  repeat rewrite <- Zplus_assoc; auto.
+Qed.
+
+Theorem Zeven_mult_Zeven_l: forall a b, 
+ Zeven a -> Zeven (a * b).
+Proof.
+  intros a b H1; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto.
+  replace (2 * x * b) with (2 * (x * b)); try apply Zeven_2p; auto with zarith.
+  (* ring part *)
+  apply Zmult_assoc.
+Qed.
+
+Theorem Zeven_mult_Zeven_r: forall a b, 
+ Zeven b -> Zeven (a * b).
+Proof.
+  intros a b H1; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto.
+  replace (a * (2 * x)) with (2 * (x * a)); try apply Zeven_2p; auto.
+  (* ring part *)
+  rewrite (Zmult_comm x a).
+  do 2 rewrite Zmult_assoc.
+  rewrite (Zmult_comm 2 a); auto.
+Qed.
+
+Hint Rewrite Zmult_plus_distr_r Zmult_plus_distr_l 
+     Zplus_assoc Zmult_1_r Zmult_1_l : Zexpand.
+
+Theorem Zodd_mult_Zodd: forall a b, 
+ Zodd a -> Zodd b -> Zodd (a * b).
+Proof.
+  intros a b H1 H2; case Zodd_ex with (1 := H1); intros x H3; try rewrite H3; auto.
+  case Zodd_ex with (1 := H2); intros y H4; try rewrite H4; auto.
+  replace ((2 * x + 1) * (2 * y + 1)) with (2 * (2 * x * y + x + y) + 1); try apply Zodd_2p_plus_1; auto.
+  (* ring part *)
+  autorewrite with Zexpand; f_equal.
+  repeat rewrite <- Zplus_assoc; f_equal.
+  repeat rewrite <- Zmult_assoc; f_equal. 
+  repeat rewrite Zmult_assoc; f_equal; apply Zmult_comm.
+Qed.
+
+(* for compatibility *)
+Close Scope Z_scope.
diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v
new file mode 100644
index 00000000..286dd710
--- /dev/null
+++ b/theories/ZArith/Zgcd_alt.v
@@ -0,0 +1,317 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Zgcd_alt.v 10997 2008-05-27 15:16:40Z letouzey $ i*)
+
+(** * Zgcd_alt : an alternate version of Zgcd, based on Euler's algorithm *)
+
+(**
+Author: Pierre Letouzey
+*)
+
+(** The alternate [Zgcd_alt] given here used to be the main [Zgcd]
+    function (see file [Znumtheory]), but this main [Zgcd] is now
+    based on a modern binary-efficient algorithm. This earlier
+    version, based on Euler's algorithm of iterated modulo, is kept
+    here due to both its intrinsic interest and its use as reference
+    point when proving gcd on Int31 numbers *)
+
+Require Import ZArith_base.
+Require Import ZArithRing.
+Require Import Zdiv.
+Require Import Znumtheory.
+
+Open Scope Z_scope.
+
+(** In Coq, we need to control the number of iteration of modulo.
+   For that, we use an explicit measure in [nat], and we prove later
+   that using [2*d] is enough, where [d] is the number of binary 
+   digits of the first argument. *)
+
+ Fixpoint Zgcdn (n:nat) : Z -> Z -> Z := fun a b =>
+   match n with
+     | O => 1 (* arbitrary, since n should be big enough *)
+     | S n => match a with
+  	        | Z0 => Zabs b
+  	        | Zpos _ => Zgcdn n (Zmod b a) a
+  	        | Zneg a => Zgcdn n (Zmod b (Zpos a)) (Zpos a)
+  	      end
+   end.
+
+ Definition Zgcd_bound (a:Z) := 
+   match a with
+     | Z0 => S O
+     | Zpos p => let n := Psize p in (n+n)%nat
+     | Zneg p => let n := Psize p in (n+n)%nat
+   end.
+ 
+ Definition Zgcd_alt a b := Zgcdn (Zgcd_bound a) a b.
+ 
+ (** A first obvious fact : [Zgcd a b] is positive. *)
+ 
+ Lemma Zgcdn_pos : forall n a b,
+   0 <= Zgcdn n a b.
+ Proof.
+   induction n.
+   simpl; auto with zarith.
+   destruct a; simpl; intros; auto with zarith; auto.
+ Qed.
+ 
+ Lemma Zgcd_alt_pos : forall a b, 0 <= Zgcd_alt a b.
+ Proof.
+   intros; unfold Zgcd; apply Zgcdn_pos; auto.
+ Qed.
+ 
+ (** We now prove that Zgcd is indeed a gcd. *)
+ 
+ (** 1) We prove a weaker & easier bound. *)
+ 
+ Lemma Zgcdn_linear_bound : forall n a b,
+   Zabs a < Z_of_nat n -> Zis_gcd a b (Zgcdn n a b).
+ Proof.
+   induction n.
+   simpl; intros.
+   elimtype False; generalize (Zabs_pos a); omega.
+   destruct a; intros; simpl;
+     [ generalize (Zis_gcd_0_abs b); intuition | | ];
+   unfold Zmod;
+   generalize (Z_div_mod b (Zpos p) (refl_equal Gt));
+   destruct (Zdiv_eucl b (Zpos p)) as (q,r);
+   intros (H0,H1);
+   rewrite inj_S in H; simpl Zabs in H;
+   (assert (H2: Zabs r < Z_of_nat n) by
+    (rewrite Zabs_eq; auto with zarith));
+    assert (IH:=IHn r (Zpos p) H2); clear IHn;
+    simpl in IH |- *;
+    rewrite H0.
+   apply Zis_gcd_for_euclid2; auto.
+   apply Zis_gcd_minus; apply Zis_gcd_sym.
+   apply Zis_gcd_for_euclid2; auto.
+ Qed.
+  	 
+ (** 2) For Euclid's algorithm, the worst-case situation corresponds
+    to Fibonacci numbers. Let's define them: *)
+ 
+ Fixpoint fibonacci (n:nat) : Z :=
+   match n with
+     | O => 1
+     | S O => 1
+     | S (S n as p) => fibonacci p + fibonacci n
+   end.
+  	 
+ Lemma fibonacci_pos : forall n, 0 <= fibonacci n.
+ Proof.
+   cut (forall N n, (n<N)%nat -> 0<=fibonacci n).
+   eauto.
+   induction N.
+   inversion 1.
+   intros.
+   destruct n.
+   simpl; auto with zarith.
+   destruct n.
+   simpl; auto with zarith.
+   change (0 <= fibonacci (S n) + fibonacci n).
+   generalize (IHN n) (IHN (S n)); omega.
+ Qed.
+ 
+ Lemma fibonacci_incr :
+   forall n m, (n<=m)%nat -> fibonacci n <= fibonacci m.
+ Proof.
+   induction 1.
+   auto with zarith.
+   apply Zle_trans with (fibonacci m); auto.
+   clear.
+   destruct m.
+   simpl; auto with zarith.
+   change (fibonacci (S m) <= fibonacci (S m)+fibonacci m).
+   generalize (fibonacci_pos m); omega.
+ Qed.
+ 
+ (** 3) We prove that fibonacci numbers are indeed worst-case:
+    for a given number [n], if we reach a conclusion about [gcd(a,b)] in
+    exactly [n+1] loops, then [fibonacci (n+1)<=a /\ fibonacci(n+2)<=b] *)
+ 
+ Lemma Zgcdn_worst_is_fibonacci : forall n a b,
+   0 < a < b ->
+   Zis_gcd a b (Zgcdn (S n) a b) ->
+   Zgcdn n a b <> Zgcdn (S n) a b ->
+   fibonacci (S n) <= a /\
+   fibonacci (S (S n)) <= b.
+ Proof.
+   induction n.
+   simpl; intros.
+   destruct a; omega.
+   intros.
+   destruct a; [simpl in *; omega| | destruct H; discriminate].
+   revert H1; revert H0.
+   set (m:=S n) in *; (assert (m=S n) by auto); clearbody m.
+   pattern m at 2; rewrite H0.
+   simpl Zgcdn.
+   unfold Zmod; generalize (Z_div_mod b (Zpos p) (refl_equal Gt)).
+   destruct (Zdiv_eucl b (Zpos p)) as (q,r).
+   intros (H1,H2).
+   destruct H2.
+   destruct (Zle_lt_or_eq _ _ H2).
+   generalize (IHn _ _ (conj H4 H3)).
+   intros H5 H6 H7.
+   replace (fibonacci (S (S m))) with (fibonacci (S m) + fibonacci m) by auto.
+   assert (r = Zpos p * (-q) + b) by (rewrite H1; ring).
+   destruct H5; auto.
+   pattern r at 1; rewrite H8.
+   apply Zis_gcd_sym.
+   apply Zis_gcd_for_euclid2; auto.
+   apply Zis_gcd_sym; auto.
+   split; auto.
+   rewrite H1.
+   apply Zplus_le_compat; auto.
+   apply Zle_trans with (Zpos p * 1); auto.
+   ring_simplify (Zpos p * 1); auto.
+   apply Zmult_le_compat_l.
+   destruct q.
+   omega.
+   assert (0 < Zpos p0) by (compute; auto).
+   omega.
+   assert (Zpos p * Zneg p0 < 0) by (compute; auto).
+   omega.
+   compute; intros; discriminate.
+   (* r=0 *)
+   subst r.
+   simpl; rewrite H0.
+   intros.
+   simpl in H4.
+   simpl in H5.
+   destruct n.
+   simpl in H5.
+   simpl.
+   omega.
+   simpl in H5.
+   elim H5; auto.
+ Qed.
+  	 
+ (** 3b) We reformulate the previous result in a more positive way. *)
+ 
+ Lemma Zgcdn_ok_before_fibonacci : forall n a b,
+   0 < a < b -> a < fibonacci (S n) ->
+   Zis_gcd a b (Zgcdn n a b).
+ Proof.
+   destruct a; [ destruct 1; elimtype False; omega | | destruct 1; discriminate].
+   cut (forall k n b,
+     k = (S (nat_of_P p) - n)%nat ->
+     0 < Zpos p < b -> Zpos p < fibonacci (S n) ->
+     Zis_gcd (Zpos p) b (Zgcdn n (Zpos p) b)).
+   destruct 2; eauto.
+   clear n; induction k.
+   intros.
+   assert (nat_of_P p < n)%nat by omega.
+   apply Zgcdn_linear_bound.
+   simpl.
+   generalize (inj_le _ _ H2).
+   rewrite inj_S.
+   rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto.
+   omega.
+   intros.
+   generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros.
+   assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)).
+   apply IHk; auto.
+   omega.
+   replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto.
+   generalize (fibonacci_pos n); omega.
+   replace (Zgcdn n (Zpos p) b) with (Zgcdn (S n) (Zpos p) b); auto.
+   generalize (H2 H3); clear H2 H3; omega.
+ Qed.
+ 
+ (** 4) The proposed bound leads to a fibonacci number that is big enough. *)
+ 
+ Lemma Zgcd_bound_fibonacci :
+   forall a, 0 < a -> a < fibonacci (Zgcd_bound a).
+ Proof.
+   destruct a; [omega| | intro H; discriminate].
+   intros _.
+   induction p; [ | | compute; auto ]; 
+    simpl Zgcd_bound in *;
+    rewrite plus_comm; simpl plus; 
+    set (n:= (Psize p+Psize p)%nat) in *; simpl;
+    assert (n <> O) by (unfold n; destruct p; simpl; auto).
+   
+   destruct n as [ |m]; [elim H; auto| ].
+   generalize (fibonacci_pos m); rewrite Zpos_xI; omega.
+
+   destruct n as [ |m]; [elim H; auto| ].
+   generalize (fibonacci_pos m); rewrite Zpos_xO; omega.
+ Qed.
+  	 
+ (* 5) the end: we glue everything together and take care of
+    situations not corresponding to [0<a<b]. *)
+
+ Lemma Zgcdn_is_gcd :
+   forall n a b, (Zgcd_bound a <= n)%nat -> 
+     Zis_gcd a b (Zgcdn n a b).
+ Proof.
+   destruct a; intros.
+   simpl in H.
+   destruct n; [elimtype False; omega | ].
+   simpl; generalize (Zis_gcd_0_abs b); intuition.
+   (*Zpos*)
+   generalize (Zgcd_bound_fibonacci (Zpos p)).
+   simpl Zgcd_bound in *.
+   remember (Psize p+Psize p)%nat as m.
+   assert (1 < m)%nat.
+     rewrite Heqm; destruct p; simpl; rewrite 1? plus_comm; 
+       auto with arith.
+   destruct m as [ |m]; [inversion H0; auto| ].
+   destruct n as [ |n]; [inversion H; auto| ].
+   simpl Zgcdn.
+   unfold Zmod.
+   generalize (Z_div_mod b (Zpos p) (refl_equal Gt)).
+   destruct (Zdiv_eucl b (Zpos p)) as (q,r).
+   intros (H2,H3) H4.
+   rewrite H2.
+   apply Zis_gcd_for_euclid2.
+   destruct H3.
+   destruct (Zle_lt_or_eq _ _ H1).
+   apply Zgcdn_ok_before_fibonacci; auto.
+   apply Zlt_le_trans with (fibonacci (S m)); [ omega | apply fibonacci_incr; auto].
+   subst r; simpl.
+   destruct m as [ |m]; [elimtype False; omega| ].
+   destruct n as [ |n]; [elimtype False; omega| ].
+   simpl; apply Zis_gcd_sym; apply Zis_gcd_0.
+   (*Zneg*)
+   generalize (Zgcd_bound_fibonacci (Zpos p)).
+   simpl Zgcd_bound in *.
+   remember (Psize p+Psize p)%nat as m.
+   assert (1 < m)%nat.
+     rewrite Heqm; destruct p; simpl; rewrite 1? plus_comm; 
+       auto with arith.
+   destruct m as [ |m]; [inversion H0; auto| ].
+   destruct n as [ |n]; [inversion H; auto| ].
+   simpl Zgcdn.
+   unfold Zmod.
+   generalize (Z_div_mod b (Zpos p) (refl_equal Gt)).
+   destruct (Zdiv_eucl b (Zpos p)) as (q,r).
+   intros (H1,H2) H3.
+   rewrite H1.
+   apply Zis_gcd_minus.
+   apply Zis_gcd_sym.
+   apply Zis_gcd_for_euclid2.
+   destruct H2.
+   destruct (Zle_lt_or_eq _ _ H2).
+   apply Zgcdn_ok_before_fibonacci; auto.
+   apply Zlt_le_trans with (fibonacci (S m)); [ omega | apply fibonacci_incr; auto].
+   subst r; simpl.
+   destruct m as [ |m]; [elimtype False; omega| ].
+   destruct n as [ |n]; [elimtype False; omega| ].
+   simpl; apply Zis_gcd_sym; apply Zis_gcd_0.
+ Qed.
+ 
+ Lemma Zgcd_is_gcd :
+   forall a b, Zis_gcd a b (Zgcd_alt a b).
+ Proof.
+  unfold Zgcd_alt; intros; apply Zgcdn_is_gcd; auto.
+ Qed.
+
+
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index 8af9b891..0d6fc94a 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*i $Id: Zmax.v 9302 2006-10-27 21:21:17Z barras $ i*)
+(*i $Id: Zmax.v 10291 2007-11-06 02:18:53Z letouzey $ i*)
 
 Require Import Arith_base.
 Require Import BinInt.
@@ -38,6 +38,28 @@ Proof.
   destruct (n ?= m); (apply H1|| apply H2); discriminate. 
 Qed.
 
+Lemma Zmax_spec : forall x y:Z, 
+  x >= y /\ Zmax x y = x  \/
+  x < y /\ Zmax x y = y.
+Proof.
+ intros; unfold Zmax, Zlt, Zge.
+ destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate.
+Qed.
+
+Lemma Zmax_left : forall n m:Z, n>=m -> Zmax n m = n.
+Proof.
+  intros n m; unfold Zmax, Zge; destruct (n ?= m); auto.
+  intro H; elim H; auto.
+Qed.
+
+Lemma Zmax_right : forall n m:Z, n<=m -> Zmax n m = m.
+Proof.
+  intros n m; unfold Zmax, Zle.
+  generalize (Zcompare_Eq_eq n m).
+  destruct (n ?= m); auto.
+  intros _ H; elim H; auto.
+Qed.
+
 (** * Least upper bound properties of max *)
 
 Lemma Zle_max_l : forall n m:Z, n <= Zmax n m.
@@ -106,3 +128,39 @@ Proof.
     rewrite (Zcompare_plus_compat x y n).
   case (x ?= y); apply Zplus_comm.
 Qed.
+
+(** * Maximum and Zpos *)
+
+Lemma Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q).
+Proof.
+  intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q).
+  destruct Pcompare; auto.
+  intro H; rewrite H; auto.
+Qed.
+
+Lemma Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p.
+Proof.
+  intros; unfold Zmax; simpl; destruct p; simpl; auto.
+Qed.
+
+(** * Characterization of Pminus in term of Zminus and Zmax *)
+
+Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).
+Proof.
+  intros.
+  case_eq (Pcompare p q Eq).
+  intros H; rewrite (Pcompare_Eq_eq _ _ H).
+  rewrite Zminus_diag.
+  unfold Zmax; simpl.
+  unfold Pminus; rewrite Pminus_mask_diag; auto.
+  intros; rewrite Pminus_Lt; auto.
+  destruct (Zmax_spec 1 (Zpos p - Zpos q)) as [(H1,H2)|(H1,H2)]; auto.
+  elimtype False; clear H2.
+  assert (H1':=Zlt_trans 0 1 _ Zlt_0_1 H1).
+  generalize (Zlt_0_minus_lt _ _ H1').
+  unfold Zlt; simpl.
+  rewrite (ZC2 _ _ H); intro; discriminate.
+  intros; simpl; rewrite H.
+  symmetry; apply Zpos_max_1.
+Qed.
+
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index 37d78a74..bad40a32 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -5,9 +5,9 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*i $Id: Zmin.v 9302 2006-10-27 21:21:17Z barras $ i*)
+(*i $Id: Zmin.v 10028 2007-07-18 22:38:06Z letouzey $ i*)
 
-(** Initial version from Pierre Crégut (CNET, Lannion, France), 1996.
+(** Initial version from Pierre Crégut (CNET, Lannion, France), 1996.
     Further extensions by the Coq development team, with suggestions
     from Russell O'Connor (Radbout U., Nijmegen, The Netherlands).
  *)
@@ -43,6 +43,14 @@ Proof.
   intros n m P H1 H2; unfold Zmin in |- *; case (n ?= m); auto with arith.
 Qed.
 
+Lemma Zmin_spec : forall x y:Z, 
+  x <= y /\ Zmin x y = x  \/
+  x > y /\ Zmin x y = y.
+Proof.
+ intros; unfold Zmin, Zle, Zgt.
+ destruct (Zcompare x y); [ left | left | right ]; split; auto; discriminate.
+Qed.
+
 (** * Greatest lower bound properties of min *)
 
 Lemma Zle_min_l : forall n m:Z, Zmin n m <= n.
@@ -128,3 +136,11 @@ Proof.
 Qed.
 
 Notation Zmin_plus := Zplus_min_distr_r (only parsing).
+
+(** * Minimum and Zpos *)
+
+Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q).
+Proof.
+  intros; unfold Zmin, Pmin; simpl; destruct Pcompare; auto.
+Qed.
+
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index d01cada6..0634096e 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -6,8 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Zmisc.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Zmisc.v 11072 2008-06-08 16:13:37Z herbelin $ i*)
 
+Require Import Wf_nat.
 Require Import BinInt.
 Require Import Zcompare.
 Require Import Zorder.
@@ -18,37 +19,23 @@ Open Local Scope Z_scope.
 (** Iterators *)
 
 (** [n]th iteration of the function [f] *)
-Fixpoint iter_nat (n:nat) (A:Set) (f:A -> A) (x:A) {struct n} : A :=
-  match n with
-    | O => x
-    | S n' => f (iter_nat n' A f x)
-  end.
 
-Fixpoint iter_pos (n:positive) (A:Set) (f:A -> A) (x:A) {struct n} : A :=
+Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) {struct n} : A :=
   match n with
     | xH => f x
     | xO n' => iter_pos n' A f (iter_pos n' A f x)
     | xI n' => f (iter_pos n' A f (iter_pos n' A f x))
   end.
 
-Definition iter (n:Z) (A:Set) (f:A -> A) (x:A) :=
+Definition iter (n:Z) (A:Type) (f:A -> A) (x:A) :=
   match n with
     | Z0 => x
     | Zpos p => iter_pos p A f x
     | Zneg p => x
   end.
 
-Theorem iter_nat_plus :
-  forall (n m:nat) (A:Set) (f:A -> A) (x:A),
-    iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x).
-Proof.    
-  simple induction n;
-    [ simpl in |- *; auto with arith
-      | intros; simpl in |- *; apply f_equal with (f := f); apply H ].  
-Qed.
-
 Theorem iter_nat_of_P :
-  forall (p:positive) (A:Set) (f:A -> A) (x:A),
+  forall (p:positive) (A:Type) (f:A -> A) (x:A),
     iter_pos p A f x = iter_nat (nat_of_P p) A f x.
 Proof.    
   intro n; induction n as [p H| p H| ];
@@ -63,7 +50,7 @@ Proof.
 Qed.
 
 Theorem iter_pos_plus :
-  forall (p q:positive) (A:Set) (f:A -> A) (x:A),
+  forall (p q:positive) (A:Type) (f:A -> A) (x:A),
     iter_pos (p + q) A f x = iter_pos p A f (iter_pos q A f x).
 Proof.    
   intros n m; intros.
@@ -78,7 +65,7 @@ Qed.
     then the iterates of [f] also preserve it. *)
 
 Theorem iter_nat_invariant :
-  forall (n:nat) (A:Set) (f:A -> A) (Inv:A -> Prop),
+  forall (n:nat) (A:Type) (f:A -> A) (Inv:A -> Prop),
     (forall x:A, Inv x -> Inv (f x)) ->
     forall x:A, Inv x -> Inv (iter_nat n A f x).
 Proof.    
@@ -89,7 +76,7 @@ Proof.
 Qed.
 
 Theorem iter_pos_invariant :
-  forall (p:positive) (A:Set) (f:A -> A) (Inv:A -> Prop),
+  forall (p:positive) (A:Type) (f:A -> A) (Inv:A -> Prop),
     (forall x:A, Inv x -> Inv (f x)) ->
     forall x:A, Inv x -> Inv (iter_pos p A f x).
 Proof.    
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index f0a3d47b..c5b5edc1 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Znat.v 9302 2006-10-27 21:21:17Z barras $ i*)
+(*i $Id: Znat.v 10726 2008-03-28 18:15:23Z notin $ i*)
 
-(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 
 Require Export Arith_base.
 Require Import BinPos.
@@ -17,6 +17,7 @@ Require Import Zcompare.
 Require Import Zorder.
 Require Import Decidable.
 Require Import Peano_dec.
+Require Import Min Max Zmin Zmax.
 Require Export Compare_dec.
 
 Open Local Scope Z_scope.
@@ -26,6 +27,13 @@ Definition neq (x y:nat) := x <> y.
 (************************************************)
 (** Properties of the injection from nat into Z *)
 
+(** Injection and successor *)
+
+Theorem inj_0 : Z_of_nat 0 = 0%Z.
+Proof.
+  reflexivity.
+Qed.
+
 Theorem inj_S : forall n:nat, Z_of_nat (S n) = Zsucc (Z_of_nat n).
 Proof.
   intro y; induction y as [| n H];
@@ -33,25 +41,12 @@ Proof.
       | change (Zpos (Psucc (P_of_succ_nat n)) = Zsucc (Z_of_nat (S n))) in |- *;
 	rewrite Zpos_succ_morphism; trivial with arith ].
 Qed.
- 
-Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m.
-Proof.
-  intro x; induction x as [| n H]; intro y; destruct y as [| m];
-    [ simpl in |- *; trivial with arith
-      | simpl in |- *; trivial with arith
-      | simpl in |- *; rewrite <- plus_n_O; trivial with arith
-      | change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *;
-	rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l;
-	  trivial with arith ].
-Qed.
 
-Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m.
+(** Injection and equality. *)
+
+Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m.
 Proof.
-  intro x; induction x as [| n H];
-    [ simpl in |- *; trivial with arith
-      | intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H;
-	rewrite <- inj_plus; simpl in |- *; rewrite plus_comm; 
-	  trivial with arith ].
+  intros x y H; rewrite H; trivial with arith.
 Qed.
 
 Theorem inj_neq : forall n m:nat, neq n m -> Zne (Z_of_nat n) (Z_of_nat m).
@@ -66,6 +61,24 @@ Proof.
 	    intros E; rewrite E; auto with arith ].
 Qed. 
 
+Theorem inj_eq_rev : forall n m:nat, Z_of_nat n = Z_of_nat m -> n = m.
+Proof.
+  intros x y H.
+  destruct (eq_nat_dec x y) as [H'|H']; auto.
+  elimtype False.
+  exact (inj_neq _ _ H' H).
+Qed.
+
+Theorem inj_eq_iff : forall n m:nat, n=m <-> Z_of_nat n = Z_of_nat m.
+Proof.
+ split; [apply inj_eq | apply inj_eq_rev].
+Qed.
+
+
+(** Injection and order relations: *)
+
+(** One way ... *)
+
 Theorem inj_le : forall n m:nat, (n <= m)%nat -> Z_of_nat n <= Z_of_nat m.
 Proof.
   intros x y; intros H; elim H;
@@ -81,29 +94,100 @@ Proof.
     exact H.
 Qed.
 
+Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m.
+Proof.
+  intros x y H; apply Zle_ge; apply inj_le; apply H.
+Qed.
+
 Theorem inj_gt : forall n m:nat, (n > m)%nat -> Z_of_nat n > Z_of_nat m.
 Proof.
   intros x y H; apply Zlt_gt; apply inj_lt; exact H.
 Qed.
 
-Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m.
+(** The other way ... *)
+
+Theorem inj_le_rev : forall n m:nat, Z_of_nat n <= Z_of_nat m -> (n <= m)%nat.
 Proof.
-  intros x y H; apply Zle_ge; apply inj_le; apply H.
+  intros x y H.
+  destruct (le_lt_dec x y) as [H0|H0]; auto.
+  elimtype False.
+  assert (H1:=inj_lt _ _ H0).
+  red in H; red in H1.
+  rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto.
 Qed.
 
-Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m.
+Theorem inj_lt_rev : forall n m:nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat.
 Proof.
-  intros x y H; rewrite H; trivial with arith.
+  intros x y H.
+  destruct (le_lt_dec y x) as [H0|H0]; auto.
+  elimtype False.
+  assert (H1:=inj_le _ _ H0).
+  red in H; red in H1.
+  rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto.
 Qed.
 
-Theorem intro_Z :
-  forall n:nat,  exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0.
+Theorem inj_ge_rev : forall n m:nat, Z_of_nat n >= Z_of_nat m -> (n >= m)%nat.
 Proof.
-  intros x; exists (Z_of_nat x); split;
-    [ trivial with arith
-      | rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r;
-	unfold Zle in |- *; elim x; intros; simpl in |- *; 
-          discriminate ].
+  intros x y H.
+  destruct (le_lt_dec y x) as [H0|H0]; auto.
+  elimtype False.
+  assert (H1:=inj_gt _ _ H0).
+  red in H; red in H1.
+  rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto.
+Qed.
+
+Theorem inj_gt_rev : forall n m:nat, Z_of_nat n > Z_of_nat m -> (n > m)%nat.
+Proof.
+  intros x y H.
+  destruct (le_lt_dec x y) as [H0|H0]; auto.
+  elimtype False.
+  assert (H1:=inj_ge _ _ H0).
+  red in H; red in H1.
+  rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto.
+Qed.
+
+(* Both ways ... *)
+
+Theorem inj_le_iff : forall n m:nat, (n<=m)%nat <-> Z_of_nat n <= Z_of_nat m.
+Proof.
+ split; [apply inj_le | apply inj_le_rev].
+Qed.
+
+Theorem inj_lt_iff : forall n m:nat, (n<m)%nat <-> Z_of_nat n < Z_of_nat m.
+Proof.
+ split; [apply inj_lt | apply inj_lt_rev].
+Qed.
+
+Theorem inj_ge_iff : forall n m:nat, (n>=m)%nat <-> Z_of_nat n >= Z_of_nat m.
+Proof.
+ split; [apply inj_ge | apply inj_ge_rev].
+Qed.
+
+Theorem inj_gt_iff : forall n m:nat, (n>m)%nat <-> Z_of_nat n > Z_of_nat m.
+Proof.
+ split; [apply inj_gt | apply inj_gt_rev].
+Qed.
+
+(** Injection and usual operations *)
+ 
+Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m.
+Proof.
+  intro x; induction x as [| n H]; intro y; destruct y as [| m];
+    [ simpl in |- *; trivial with arith
+      | simpl in |- *; trivial with arith
+      | simpl in |- *; rewrite <- plus_n_O; trivial with arith
+      | change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *;
+	rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l;
+	  trivial with arith ].
+Qed.
+
+Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m.
+Proof.
+  intro x; induction x as [| n H];
+    [ simpl in |- *; trivial with arith
+      | intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H;
+	rewrite <- inj_plus; simpl in |- *; rewrite plus_comm; 
+	  trivial with arith ].
 Qed.
 
 Theorem inj_minus1 :
@@ -121,6 +205,46 @@ Proof.
     [ trivial with arith | apply gt_not_le; assumption ].
 Qed.
 
+Theorem inj_minus : forall n m:nat, 
+ Z_of_nat (minus n m) = Zmax 0 (Z_of_nat n - Z_of_nat m).
+Proof.
+ intros.
+ rewrite Zmax_comm.
+ unfold Zmax.
+ destruct (le_lt_dec m n) as [H|H].
+
+ rewrite (inj_minus1 _ _ H).
+ assert (H':=Zle_minus_le_0 _ _ (inj_le _ _ H)).
+ unfold Zle in H'.
+ rewrite <- Zcompare_antisym in H'.
+ destruct Zcompare; simpl in *; intuition.
+
+ rewrite (inj_minus2 _ _ H).
+ assert (H':=Zplus_lt_compat_r _ _ (- Z_of_nat m) (inj_lt _ _ H)).
+ rewrite Zplus_opp_r in H'.
+ unfold Zminus; rewrite H'; auto.
+Qed.
+
+Theorem inj_min : forall n m:nat, 
+  Z_of_nat (min n m) = Zmin (Z_of_nat n) (Z_of_nat m).
+Proof.
+ induction n; destruct m; try (compute; auto; fail).
+ simpl min.
+ do 3 rewrite inj_S.
+ rewrite <- Zsucc_min_distr; f_equal; auto.
+Qed.
+
+Theorem inj_max : forall n m:nat, 
+  Z_of_nat (max n m) = Zmax (Z_of_nat n) (Z_of_nat m).
+Proof.
+ induction n; destruct m; try (compute; auto; fail).
+ simpl max.
+ do 3 rewrite inj_S.
+ rewrite <- Zsucc_max_distr; f_equal; auto.
+Qed.
+
+(** Composition of injections **)
+
 Theorem Zpos_eq_Z_of_nat_o_nat_of_P :
   forall p:positive, Zpos p = Z_of_nat (nat_of_P p).
 Proof.
@@ -136,3 +260,26 @@ Proof.
   rewrite inj_plus; repeat rewrite <- H.
   rewrite Zpos_xO; simpl in |- *; rewrite Pplus_diag; reflexivity.
 Qed.
+
+(** Misc *)
+
+Theorem intro_Z :
+  forall n:nat,  exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0.
+Proof.
+  intros x; exists (Z_of_nat x); split;
+    [ trivial with arith
+      | rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r;
+	unfold Zle in |- *; elim x; intros; simpl in |- *; 
+          discriminate ].
+Qed.
+
+Lemma Zpos_P_of_succ_nat : forall n:nat, 
+ Zpos (P_of_succ_nat n) = Zsucc (Z_of_nat n).
+Proof.
+  intros.
+  unfold Z_of_nat.
+  destruct n.
+  simpl; auto.
+  simpl (P_of_succ_nat (S n)).
+  apply Zpos_succ_morphism.
+Qed.
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index d89ec052..e77475e0 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -6,13 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Znumtheory.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Znumtheory.v 10295 2007-11-06 22:46:21Z letouzey $ i*)
 
 Require Import ZArith_base.
 Require Import ZArithRing.
 Require Import Zcomplements.
 Require Import Zdiv.
-Require Import Ndigits.
 Require Import Wf_nat.
 Open Local Scope Z_scope.
 
@@ -156,21 +155,27 @@ Qed.
 
 Lemma Zdivide_antisym : forall a b:Z, (a | b) -> (b | a) -> a = b \/ a = - b.
 Proof.
-simple induction 1; intros.
-inversion H1.
-rewrite H0 in H2; clear H H1.
-case (Z_zerop a); intro.
-left; rewrite H0; rewrite e; ring.
-assert (Hqq0 : q0 * q = 1).
-apply Zmult_reg_l with a.
-assumption.
-ring_simplify.
-pattern a at 2 in |- *; rewrite H2; ring.
-assert (q | 1).
-rewrite <- Hqq0; auto with zarith.
-elim (Zdivide_1 q H); intros.
-rewrite H1 in H0; left; omega.
-rewrite H1 in H0; right; omega.
+  simple induction 1; intros.
+  inversion H1.
+  rewrite H0 in H2; clear H H1.
+  case (Z_zerop a); intro.
+  left; rewrite H0; rewrite e; ring.
+  assert (Hqq0 : q0 * q = 1).
+  apply Zmult_reg_l with a.
+  assumption.
+  ring_simplify.
+  pattern a at 2 in |- *; rewrite H2; ring.
+  assert (q | 1).
+  rewrite <- Hqq0; auto with zarith.
+  elim (Zdivide_1 q H); intros.
+  rewrite H1 in H0; left; omega.
+  rewrite H1 in H0; right; omega.
+Qed.
+ 
+Theorem Zdivide_trans: forall a b c, (a | b) -> (b | c) ->  (a | c).
+Proof.
+  intros a b c [d H1] [e H2]; exists (d * e); auto with zarith.
+  rewrite H2; rewrite H1; ring.
 Qed.
 
 (** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *)
@@ -194,6 +199,134 @@ Proof.
   subst q; omega.
 Qed.
 
+(** [Zdivide] can be expressed using [Zmod]. *)
+
+Lemma Zmod_divide : forall a b:Z, b > 0 -> a mod b = 0 -> (b | a).
+Proof.
+  intros a b H H0.
+  apply Zdivide_intro with (a / b).
+  pattern a at 1 in |- *; rewrite (Z_div_mod_eq a b H).
+  rewrite H0; ring.
+Qed.
+
+Lemma Zdivide_mod : forall a b:Z, b > 0 -> (b | a) -> a mod b = 0.
+Proof.
+  intros a b; simple destruct 2; intros; subst.
+  change (q * b) with (0 + q * b) in |- *.
+  rewrite Z_mod_plus; auto.
+Qed.
+
+(** [Zdivide] is hence decidable *)
+
+Lemma Zdivide_dec : forall a b:Z, {(a | b)} + {~ (a | b)}.
+Proof.
+  intros a b; elim (Ztrichotomy_inf a 0).
+  (* a<0 *)
+  intros H; elim H; intros. 
+  case (Z_eq_dec (b mod - a) 0).
+  left; apply Zdivide_opp_l_rev; apply Zmod_divide; auto with zarith.
+  intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith.
+  (* a=0 *)
+  case (Z_eq_dec b 0); intro.
+  left; subst; auto with zarith.
+  right; subst; intro H0; inversion H0; omega.
+  (* a>0 *)
+  intro H; case (Z_eq_dec (b mod a) 0).
+  left; apply Zmod_divide; auto with zarith.
+  intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith.
+Qed.
+
+Theorem Zdivide_Zdiv_eq: forall a b : Z, 
+ 0 < a -> (a | b) ->  b = a * (b / a).
+Proof.
+  intros a b Hb Hc.
+  pattern b at 1; rewrite (Z_div_mod_eq b a); auto with zarith.
+  rewrite (Zdivide_mod b a); auto with zarith.
+Qed.
+
+Theorem Zdivide_Zdiv_eq_2: forall a b c : Z, 
+ 0 < a -> (a | b) -> (c * b)/a = c * (b / a).
+Proof.
+  intros a b c H1 H2.
+  inversion H2 as [z Hz].
+  rewrite Hz; rewrite Zmult_assoc.
+  repeat rewrite Z_div_mult; auto with zarith.
+Qed.
+ 
+Theorem Zdivide_Zabs_l: forall a b, (Zabs a | b) ->  (a | b).
+Proof.
+  intros a b [x H]; subst b.
+  pattern (Zabs a); apply Zabs_intro.
+  exists (- x); ring.
+  exists x; ring.
+Qed.
+ 
+Theorem Zdivide_Zabs_inv_l: forall a b, (a | b) ->  (Zabs a | b).
+Proof.
+  intros a b [x H]; subst b.
+  pattern (Zabs a); apply Zabs_intro.
+  exists (- x);  ring.
+  exists x; ring.
+Qed.
+
+Theorem Zdivide_le: forall a b : Z, 
+ 0 <= a -> 0 < b -> (a | b) ->  a <= b.
+Proof.
+  intros a b H1 H2 [q H3]; subst b.
+  case (Zle_lt_or_eq 0 a); auto with zarith; intros H3.
+  case (Zle_lt_or_eq 0 q); auto with zarith.
+  apply (Zmult_le_0_reg_r a); auto with zarith.
+  intros H4; apply Zle_trans with (1 * a); auto with zarith.
+  intros H4; subst q; omega.
+Qed.
+
+Theorem Zdivide_Zdiv_lt_pos: forall a b : Z, 
+ 1 < a -> 0 < b -> (a | b) ->  0 < b / a < b .
+Proof.
+  intros a b H1 H2 H3; split.
+  apply Zmult_lt_reg_r with a; auto with zarith.
+  rewrite (Zmult_comm (Zdiv b a)); rewrite <- Zdivide_Zdiv_eq; auto with zarith.
+  apply Zmult_lt_reg_r with a; auto with zarith.
+  repeat rewrite (fun x => Zmult_comm x a); auto with zarith.
+  rewrite <- Zdivide_Zdiv_eq; auto with zarith.
+  pattern b at 1; replace b with (1 * b); auto with zarith.
+  apply Zmult_lt_compat_r; auto with zarith.
+Qed.
+
+Lemma Zmod_div_mod: forall n m a, 0 < n -> 0 < m ->
+ (n | m) -> a mod n = (a mod m) mod n.
+Proof.
+  intros n m a H1 H2 H3.
+  pattern a at 1; rewrite (Z_div_mod_eq a m); auto with zarith.
+  case H3; intros q Hq; pattern m at 1; rewrite Hq.
+  rewrite (Zmult_comm q).
+  rewrite Zplus_mod; auto with zarith.
+  rewrite <- Zmult_assoc; rewrite Zmult_mod; auto with zarith.
+  rewrite Z_mod_same; try rewrite Zmult_0_l; auto with zarith.
+  rewrite (Zmod_small 0); auto with zarith.
+  rewrite Zplus_0_l; rewrite Zmod_mod; auto with zarith.
+Qed.
+
+Lemma Zmod_divide_minus: forall a b c : Z, 0 < b -> 
+ a mod b = c -> (b | a - c).
+Proof.
+  intros a b c H H1; apply Zmod_divide; auto with zarith.
+  rewrite Zminus_mod; auto with zarith.
+  rewrite H1; pattern c at 1; rewrite <- (Zmod_small c b); auto with zarith.
+  rewrite Zminus_diag; apply Zmod_small; auto with zarith.
+  subst; apply Z_mod_lt; auto with zarith.
+Qed.
+
+Lemma Zdivide_mod_minus: forall a b c : Z, 0 <= c < b -> 
+ (b | a - c) -> a mod b = c.
+Proof.
+  intros a b c (H1, H2) H3; assert (0 < b); try apply Zle_lt_trans with c; auto.
+  replace a with ((a - c) + c); auto with zarith.
+  rewrite Zplus_mod; auto with zarith.
+  rewrite (Zdivide_mod (a -c) b); try rewrite Zplus_0_l; auto with zarith.
+  rewrite Zmod_mod; try apply Zmod_small; auto with zarith.
+Qed.
+
 (** * Greatest common divisor (gcd). *)
    
 (** There is no unicity of the gcd; hence we define the predicate [gcd a b d] 
@@ -246,6 +379,18 @@ Proof.
 Qed.
 
 Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith.
+ 
+Theorem Zis_gcd_unique: forall a b c d : Z, 
+ Zis_gcd a b c -> Zis_gcd a b d ->  c = d \/ c = (- d).
+Proof.
+intros a b c d H1 H2.
+inversion_clear H1 as [Hc1 Hc2 Hc3].
+inversion_clear H2 as [Hd1 Hd2 Hd3].
+assert (H3: Zdivide c d); auto.
+assert (H4: Zdivide d c); auto.
+apply Zdivide_antisym; auto.
+Qed.
+
 
 (** * Extended Euclid algorithm. *)
 
@@ -463,6 +608,7 @@ Qed.
 Lemma Zis_gcd_rel_prime :
   forall a b g:Z,
     b > 0 -> g >= 0 -> Zis_gcd a b g -> rel_prime (a / g) (b / g).
+Proof.
   intros a b g; intros.
   assert (g <> 0).
   intro.
@@ -491,6 +637,68 @@ Lemma Zis_gcd_rel_prime :
   exists q; auto with zarith.
 Qed.
 
+Theorem rel_prime_sym: forall a b, rel_prime a b -> rel_prime b a.
+Proof.
+  intros a b H; auto with zarith.
+  red; apply Zis_gcd_sym; auto with zarith.
+Qed.
+
+Theorem rel_prime_div: forall p q r, 
+ rel_prime p q -> (r | p) -> rel_prime r q.
+Proof.
+  intros p q r H (u, H1); subst.
+  inversion_clear H as [H1 H2 H3].
+  red; apply Zis_gcd_intro; try apply Zone_divide.
+  intros x H4 H5; apply H3; auto.
+  apply Zdivide_mult_r; auto.
+Qed.
+
+Theorem rel_prime_1: forall n, rel_prime 1 n.
+Proof.
+  intros n; red; apply Zis_gcd_intro; auto.
+  exists 1; auto with zarith.
+  exists n; auto with zarith.
+Qed.
+
+Theorem not_rel_prime_0: forall n, 1 < n -> ~ rel_prime 0 n.
+Proof.
+  intros n H H1; absurd (n = 1 \/ n = -1).
+  intros [H2 | H2]; subst; contradict H; auto with zarith.
+  case (Zis_gcd_unique  0 n n 1); auto.
+  apply Zis_gcd_intro; auto.
+  exists 0; auto with zarith.
+  exists 1; auto with zarith.
+Qed.
+
+Theorem rel_prime_mod: forall p q, 0 < q -> 
+ rel_prime p q -> rel_prime (p mod q) q.
+Proof.
+  intros p q H H0.
+  assert (H1: Bezout p q 1).
+  apply rel_prime_bezout; auto.
+  inversion_clear H1 as [q1 r1 H2].
+  apply bezout_rel_prime.
+  apply Bezout_intro with q1  (r1 + q1 * (p / q)).
+  rewrite <- H2.
+  pattern p at 3; rewrite (Z_div_mod_eq p q); try ring; auto with zarith.
+Qed.
+
+Theorem rel_prime_mod_rev: forall p q, 0 < q -> 
+ rel_prime (p mod q) q -> rel_prime p q.
+Proof.
+  intros p q H H0.
+  rewrite (Z_div_mod_eq p q); auto with zarith; red.
+  apply Zis_gcd_sym; apply Zis_gcd_for_euclid2; auto with zarith.
+Qed.
+
+Theorem Zrel_prime_neq_mod_0: forall a b, 1 < b -> rel_prime a b -> a mod b <> 0.
+Proof.
+  intros a b H H1 H2.
+  case (not_rel_prime_0 _ H).
+  rewrite <- H2.
+  apply rel_prime_mod; auto with zarith.
+Qed.
+
 (** * Primality *)
 
 Inductive prime (p:Z) : Prop :=
@@ -543,42 +751,19 @@ Qed.
 
 Hint Resolve prime_rel_prime: zarith.
 
-(** [Zdivide] can be expressed using [Zmod]. *)
+(** As a consequence, a prime number is relatively prime with smaller numbers *)
 
-Lemma Zmod_divide : forall a b:Z, b > 0 -> a mod b = 0 -> (b | a).
+Theorem rel_prime_le_prime:
+ forall a p, prime p -> 1 <=  a < p -> rel_prime a p.
 Proof.
-  intros a b H H0.
-  apply Zdivide_intro with (a / b).
-  pattern a at 1 in |- *; rewrite (Z_div_mod_eq a b H).
-  rewrite H0; ring.
+  intros a p Hp [H1 H2].
+  apply rel_prime_sym; apply prime_rel_prime; auto.
+  intros [q Hq]; subst a.
+  case (Zle_or_lt q 0); intros Hl.
+  absurd (q * p <= 0 * p); auto with zarith.
+  absurd (1 * p <= q * p); auto with zarith.
 Qed.
 
-Lemma Zdivide_mod : forall a b:Z, b > 0 -> (b | a) -> a mod b = 0.
-Proof.
-  intros a b; simple destruct 2; intros; subst.
-  change (q * b) with (0 + q * b) in |- *.
-  rewrite Z_mod_plus; auto.
-Qed.
-
-(** [Zdivide] is hence decidable *)
-
-Lemma Zdivide_dec : forall a b:Z, {(a | b)} + {~ (a | b)}.
-Proof.
-  intros a b; elim (Ztrichotomy_inf a 0).
-  (* a<0 *)
-  intros H; elim H; intros. 
-  case (Z_eq_dec (b mod - a) 0).
-  left; apply Zdivide_opp_l_rev; apply Zmod_divide; auto with zarith.
-  intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith.
-  (* a=0 *)
-  case (Z_eq_dec b 0); intro.
-  left; subst; auto with zarith.
-  right; subst; intro H0; inversion H0; omega.
-  (* a>0 *)
-  intro H; case (Z_eq_dec (b mod a) 0).
-  left; apply Zmod_divide; auto with zarith.
-  intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith.
-Qed.
 
 (** If a prime [p] divides [ab] then it divides either [a] or [b] *)
 
@@ -590,6 +775,108 @@ Proof.
   right; apply Gauss with a; auto with zarith.
 Qed.
 
+Lemma not_prime_0: ~ prime 0.
+Proof.
+  intros H1; case (prime_divisors _ H1 2); auto with zarith.
+Qed.
+
+Lemma not_prime_1: ~ prime 1.
+Proof.
+  intros H1; absurd (1 < 1); auto with zarith.
+  inversion H1; auto.
+Qed.
+ 
+Lemma prime_2: prime 2.
+Proof.
+  apply prime_intro; auto with zarith.
+  intros n [H1 H2]; case Zle_lt_or_eq with ( 1 := H1 ); auto with zarith;
+   clear H1; intros H1.
+  contradict H2; auto with zarith.
+  subst n; red; auto with zarith.
+  apply Zis_gcd_intro; auto with zarith.
+Qed.
+ 
+Theorem prime_3: prime 3.
+Proof.
+  apply prime_intro; auto with zarith.
+  intros n [H1 H2]; case Zle_lt_or_eq with ( 1 := H1 ); auto with zarith;
+   clear H1; intros H1.
+  case (Zle_lt_or_eq 2 n); auto with zarith; clear H1; intros H1.
+  contradict H2; auto with zarith.
+  subst n; red; auto with zarith.
+  apply Zis_gcd_intro; auto with zarith.
+  intros x [q1 Hq1] [q2 Hq2].
+  exists (q2 - q1).
+  apply trans_equal with (3 - 2); auto with zarith.
+  rewrite Hq1; rewrite Hq2; ring.
+  subst n; red; auto with zarith.
+  apply Zis_gcd_intro; auto with zarith.
+Qed.
+ 
+Theorem prime_ge_2: forall p, prime p ->  2 <= p.
+Proof.
+  intros p Hp; inversion Hp; auto with zarith.
+Qed.
+
+Definition prime' p := 1<p /\ (forall n, 1<n<p -> ~ (n|p)).
+
+Theorem prime_alt: 
+ forall p, prime' p <-> prime p.
+Proof.
+  split; destruct 1; intros.
+  (* prime -> prime' *)
+  constructor; auto; intros.
+  red; apply Zis_gcd_intro; auto with zarith; intros.
+  case (Zle_lt_or_eq 0 (Zabs x)); auto with zarith; intros H6.
+  case (Zle_lt_or_eq 1 (Zabs x)); auto with zarith; intros H7.
+  case (Zle_lt_or_eq (Zabs x) p); auto with zarith.
+  apply Zdivide_le; auto with zarith.
+  apply Zdivide_Zabs_inv_l; auto.
+  intros H8; case (H0 (Zabs x)); auto.
+  apply Zdivide_Zabs_inv_l; auto.
+  intros H8; subst p; absurd (Zabs x <= n); auto with zarith.
+  apply Zdivide_le; auto with zarith.
+  apply Zdivide_Zabs_inv_l; auto.
+  rewrite H7; pattern (Zabs x); apply Zabs_intro; auto with zarith.
+  absurd (0%Z = p); auto with zarith.
+  assert (x=0) by (destruct x; simpl in *; now auto).
+  subst x; elim H3; intro q; rewrite Zmult_0_r; auto.
+  (* prime' -> prime *)
+  split; auto; intros.
+  intros H2.
+  case (Zis_gcd_unique n p n 1); auto with zarith.
+  apply Zis_gcd_intro; auto with zarith.
+  apply H0; auto with zarith.
+Qed.
+ 
+Theorem square_not_prime: forall a, ~ prime (a * a).
+Proof.
+  intros a Ha.
+  rewrite <- (Zabs_square a) in Ha.
+  assert (0 <= Zabs a) by auto with zarith.
+  set (b:=Zabs a) in *; clearbody b.
+  rewrite <- prime_alt in Ha; destruct Ha.
+  case (Zle_lt_or_eq 0 b); auto with zarith; intros Hza1; [ | subst; omega].
+  case (Zle_lt_or_eq 1 b); auto with zarith; intros Hza2; [ | subst; omega].
+  assert (Hza3 := Zmult_lt_compat_r 1 b b Hza1 Hza2).
+  rewrite Zmult_1_l in Hza3.
+  elim (H1 _ (conj Hza2 Hza3)).
+  exists b; auto.
+Qed.
+
+Theorem prime_div_prime: forall p q, 
+ prime p -> prime q -> (p | q) -> p = q.
+Proof.
+  intros p q H H1 H2; 
+  assert (Hp: 0 < p); try apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
+  assert (Hq: 0 < q); try apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
+  case prime_divisors with (2 := H2); auto.
+  intros H4; contradict Hp; subst; auto with zarith.
+  intros [H4| [H4 | H4]]; subst; auto.
+  contradict H; auto; apply not_prime_1.
+  contradict Hp; auto with zarith.
+Qed.
+
 
 (** We could obtain a [Zgcd] function via Euclid algorithm. But we propose 
   here a binary version of [Zgcd], faster and executable within Coq.
@@ -617,105 +904,34 @@ Fixpoint Pgcdn (n: nat) (a b : positive) { struct n } : positive :=
 	| xO a, xO b => xO (Pgcdn n a b)
 	| a, xO b => Pgcdn n a b
 	| xO a, b => Pgcdn n a b
-	| xI a', xI b' => match Pcompare a' b' Eq with 
-			    | Eq => a
-			    | Lt => Pgcdn  n (b'-a') a
-			    | Gt => Pgcdn n (a'-b') b
-			  end
-      end
-  end.
-
-Fixpoint Pggcdn (n: nat) (a b : positive) { struct n } : (positive*(positive*positive)) := 
-  match n with 
-    | O => (1,(a,b))
-    | S n => 
-      match a,b with 
-	| xH, b => (1,(1,b)) 
-	| a, xH => (1,(a,1))
-	| xO a, xO b => 
-          let (g,p) := Pggcdn n a b in 
-            (xO g,p)
-	| a, xO b => 
-          let (g,p) := Pggcdn n a b in 
-            let (aa,bb) := p in 
-              (g,(aa, xO bb))
-	| xO a, b => 
-          let (g,p) := Pggcdn n a b in 
-            let (aa,bb) := p in 
-              (g,(xO aa, bb))
-	| xI a', xI b' => match Pcompare a' b' Eq with 
-			    | Eq => (a,(1,1))
-			    | Lt => 
-			      let (g,p) := Pggcdn n (b'-a') a in 
-				let (ba,aa) := p in 
-				  (g,(aa, aa + xO ba))
-			    | Gt => 
-			      let (g,p) := Pggcdn n (a'-b') b in 
-				let (ab,bb) := p in 
-				  (g,(bb+xO ab, bb))
-			  end
+	| xI a', xI b' => 
+          match Pcompare a' b' Eq with 
+	    | Eq => a
+	    | Lt => Pgcdn  n (b'-a') a
+	    | Gt => Pgcdn n (a'-b') b
+          end
       end
   end.
 
 Definition Pgcd (a b: positive) := Pgcdn (Psize a + Psize b)%nat a b.
-Definition Pggcd (a b: positive) := Pggcdn (Psize a + Psize b)%nat a b.
 
-Open Scope Z_scope.
+Close Scope positive_scope.
 
-Definition Zgcd (a b : Z) : Z := match a,b with 
-				   | Z0, _ => Zabs b 
-				   | _, Z0 => Zabs a
-				   | Zpos a, Zpos b => Zpos (Pgcd a b)
-				   | Zpos a, Zneg b => Zpos (Pgcd a b)
-				   | Zneg a, Zpos b => Zpos (Pgcd a b)
-				   | Zneg a, Zneg b => Zpos (Pgcd a b)
-				 end.
-
-Definition Zggcd (a b : Z) : Z*(Z*Z) := match a,b with 
-					  | Z0, _ => (Zabs b,(0, Zsgn b)) 
-					  | _, Z0 => (Zabs a,(Zsgn a, 0))
-					  | Zpos a, Zpos b => 
-					    let (g,p) := Pggcd a b in 
-					      let (aa,bb) := p in 
-						(Zpos g, (Zpos aa, Zpos bb))
-					  | Zpos a, Zneg b => 
-					    let (g,p) := Pggcd a b in 
-					      let (aa,bb) := p in 
-						(Zpos g, (Zpos aa, Zneg bb))
-					  | Zneg a, Zpos b => 
-					    let (g,p) := Pggcd a b in 
-					      let (aa,bb) := p in 
-						(Zpos g, (Zneg aa, Zpos bb))
-					  | Zneg a, Zneg b =>
-					    let (g,p) := Pggcd a b in 
-					      let (aa,bb) := p in 
-						(Zpos g, (Zneg aa, Zneg bb))
-					end.
+Definition Zgcd (a b : Z) : Z :=
+  match a,b with
+    | Z0, _ => Zabs b 
+    | _, Z0 => Zabs a
+    | Zpos a, Zpos b => Zpos (Pgcd a b)
+    | Zpos a, Zneg b => Zpos (Pgcd a b)
+    | Zneg a, Zpos b => Zpos (Pgcd a b)
+    | Zneg a, Zneg b => Zpos (Pgcd a b)
+  end.
 
 Lemma Zgcd_is_pos : forall a b, 0 <= Zgcd a b.
 Proof.
   unfold Zgcd; destruct a; destruct b; auto with zarith.
 Qed.
 
-Lemma Psize_monotone : forall p q, Pcompare p q Eq = Lt -> (Psize p <= Psize q)%nat.
-Proof.
-  induction p; destruct q; simpl; auto with arith; intros; try discriminate.
-  intros; generalize (Pcompare_Gt_Lt _ _ H); auto with arith.
-  intros; destruct (Pcompare_Lt_Lt _ _ H); auto with arith; subst; auto.
-Qed.
-
-Lemma Pminus_Zminus : forall a b, Pcompare a b Eq = Lt -> 
-  Zpos (b-a) = Zpos b - Zpos a.
-Proof.
-  intros.
-  repeat rewrite Zpos_eq_Z_of_nat_o_nat_of_P.
-  rewrite nat_of_P_minus_morphism.
-  apply inj_minus1.
-  apply lt_le_weak.
-  apply nat_of_P_lt_Lt_compare_morphism; auto.
-  rewrite ZC4; rewrite H; auto.
-Qed.
-
 Lemma Zis_gcd_even_odd : forall a b g, Zis_gcd (Zpos a) (Zpos (xI b)) g -> 
   Zis_gcd (Zpos (xO a)) (Zpos (xI b)) g. 
 Proof.
@@ -758,12 +974,12 @@ Proof.
   assert (Psize (b-a) <= Psize b)%nat.
   apply Psize_monotone.
   change (Zpos (b-a) < Zpos b).
-  rewrite (Pminus_Zminus _ _ H1).
+  rewrite (Zpos_minus_morphism _ _ H1).
   assert (0 < Zpos a) by (compute; auto).
   omega.
   omega.  
   rewrite Zpos_xO; do 2 rewrite Zpos_xI.
-  rewrite Pminus_Zminus; auto.
+  rewrite Zpos_minus_morphism; auto.
   omega.
   (* a = xI, b = xI, compare = Gt *)
   apply Zis_gcd_for_euclid with 1.
@@ -775,13 +991,13 @@ Proof.
   assert (Psize (a-b) <= Psize a)%nat.
   apply Psize_monotone.
   change (Zpos (a-b) < Zpos a).
-  rewrite (Pminus_Zminus b a).
+  rewrite (Zpos_minus_morphism b a).
   assert (0 < Zpos b) by (compute; auto).
   omega.
   rewrite ZC4; rewrite H1; auto.
   omega.  
   rewrite Zpos_xO; do 2 rewrite Zpos_xI.
-  rewrite Pminus_Zminus; auto.
+  rewrite Zpos_minus_morphism; auto.
   omega.
   rewrite ZC4; rewrite H1; auto.
   (* a = xI, b = xO *)
@@ -840,6 +1056,230 @@ Proof.
   apply Pgcd_correct.
 Qed.
 
+Theorem Zgcd_spec : forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}.
+Proof.
+  intros x y; exists (Zgcd x y).
+  split; [apply Zgcd_is_gcd  | apply Zgcd_is_pos].
+Qed.
+
+Theorem Zdivide_Zgcd: forall p q r : Z, 
+ (p | q) -> (p | r) -> (p | Zgcd q r).
+Proof.
+  intros p q r H1 H2.
+  assert (H3: (Zis_gcd q r (Zgcd q r))).
+  apply Zgcd_is_gcd.
+  inversion_clear H3; auto.
+Qed.
+
+Theorem Zis_gcd_gcd: forall a b c : Z, 
+ 0 <= c ->  Zis_gcd a b c -> Zgcd a b = c.
+Proof.
+  intros a b c H1 H2.
+  case (Zis_gcd_uniqueness_apart_sign a b c (Zgcd a b)); auto.
+  apply Zgcd_is_gcd; auto.
+  case Zle_lt_or_eq with (1 := H1); clear H1; intros H1; subst; auto.
+  intros H3; subst.
+  generalize (Zgcd_is_pos a b); auto with zarith.
+  case (Zgcd a b); simpl; auto; intros; discriminate.
+Qed.
+
+Theorem Zgcd_inv_0_l: forall x y, Zgcd x y = 0 -> x = 0.
+Proof.
+  intros x y H.
+  assert (F1: Zdivide 0 x).
+   rewrite <- H.
+   generalize (Zgcd_is_gcd x y); intros HH; inversion HH; auto.
+  inversion F1 as [z H1].
+  rewrite H1; ring.
+Qed.
+
+Theorem Zgcd_inv_0_r: forall x y, Zgcd x y = 0 -> y = 0.
+Proof.
+  intros x y H.
+  assert (F1: Zdivide 0 y).
+   rewrite <- H.
+   generalize (Zgcd_is_gcd x y); intros HH; inversion HH; auto.
+  inversion F1 as [z H1].
+  rewrite H1; ring.
+Qed.
+
+Theorem Zgcd_div_swap0 : forall a b : Z, 
+ 0 < Zgcd a b ->
+ 0 < b ->
+ (a / Zgcd a b) * b = a * (b/Zgcd a b).
+Proof.
+  intros a b Hg Hb.
+  assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3].
+  pattern b at 2; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto.
+  repeat rewrite Zmult_assoc; f_equal.
+  rewrite Zmult_comm.
+  rewrite <- Zdivide_Zdiv_eq; auto.
+Qed.
+
+Theorem Zgcd_div_swap : forall a b c : Z, 
+ 0 < Zgcd a b ->
+ 0 < b ->
+ (c * a) / Zgcd a b * b = c * a * (b/Zgcd a b).
+Proof.
+  intros a b c Hg Hb.
+  assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3].
+  pattern b at 2; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto.
+  repeat rewrite Zmult_assoc; f_equal.
+  rewrite Zdivide_Zdiv_eq_2; auto.
+  repeat rewrite <- Zmult_assoc; f_equal.
+  rewrite Zmult_comm.
+  rewrite <- Zdivide_Zdiv_eq; auto.
+Qed.
+
+Theorem Zgcd_1_rel_prime : forall a b, 
+ Zgcd a b = 1 <-> rel_prime a b.
+Proof.
+  unfold rel_prime; split; intro H.
+  rewrite <- H; apply Zgcd_is_gcd.
+  case (Zis_gcd_unique a b (Zgcd a b) 1); auto.
+  apply Zgcd_is_gcd.
+  intros H2; absurd (0 <= Zgcd a b); auto with zarith.
+  generalize (Zgcd_is_pos a b); auto with zarith.
+Qed.
+
+Definition rel_prime_dec: forall a b, 
+ { rel_prime a b }+{ ~ rel_prime a b }.
+Proof.
+  intros a b; case (Z_eq_dec (Zgcd a b) 1); intros H1.
+  left; apply -> Zgcd_1_rel_prime; auto.
+  right; contradict H1; apply <- Zgcd_1_rel_prime; auto.
+Defined.
+
+Definition prime_dec_aux:
+ forall p m,
+  { forall n, 1 < n < m -> rel_prime n p } +
+  { exists n, 1 < n < m  /\ ~ rel_prime n p }.
+Proof.
+  intros p m.
+  case (Z_lt_dec 1 m); intros H1; 
+   [ | left; intros; elimtype False; omega ].
+  pattern m; apply natlike_rec; auto with zarith.
+  left; intros; elimtype False; omega.
+  intros x Hx IH; destruct IH as [F|E].
+  destruct (rel_prime_dec x p) as [Y|N].
+  left; intros n [HH1 HH2].
+  case (Zgt_succ_gt_or_eq x n); auto with zarith.
+  intros HH3; subst x; auto.
+  case (Z_lt_dec 1 x); intros HH1.
+  right; exists x; split; auto with zarith.
+  left; intros n [HHH1 HHH2]; contradict HHH1; auto with zarith.
+  right; destruct E as (n,((H0,H2),H3)); exists n; auto with zarith.
+Defined.
+
+Definition prime_dec: forall p, { prime p }+{ ~ prime p }.
+Proof.
+  intros p; case (Z_lt_dec 1 p); intros H1.
+  case (prime_dec_aux p p); intros H2.
+  left; apply prime_intro; auto.
+  intros n [Hn1 Hn2]; case Zle_lt_or_eq with ( 1 := Hn1 ); auto.
+  intros HH; subst n.
+  red; apply Zis_gcd_intro; auto with zarith.
+  right; intros H3; inversion_clear H3 as [Hp1 Hp2].
+  case H2; intros n [Hn1 Hn2]; case Hn2; auto with zarith.
+  right; intros H3; inversion_clear H3 as [Hp1 Hp2]; case H1; auto.
+Defined.
+
+Theorem not_prime_divide:
+ forall p, 1 < p -> ~ prime p -> exists n, 1 < n < p  /\ (n | p).
+Proof.
+  intros p Hp Hp1.
+  case (prime_dec_aux p p); intros H1.
+  elim Hp1; constructor; auto.
+  intros n [Hn1 Hn2].
+  case Zle_lt_or_eq with ( 1 := Hn1 ); auto with zarith.
+  intros H2; subst n; red; apply Zis_gcd_intro; auto with zarith.
+  case H1; intros n [Hn1 Hn2].
+  generalize (Zgcd_is_pos n p); intros Hpos.
+  case (Zle_lt_or_eq 0 (Zgcd n p)); auto with zarith; intros H3.
+  case (Zle_lt_or_eq 1 (Zgcd n p)); auto with zarith; intros H4.
+  exists (Zgcd n p); split; auto.
+  split; auto.
+  apply Zle_lt_trans with n; auto with zarith.
+  generalize (Zgcd_is_gcd n p); intros tmp; inversion_clear tmp as [Hr1 Hr2 Hr3].
+  case Hr1; intros q Hq.
+  case (Zle_or_lt q 0); auto with zarith; intros Ht.
+  absurd (n <= 0 * Zgcd n p) ; auto with zarith.
+  pattern n at 1; rewrite Hq; auto with zarith.
+  apply Zle_trans with (1 * Zgcd n p); auto with zarith.
+  pattern n at 2; rewrite Hq; auto with zarith.
+  generalize (Zgcd_is_gcd n p); intros Ht; inversion Ht; auto.
+  case Hn2; red.
+  rewrite H4; apply Zgcd_is_gcd.
+  generalize (Zgcd_is_gcd n p); rewrite <- H3; intros tmp;
+  inversion_clear tmp as [Hr1 Hr2 Hr3].
+  absurd (n = 0); auto with zarith.
+  case Hr1; auto with zarith.
+Qed.
+
+(** A Generalized Gcd that also computes Bezout coefficients.
+   The algorithm is the same as for Zgcd. *)
+
+Open Scope positive_scope.
+
+Fixpoint Pggcdn (n: nat) (a b : positive) { struct n } : (positive*(positive*positive)) := 
+  match n with 
+    | O => (1,(a,b))
+    | S n => 
+      match a,b with 
+	| xH, b => (1,(1,b)) 
+	| a, xH => (1,(a,1))
+	| xO a, xO b => 
+           let (g,p) := Pggcdn n a b in 
+           (xO g,p)
+	| a, xO b => 
+           let (g,p) := Pggcdn n a b in 
+           let (aa,bb) := p in 
+           (g,(aa, xO bb))
+	| xO a, b => 
+           let (g,p) := Pggcdn n a b in 
+           let (aa,bb) := p in 
+           (g,(xO aa, bb))
+	| xI a', xI b' => 
+           match Pcompare a' b' Eq with 
+	     | Eq => (a,(1,1))
+	     | Lt => 
+	        let (g,p) := Pggcdn n (b'-a') a in 
+	        let (ba,aa) := p in 
+	        (g,(aa, aa + xO ba))
+	     | Gt => 
+		let (g,p) := Pggcdn n (a'-b') b in 
+		let (ab,bb) := p in 
+		(g,(bb+xO ab, bb))
+	   end
+      end
+  end.
+
+Definition Pggcd (a b: positive) := Pggcdn (Psize a + Psize b)%nat a b.
+
+Open Scope Z_scope.
+
+Definition Zggcd (a b : Z) : Z*(Z*Z) :=
+  match a,b with
+    | Z0, _ => (Zabs b,(0, Zsgn b)) 
+    | _, Z0 => (Zabs a,(Zsgn a, 0))
+    | Zpos a, Zpos b => 
+       let (g,p) := Pggcd a b in 
+       let (aa,bb) := p in 
+       (Zpos g, (Zpos aa, Zpos bb))
+    | Zpos a, Zneg b => 
+       let (g,p) := Pggcd a b in 
+       let (aa,bb) := p in 
+       (Zpos g, (Zpos aa, Zneg bb))
+    | Zneg a, Zpos b => 
+       let (g,p) := Pggcd a b in 
+       let (aa,bb) := p in 
+       (Zpos g, (Zneg aa, Zpos bb))
+    | Zneg a, Zneg b =>
+       let (g,p) := Pggcd a b in 
+       let (aa,bb) := p in 
+       (Zpos g, (Zneg aa, Zneg bb))
+  end.
+
 
 Lemma Pggcdn_gcdn : forall n a b, 
   fst (Pggcdn n a b) = Pgcdn n a b.
@@ -870,8 +1310,8 @@ Open Scope positive_scope.
 
 Lemma Pggcdn_correct_divisors : forall n a b, 
   let (g,p) := Pggcdn n a b in 
-    let (aa,bb):=p in 
-      (a=g*aa) /\ (b=g*bb).
+  let (aa,bb):=p in 
+  (a=g*aa) /\ (b=g*bb).
 Proof.
   induction n.
   simpl; auto.
@@ -910,30 +1350,32 @@ Qed.
 
 Lemma Pggcd_correct_divisors : forall a b, 
   let (g,p) := Pggcd a b in 
-    let (aa,bb):=p in 
-      (a=g*aa) /\ (b=g*bb).
+  let (aa,bb):=p in 
+  (a=g*aa) /\ (b=g*bb).
 Proof.
   intros a b; exact (Pggcdn_correct_divisors (Psize a + Psize b)%nat a b).
 Qed.
 
-Open Scope Z_scope.
+Close Scope positive_scope.
 
 Lemma Zggcd_correct_divisors : forall a b, 
   let (g,p) := Zggcd a b in 
-    let (aa,bb):=p in 
-      (a=g*aa) /\ (b=g*bb).
+  let (aa,bb):=p in 
+  (a=g*aa) /\ (b=g*bb).
 Proof.
   destruct a; destruct b; simpl; auto; try solve [rewrite Pmult_comm; simpl; auto]; 
     generalize (Pggcd_correct_divisors p p0); destruct (Pggcd p p0) as (g,(aa,bb)); 
       destruct 1; subst; auto.
 Qed.
 
-Theorem Zgcd_spec : forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}.
+Theorem Zggcd_opp: forall x y, 
+  Zggcd (-x) y = let (p1,p) := Zggcd x y in
+                 let (p2,p3) := p in
+                 (p1,(-p2,p3)).
 Proof.
-  intros x y; exists (Zgcd x y).
-  split; [apply Zgcd_is_gcd  | apply Zgcd_is_pos].
+intros [|x|x] [|y|y]; unfold Zggcd, Zopp; auto.
+case Pggcd; intros p1 (p2, p3); auto.
+case Pggcd; intros p1 (p2, p3); auto.
+case Pggcd; intros p1 (p2, p3); auto.
+case Pggcd; intros p1 (p2, p3); auto.
 Qed.
-
-
-
-
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 47490be6..425aa83b 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -5,9 +5,9 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*i $Id: Zorder.v 9302 2006-10-27 21:21:17Z barras $ i*)
+(*i $Id: Zorder.v 10291 2007-11-06 02:18:53Z letouzey $ i*)
 
-(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
 
 Require Import BinPos.
 Require Import BinInt.
@@ -549,7 +549,7 @@ Hint Immediate Zeq_le: zarith.
 
 (** Transitivity using successor *)
 
-Lemma Zge_trans_succ : forall n m p:Z, Zsucc n > m -> m > p -> n > p.
+Lemma Zgt_trans_succ : forall n m p:Z, Zsucc n > m -> m > p -> n > p.
 Proof.
   intros n m p H1 H2; apply Zle_gt_trans with (m := m);
     [ apply Zgt_succ_le; assumption | assumption ].
@@ -997,5 +997,31 @@ Proof.
     rewrite <- Zplus_assoc; rewrite Zplus_opp_l; rewrite Zplus_0_r; exact H. 
 Qed.
 
+Lemma Zmult_lt_compat:
+  forall n m p q : Z, 0 <= n < p -> 0 <= m < q -> n * m < p * q.
+Proof.
+  intros n m p q (H1, H2) (H3,H4).
+  assert (0<p) by (apply Zle_lt_trans with n; auto).
+  assert (0<q) by (apply Zle_lt_trans with m; auto).
+  case Zle_lt_or_eq with (1 := H1); intros H5; auto with zarith.
+  case Zle_lt_or_eq with (1 := H3); intros H6; auto with zarith.
+  apply Zlt_trans with (n * q).
+  apply Zmult_lt_compat_l; auto.
+  apply Zmult_lt_compat_r; auto with zarith.
+  rewrite <- H6; rewrite Zmult_0_r; apply Zmult_lt_0_compat; auto with zarith.
+  rewrite <- H5; simpl; apply Zmult_lt_0_compat; auto with zarith.
+Qed.
+
+Lemma Zmult_lt_compat2: 
+  forall n m p q : Z, 0 < n <= p -> 0 < m < q -> n * m < p * q.
+Proof.
+  intros n m p q (H1, H2) (H3, H4).
+  apply Zle_lt_trans with (p * m).
+  apply Zmult_le_compat_r; auto.
+  apply Zlt_le_weak; auto.
+  apply Zmult_lt_compat_l; auto.
+  apply Zlt_le_trans with n; auto.
+Qed.
+
 (** For compatibility *)
 Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing).
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
new file mode 100644
index 00000000..3d4d235a
--- /dev/null
+++ b/theories/ZArith/Zpow_facts.v
@@ -0,0 +1,465 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Zpow_facts.v 11098 2008-06-11 09:16:22Z letouzey $ i*)
+
+Require Import ZArith_base.
+Require Import ZArithRing.
+Require Import Zcomplements.
+Require Export Zpower.
+Require Import Zdiv.
+Require Import Znumtheory.
+Open Local Scope Z_scope.
+
+Lemma Zpower_pos_1_r: forall x, Zpower_pos x 1 = x.
+Proof.
+  intros x; unfold Zpower_pos; simpl; auto with zarith.
+Qed.
+
+Lemma Zpower_pos_1_l: forall p, Zpower_pos 1 p = 1.
+Proof.
+  induction p.
+  (* xI *)
+  rewrite xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l.
+  repeat rewrite Zpower_pos_is_exp.
+  rewrite Zpower_pos_1_r, IHp; auto.
+  (* xO *)
+  rewrite <- Pplus_diag.
+  repeat rewrite Zpower_pos_is_exp.
+  rewrite IHp; auto.
+  (* xH *)
+  rewrite Zpower_pos_1_r; auto.
+Qed.
+
+Lemma Zpower_pos_0_l: forall p, Zpower_pos 0 p = 0.
+Proof. 
+  induction p.
+  change (xI p) with (1 + (xO p))%positive.
+  rewrite Zpower_pos_is_exp, Zpower_pos_1_r; auto.
+  rewrite <- Pplus_diag.
+  rewrite Zpower_pos_is_exp, IHp; auto.
+  rewrite Zpower_pos_1_r; auto.
+Qed.
+
+Lemma Zpower_pos_pos: forall x p,
+  0 < x -> 0 < Zpower_pos x p.
+Proof.
+  induction p; intros.
+  (* xI *)
+  rewrite xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l.
+  repeat rewrite Zpower_pos_is_exp.
+  rewrite Zpower_pos_1_r.
+  repeat apply Zmult_lt_0_compat; auto.
+  (* xO *)
+  rewrite <- Pplus_diag.
+  repeat rewrite Zpower_pos_is_exp.
+  repeat apply Zmult_lt_0_compat; auto.
+  (* xH *)
+  rewrite Zpower_pos_1_r; auto.
+Qed.
+
+
+Theorem Zpower_1_r: forall z, z^1 = z.
+Proof.
+  exact Zpower_pos_1_r.
+Qed.
+
+Theorem Zpower_1_l: forall z, 0 <= z -> 1^z = 1.
+Proof.
+  destruct z; simpl; auto.
+  intros; apply Zpower_pos_1_l.
+  intros; compute in H; elim H; auto.
+Qed.
+
+Theorem Zpower_0_l: forall z, z<>0 -> 0^z = 0.
+Proof.
+  destruct z; simpl; auto with zarith.
+  intros; apply Zpower_pos_0_l.
+Qed.
+
+Theorem Zpower_0_r: forall z, z^0 = 1.
+Proof.
+  simpl; auto.
+Qed.
+
+Theorem Zpower_2: forall z, z^2 = z * z.
+Proof.
+  intros; ring.
+Qed.
+
+Theorem Zpower_gt_0: forall x y,
+  0 < x -> 0 <= y -> 0 < x^y.
+Proof.
+  destruct y; simpl; auto with zarith.
+  intros; apply Zpower_pos_pos; auto.
+  intros; compute in H0; elim H0; auto.
+Qed.
+
+Theorem Zpower_Zabs: forall a b,  Zabs (a^b) = (Zabs a)^b.
+Proof.
+  intros a b; case (Zle_or_lt 0 b).
+  intros Hb; pattern b; apply natlike_ind; auto with zarith.
+  intros x Hx Hx1; unfold Zsucc.
+  (repeat rewrite Zpower_exp); auto with zarith.
+  rewrite Zabs_Zmult; rewrite Hx1.
+  f_equal; auto.
+  replace (a ^ 1) with a; auto.
+  simpl; unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto.
+  simpl; unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto.
+  case b; simpl; auto with zarith.
+  intros p Hp; discriminate.
+Qed.
+
+Theorem Zpower_Zsucc: forall p n, 0 <= n -> p^(Zsucc n) = p * p^n.
+Proof.
+  intros p n H.
+  unfold Zsucc; rewrite Zpower_exp; auto with zarith.
+  rewrite Zpower_1_r; apply Zmult_comm.
+Qed.
+
+Theorem Zpower_mult: forall p q r, 0 <= q -> 0 <= r -> p^(q*r) = (p^q)^r.
+Proof.
+  intros p q r H1 H2; generalize H2; pattern r; apply natlike_ind; auto.
+  intros H3; rewrite Zmult_0_r; repeat rewrite Zpower_exp_0; auto.
+  intros r1 H3 H4 H5.
+  unfold Zsucc; rewrite Zpower_exp; auto with zarith.
+  rewrite <- H4; try rewrite Zpower_1_r; try rewrite <- Zpower_exp; try f_equal; auto with zarith.
+  ring.
+  apply Zle_ge; replace 0 with (0 * r1); try apply Zmult_le_compat_r; auto.
+Qed.
+
+Theorem Zpower_le_monotone: forall a b c, 
+ 0 < a -> 0 <= b <= c -> a^b <= a^c.
+Proof.
+  intros a b c H (H1, H2).
+  rewrite <- (Zmult_1_r (a ^ b)); replace c with (b + (c - b)); auto with zarith.
+  rewrite Zpower_exp; auto with zarith.
+  apply Zmult_le_compat_l; auto with zarith.
+  assert (0 < a ^ (c - b)); auto with zarith.
+  apply Zpower_gt_0; auto with zarith.
+  apply Zlt_le_weak; apply Zpower_gt_0; auto with zarith.
+Qed.
+
+Theorem Zpower_lt_monotone: forall a b c, 
+ 1 < a -> 0 <= b < c -> a^b < a^c.
+Proof.
+  intros a b c H (H1, H2).
+  rewrite <- (Zmult_1_r (a ^ b)); replace c with (b + (c - b)); auto with zarith.
+  rewrite Zpower_exp; auto with zarith.
+  apply Zmult_lt_compat_l; auto with zarith.
+  apply Zpower_gt_0; auto with zarith.
+  assert (0 < a ^ (c - b)); auto with zarith.
+  apply Zpower_gt_0; auto with zarith.
+  apply Zlt_le_trans with (a ^1); auto with zarith.
+  rewrite Zpower_1_r; auto with zarith.
+  apply Zpower_le_monotone; auto with zarith.
+Qed.
+
+Theorem Zpower_gt_1 : forall x y, 
+  1 < x -> 0 < y -> 1 < x^y.
+Proof.
+  intros x y H1 H2.
+  replace 1 with (x ^ 0) by apply Zpower_0_r.
+  apply Zpower_lt_monotone; auto with zarith.
+Qed.
+
+Theorem Zpower_ge_0: forall x y, 0 <= x -> 0 <= x^y. 
+Proof.
+  intros x y; case y; auto with zarith.
+  simpl ; auto with zarith.
+  intros p H1; assert (H: 0 <= Zpos p); auto with zarith.
+  generalize H; pattern (Zpos p); apply natlike_ind; auto with zarith.
+  intros p1 H2 H3 _; unfold Zsucc; rewrite Zpower_exp; simpl; auto with zarith. 
+  apply Zmult_le_0_compat; auto with zarith.  
+  generalize H1; case x; compute; intros; auto; try discriminate.
+Qed.
+
+Theorem Zpower_le_monotone2:
+   forall a b c, 0 < a -> b <= c -> a^b <= a^c.
+Proof.
+  intros a b c H H2.
+  destruct (Z_le_gt_dec 0 b).
+  apply Zpower_le_monotone; auto.
+  replace (a^b) with 0.
+  destruct (Z_le_gt_dec 0 c).
+  destruct (Zle_lt_or_eq _ _ z0).
+  apply Zlt_le_weak;apply Zpower_gt_0;trivial.
+  rewrite <- H0;simpl;auto with zarith.
+  replace (a^c) with 0. auto with zarith.
+  destruct c;trivial;unfold Zgt in z0;discriminate z0.
+  destruct b;trivial;unfold Zgt in z;discriminate z.
+Qed.
+
+Theorem Zmult_power: forall p q r, 0 <= r -> 
+  (p*q)^r = p^r * q^r.
+Proof.
+  intros p q r H1; generalize H1; pattern r; apply natlike_ind; auto.
+  clear r H1; intros r H1 H2 H3.
+  unfold Zsucc; rewrite Zpower_exp; auto with zarith.
+  rewrite H2; repeat rewrite Zpower_exp; auto with zarith; ring.
+Qed.
+
+Hint Resolve Zpower_ge_0 Zpower_gt_0: zarith.
+
+Theorem Zpower_le_monotone3: forall a b c, 
+ 0 <= c -> 0 <= a <= b -> a^c <= b^c.
+Proof.
+  intros a b c H (H1, H2).
+  generalize H; pattern c; apply natlike_ind; auto.
+  intros x HH HH1 _; unfold Zsucc; repeat rewrite Zpower_exp; auto with zarith.
+  repeat rewrite Zpower_1_r.
+  apply Zle_trans with (a^x * b); auto with zarith.
+Qed.
+
+Lemma Zpower_le_monotone_inv: forall a b c, 
+  1 < a -> 0 < b -> a^b <= a^c -> b <= c.
+Proof.
+  intros a b c H H0 H1.
+  destruct (Z_le_gt_dec b c);trivial.
+  assert (2 <= a^b).
+   apply Zle_trans with (2^b).
+   pattern 2 at 1;replace 2 with (2^1);trivial.
+   apply Zpower_le_monotone;auto with zarith.
+   apply Zpower_le_monotone3;auto with zarith.
+  assert (c > 0).
+  destruct (Z_le_gt_dec 0 c);trivial. 
+  destruct (Zle_lt_or_eq _ _ z0);auto with zarith.
+  rewrite <- H3 in H1;simpl in H1; elimtype False;omega.
+  destruct c;try discriminate z0. simpl in H1. elimtype False;omega.
+  assert (H4 := Zpower_lt_monotone a c b H). elimtype False;omega.
+Qed.
+
+Theorem Zpower_nat_Zpower: forall p q, 0 <= q -> 
+ p^q = Zpower_nat p (Zabs_nat q).
+Proof.
+  intros p1 q1; case q1; simpl.
+  intros _; exact (refl_equal _).
+  intros p2 _; apply Zpower_pos_nat.
+  intros p2 H1; case H1; auto.
+Qed.
+
+Theorem Zpower2_lt_lin: forall n, 0 <= n -> n < 2^n.
+Proof.
+  intros n; apply (natlike_ind (fun n => n < 2 ^n)); clear n.
+  simpl; auto with zarith.
+  intros n H1 H2; unfold Zsucc.
+  case (Zle_lt_or_eq _ _ H1); clear H1; intros H1.
+  apply Zle_lt_trans with (n + n); auto with zarith.
+  rewrite Zpower_exp; auto with zarith.
+  rewrite Zpower_1_r.
+  assert (tmp: forall p, p * 2 = p + p); intros; try ring;
+  rewrite tmp; auto with zarith.
+  subst n; simpl; unfold Zpower_pos; simpl; auto with zarith.
+Qed.
+
+Theorem Zpower2_le_lin: forall n, 0 <= n -> n <= 2^n.
+Proof.
+  intros; apply Zlt_le_weak; apply Zpower2_lt_lin; auto.
+Qed.
+
+Lemma Zpower2_Psize : 
+  forall n p, Zpos p < 2^(Z_of_nat n) <-> (Psize p <= n)%nat.
+Proof.
+  induction n.
+  destruct p; split; intros H; discriminate H || inversion H.
+  destruct p; simpl Psize.
+  rewrite inj_S, Zpower_Zsucc; auto with zarith.
+  rewrite Zpos_xI; specialize IHn with p; omega.
+  rewrite inj_S, Zpower_Zsucc; auto with zarith.
+  rewrite Zpos_xO; specialize IHn with p; omega.
+  split; auto with arith.
+  intros _; apply Zpower_gt_1; auto with zarith.
+  rewrite inj_S; generalize (Zle_0_nat n); omega.
+Qed.
+
+(** * Zpower and modulo *)
+
+Theorem Zpower_mod: forall p q n, 0 < n ->
+ (p^q) mod n = ((p mod n)^q) mod n.
+Proof.
+  intros p q n Hn; case (Zle_or_lt 0 q); intros H1.
+  generalize H1; pattern q; apply natlike_ind; auto.
+  intros q1 Hq1 Rec _; unfold Zsucc; repeat rewrite Zpower_exp; repeat rewrite Zpower_1_r; auto with zarith.
+  rewrite (fun x => (Zmult_mod x p)); try rewrite Rec; auto with zarith.
+  rewrite (fun x y => (Zmult_mod (x ^y))); try f_equal; auto with zarith.
+  f_equal; auto; apply sym_equal; apply Zmod_mod; auto with zarith.
+  generalize H1; case q; simpl; auto.
+  intros; discriminate.
+Qed.
+
+(** A direct way to compute Zpower modulo **)
+
+Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) {struct m} : Z :=
+  match m with
+   | xH => a mod n
+   | xO m' =>
+      let z := Zpow_mod_pos a m' n in
+      match z with
+       | 0 => 0
+       | _ => (z * z) mod n
+      end
+   | xI m' =>
+      let z := Zpow_mod_pos a m' n in
+      match z with
+       | 0 => 0
+       | _ => (z * z * a) mod n
+      end
+  end.
+
+Definition Zpow_mod a m n := 
+  match m with 
+   | 0 => 1 
+   | Zpos p => Zpow_mod_pos a p n 
+   | Zneg p => 0 
+  end.
+
+Theorem Zpow_mod_pos_correct: forall a m n, 0 < n -> 
+ Zpow_mod_pos a m n = (Zpower_pos a m) mod n.
+Proof.
+  intros a m; elim m; simpl; auto.
+  intros p Rec n H1; rewrite xI_succ_xO, Pplus_one_succ_r, <-Pplus_diag; auto.
+  repeat rewrite Zpower_pos_is_exp; auto.
+  repeat rewrite Rec; auto.
+  rewrite Zpower_pos_1_r.
+  repeat rewrite (fun x => (Zmult_mod x a)); auto with zarith.
+  rewrite (Zmult_mod (Zpower_pos a p)); auto with zarith. 
+  case (Zpower_pos a p mod n); auto.
+  intros p Rec n H1; rewrite <- Pplus_diag; auto.
+  repeat rewrite Zpower_pos_is_exp; auto.
+  repeat rewrite Rec; auto.
+  rewrite (Zmult_mod (Zpower_pos a p)); auto with zarith. 
+  case (Zpower_pos a p mod n); auto.
+  unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto with zarith.
+Qed.
+
+Theorem Zpow_mod_correct: forall a m n, 1 < n -> 0 <= m ->
+ Zpow_mod a m n = (a ^ m) mod n.
+Proof.
+  intros a m n; case m; simpl.
+  intros; apply sym_equal; apply Zmod_small; auto with zarith.
+  intros; apply Zpow_mod_pos_correct; auto with zarith.
+  intros p H H1; case H1; auto.
+Qed.
+
+(* Complements about power and number theory. *)
+
+Lemma Zpower_divide: forall p q, 0 < q -> (p | p ^ q).
+Proof.
+  intros p q H; exists (p ^(q - 1)).
+  pattern p at 3; rewrite <- (Zpower_1_r p); rewrite <- Zpower_exp; try f_equal; auto with zarith.
+Qed.
+
+Theorem rel_prime_Zpower_r: forall i p q, 0 < i -> 
+ rel_prime p q -> rel_prime p (q^i).
+Proof.
+  intros i p q Hi Hpq; generalize Hi; pattern i; apply natlike_ind; auto with zarith; clear i Hi.
+  intros H; contradict H; auto with zarith.
+  intros i Hi Rec _; rewrite Zpower_Zsucc; auto.
+  apply rel_prime_mult; auto.
+  case Zle_lt_or_eq with (1 := Hi); intros Hi1; subst; auto.
+  rewrite Zpower_0_r; apply rel_prime_sym; apply rel_prime_1.
+Qed.
+
+Theorem rel_prime_Zpower: forall i j p q, 0 <= i ->  0 <= j -> 
+ rel_prime p q -> rel_prime (p^i) (q^j).
+Proof.
+  intros i j p q Hi; generalize Hi j p q; pattern i; apply natlike_ind; auto with zarith; clear i Hi j p q.
+  intros _ j p q H H1; rewrite Zpower_0_r; apply rel_prime_1.
+  intros n Hn Rec _ j p q Hj Hpq.
+  rewrite Zpower_Zsucc; auto.
+  case Zle_lt_or_eq with (1 := Hj); intros Hj1; subst.
+  apply rel_prime_sym; apply rel_prime_mult; auto.
+  apply rel_prime_sym; apply rel_prime_Zpower_r; auto with arith.
+  apply rel_prime_sym; apply Rec; auto.
+  rewrite Zpower_0_r; apply rel_prime_sym; apply rel_prime_1.
+Qed.
+
+Theorem prime_power_prime: forall p q n, 0 <= n -> 
+ prime p -> prime q -> (p | q^n)  -> p = q.
+Proof.
+  intros p q n Hn Hp Hq; pattern n; apply natlike_ind; auto; clear n Hn.
+  rewrite Zpower_0_r; intros.
+  assert (2<=p) by (apply prime_ge_2; auto).
+  assert (p<=1) by (apply Zdivide_le; auto with zarith).
+  omega.
+  intros n1 H H1.
+  unfold Zsucc; rewrite Zpower_exp; try rewrite Zpower_1_r; auto with zarith.
+  assert (2<=p) by (apply prime_ge_2; auto).
+  assert (2<=q) by (apply prime_ge_2; auto).
+  intros H3; case prime_mult with (2 := H3); auto.
+  intros; apply prime_div_prime; auto.
+Qed.
+
+Theorem Zdivide_power_2: forall x p n, 0 <= n -> 0 <= x -> prime p ->
+ (x | p^n) -> exists m, x = p^m.
+Proof.
+  intros x p n Hn Hx; revert p n Hn; generalize Hx.
+  pattern x; apply Z_lt_induction; auto.
+  clear x Hx; intros x IH Hx p n Hn Hp H.
+  case Zle_lt_or_eq with (1 := Hx); auto; clear Hx; intros Hx; subst.
+  case (Zle_lt_or_eq 1 x); auto with zarith; clear Hx; intros Hx; subst.
+  (* x > 1 *)
+  case (prime_dec x); intros H2.
+  exists 1; rewrite Zpower_1_r; apply prime_power_prime with n; auto.
+  case not_prime_divide with (2 := H2); auto.
+  intros p1 ((H3, H4), (q1, Hq1)); subst.
+  case (IH p1) with p n; auto with zarith.
+  apply Zdivide_trans with (2 := H); exists q1; auto with zarith.
+  intros r1 Hr1.
+  case (IH q1) with p n; auto with zarith.
+  case (Zle_lt_or_eq 0 q1).
+  apply Zmult_le_0_reg_r with p1; auto with zarith.
+  split; auto with zarith.
+  pattern q1 at 1; replace q1 with (q1 * 1); auto with zarith.
+  apply Zmult_lt_compat_l; auto with zarith.
+  intros H5; subst; contradict Hx; auto with zarith.
+  apply Zmult_le_0_reg_r with p1; auto with zarith.
+  apply Zdivide_trans with (2 := H); exists p1; auto with zarith.
+  intros r2 Hr2; exists (r2 + r1); subst.
+  apply sym_equal; apply Zpower_exp.
+  generalize Hx; case r2; simpl; auto with zarith.
+  intros; red; simpl; intros; discriminate.
+  generalize H3; case r1; simpl; auto with zarith.
+  intros; red; simpl; intros; discriminate.
+  (* x = 1 *)
+  exists 0; rewrite Zpower_0_r; auto.
+  (* x = 0 *)
+  exists n; destruct H; rewrite Zmult_0_r in H; auto.
+Qed.
+
+(** * Zsquare: a direct definition of [z^2] *)
+
+Fixpoint Psquare (p: positive): positive :=
+  match p with
+   | xH => xH
+   | xO p => xO (xO (Psquare p))
+   | xI p => xI (xO (Pplus (Psquare p) p))
+  end.
+
+Definition Zsquare p :=
+  match p with 
+   | Z0 => Z0 
+   | Zpos p => Zpos (Psquare p) 
+   | Zneg p => Zpos (Psquare p)
+  end.
+
+Theorem Psquare_correct: forall p, Psquare p = (p * p)%positive.
+Proof.
+  induction p; simpl; auto; f_equal; rewrite IHp.  
+  apply trans_equal with (xO p + xO (p*p))%positive; auto.
+  rewrite (Pplus_comm (xO p)); auto.
+  rewrite Pmult_xI_permute_r; rewrite Pplus_assoc.
+  f_equal; auto.
+  symmetry; apply Pplus_diag.
+  symmetry; apply Pmult_xO_permute_r.
+Qed.
+
+Theorem Zsquare_correct: forall p, Zsquare p = p * p.
+Proof.
+  intro p; case p; simpl; auto; intros p1; rewrite Psquare_correct; auto.
+Qed.
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index c9cee31d..1912f5e1 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -6,89 +6,75 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Zpower.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: Zpower.v 11072 2008-06-08 16:13:37Z herbelin $ i*)
 
+Require Import Wf_nat.
 Require Import ZArith_base.
 Require Export Zpow_def.
 Require Import Omega.
 Require Import Zcomplements.
 Open Local Scope Z_scope.
 
-Section section1.
+Infix "^" := Zpower : Z_scope.
 
 (** * Definition of powers over [Z]*)
 
 (** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary
     integer (type [nat]) and [z] a signed integer (type [Z]) *) 
 
-  Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1.
-
-  (** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for
-      [plus : nat->nat] and [Zmult : Z->Z] *)
-
-  Lemma Zpower_nat_is_exp :
-    forall (n m:nat) (z:Z),
-      Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m.
-  Proof.
-    intros; elim n;
-      [ simpl in |- *; elim (Zpower_nat z m); auto with zarith
-	| unfold Zpower_nat in |- *; intros; simpl in |- *; rewrite H;
-	  apply Zmult_assoc ].
-  Qed.
-
-  (** This theorem shows that powers of unary and binary integers
-     are the same thing, modulo the function convert : [positive -> nat] *)
-
-  Theorem Zpower_pos_nat :
-    forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p).
-  Proof.
-    intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *;
-      apply iter_nat_of_P.
-  Qed.
-
-  (** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we
-     deduce that the function [[n:positive](Zpower_pos z n)] is a morphism
-     for [add : positive->positive] and [Zmult : Z->Z] *)
-
-  Theorem Zpower_pos_is_exp :
-    forall (n m:positive) (z:Z),
-      Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m.
-  Proof.
-    intros.
-    rewrite (Zpower_pos_nat z n).
-    rewrite (Zpower_pos_nat z m).
-    rewrite (Zpower_pos_nat z (n + m)).
-    rewrite (nat_of_P_plus_morphism n m).
-    apply Zpower_nat_is_exp.
-  Qed.
-
-  Infix "^" := Zpower : Z_scope.
-
-  Hint Immediate Zpower_nat_is_exp: zarith.
-  Hint Immediate Zpower_pos_is_exp: zarith.
-  Hint Unfold Zpower_pos: zarith.
-  Hint Unfold Zpower_nat: zarith.
-
-  Lemma Zpower_exp :
-    forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m.
-  Proof.
-    destruct n; destruct m; auto with zarith.
-    simpl in |- *; intros; apply Zred_factor0.
-    simpl in |- *; auto with zarith.
-    intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith.
-    intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith.
-  Qed.
-
-End section1.
-
-(** Exporting notation "^" *)
-
-Infix "^" := Zpower : Z_scope.
-
-Hint Immediate Zpower_nat_is_exp: zarith.
-Hint Immediate Zpower_pos_is_exp: zarith.
-Hint Unfold Zpower_pos: zarith.
-Hint Unfold Zpower_nat: zarith.
+Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1.
+
+(** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for
+    [plus : nat->nat] and [Zmult : Z->Z] *)
+
+Lemma Zpower_nat_is_exp :
+  forall (n m:nat) (z:Z),
+    Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m.
+Proof.
+  intros; elim n;
+   [ simpl in |- *; elim (Zpower_nat z m); auto with zarith
+     | unfold Zpower_nat in |- *; intros; simpl in |- *; rewrite H;
+       apply Zmult_assoc ].
+Qed.
+
+(** This theorem shows that powers of unary and binary integers
+   are the same thing, modulo the function convert : [positive -> nat] *)
+
+Lemma Zpower_pos_nat :
+  forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p).
+Proof.
+  intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *;
+    apply iter_nat_of_P.
+Qed.
+
+(** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we
+   deduce that the function [[n:positive](Zpower_pos z n)] is a morphism
+   for [add : positive->positive] and [Zmult : Z->Z] *)
+
+Lemma Zpower_pos_is_exp :
+  forall (n m:positive) (z:Z),
+    Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m.
+Proof.
+  intros.
+  rewrite (Zpower_pos_nat z n).
+  rewrite (Zpower_pos_nat z m).
+  rewrite (Zpower_pos_nat z (n + m)).
+  rewrite (nat_of_P_plus_morphism n m).
+  apply Zpower_nat_is_exp.
+Qed.
+
+Hint Immediate Zpower_nat_is_exp Zpower_pos_is_exp : zarith.
+Hint Unfold Zpower_pos Zpower_nat: zarith.
+
+Theorem Zpower_exp :
+  forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m.
+Proof.
+  destruct n; destruct m; auto with zarith.
+  simpl; intros; apply Zred_factor0.
+  simpl; auto with zarith.
+  intros; compute in H0; elim H0; auto.
+  intros; compute in H; elim H; auto.
+Qed.
 
 Section Powers_of_2.
 
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index 3f475a63..6ea952e6 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Zsqrt.v 9551 2007-01-29 15:13:35Z bgregoir $ *)
+(* $Id: Zsqrt.v 10295 2007-11-06 22:46:21Z letouzey $ *)
 
 Require Import ZArithRing.
 Require Import Omega.
@@ -148,6 +148,7 @@ Definition Zsqrt_plain (x:Z) : Z :=
   end.
 
 (** A basic theorem about Zsqrt_plain *)
+
 Theorem Zsqrt_interval :
   forall n:Z,
     0 <= n ->
@@ -162,3 +163,53 @@ Proof.
   intros p Hle; elim Hle; auto.
 Qed.
 
+(** Positivity *)
+
+Theorem Zsqrt_plain_is_pos: forall n, 0 <= n ->  0 <= Zsqrt_plain n.
+Proof.
+  intros n m; case (Zsqrt_interval n); auto with zarith.
+  intros H1 H2; case (Zle_or_lt 0 (Zsqrt_plain n)); auto.
+  intros H3; contradict H2; auto; apply Zle_not_lt.
+  apply Zle_trans with ( 2 := H1 ).
+  replace ((Zsqrt_plain n + 1) * (Zsqrt_plain n + 1))
+     with (Zsqrt_plain n * Zsqrt_plain n + (2 * Zsqrt_plain n + 1));
+  auto with zarith.
+  ring.
+Qed.
+
+(** Direct correctness on squares. *)
+
+Theorem Zsqrt_square_id: forall a, 0 <= a ->  Zsqrt_plain (a * a) = a.
+Proof.
+  intros a H.
+  generalize (Zsqrt_plain_is_pos (a * a)); auto with zarith; intros Haa.
+  case (Zsqrt_interval (a * a)); auto with zarith.
+  intros H1 H2.
+  case (Zle_or_lt a (Zsqrt_plain (a * a))); intros H3; auto.
+  case Zle_lt_or_eq with (1:=H3); auto; clear H3; intros H3.
+  contradict H1; auto; apply Zlt_not_le; auto with zarith.
+  apply Zle_lt_trans with (a * Zsqrt_plain (a * a)); auto with zarith.
+  apply Zmult_lt_compat_r; auto with zarith.
+  contradict H2; auto; apply Zle_not_lt; auto with zarith.
+  apply Zmult_le_compat; auto with zarith.
+Qed.
+
+(** [Zsqrt_plain] is increasing *)
+
+Theorem Zsqrt_le:
+ forall p q, 0 <= p <= q  ->  Zsqrt_plain p <= Zsqrt_plain q.
+Proof.
+  intros p q [H1 H2]; case Zle_lt_or_eq with (1:=H2); clear H2; intros H2; 
+  [ | subst q; auto with zarith].
+  case (Zle_or_lt (Zsqrt_plain p) (Zsqrt_plain q)); auto; intros H3.
+  assert (Hp: (0 <= Zsqrt_plain q)).
+   apply Zsqrt_plain_is_pos; auto with zarith.
+  absurd (q <= p); auto with zarith.
+  apply Zle_trans with ((Zsqrt_plain q + 1) * (Zsqrt_plain q + 1)).
+  case (Zsqrt_interval q); auto with zarith.
+  apply Zle_trans with (Zsqrt_plain p * Zsqrt_plain p); auto with zarith.
+  apply Zmult_le_compat; auto with zarith.
+  case (Zsqrt_interval p); auto with zarith.
+Qed.
+
+