Integer division: quot and rem (trunc convention) in addition to div and mod

(floor convention).

We follow Haskell naming convention: quot and rem are for
Round-Toward-Zero (a.k.a Trunc, what Ocaml, C, Asm do by default, cf.
the ex-ZOdiv file), while div and mod are for Round-Toward-Bottom
(a.k.a Floor, what Coq does historically in Zdiv). We use unicode ÷
for quot, and infix rem for rem (which is actually remainder in
full). This way, both conventions can be used at the same time.

Definitions (and proofs of specifications) for div mod quot rem are
migrated in a new file Zdiv_def. Ex-ZOdiv file is now Zquot. With
this new organisation, no need for functor application in Zdiv and
Zquot.

On the abstract side, ZAxiomsSig now provides div mod quot rem.
Zproperties now contains properties of them. In NZDiv, we stop
splitting specifications in Common vs. Specific parts. Instead,
the NZ specification is be extended later, even if this leads to
a useless mod_bound_pos, subsumed by more precise axioms.

A few results in ZDivTrunc and ZDivFloor are improved (sgn stuff).

A few proofs in Nnat, Znat, Zabs are reworked (no more dependency
to Zmin, Zmax).

A lcm (least common multiple) is derived abstractly from gcd and
division (and hence available for nat N BigN Z BigZ :-).
In these new files NLcm and ZLcm, we also provide some combined
properties of div mod quot rem gcd.

We also provide a new file Zeuclid implementing a third division
convention, where the remainder is always positive. This file
instanciate the abstract one ZDivEucl. Operation names are
ZEuclid.div and ZEuclid.modulo.

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

10 files changed, 991 insertions, 982 deletions

diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index 3956e91607..26d700773e 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -12,7 +12,7 @@ Require Export ZArith_base.
 
 (** Extra definitions *)
 
-Require Export Zpow_def Zsqrt_def Zlog_def Zgcd_def.
+Require Export Zpow_def Zsqrt_def Zlog_def Zgcd_def Zdiv_def.
 
 (** Extra modules using [Omega] or [Ring]. *)
 
@@ -22,7 +22,3 @@ Require Export Zdiv.
 Require Export Zlogarithm.
 
 Export ZArithRing.
-
-(** Final Z module, cumulating ZBinary.Z and Zdiv.Z *)
-
-Module Z := Zdiv.Z.
diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v
deleted file mode 100644
index df81fa9a6a..0000000000
--- a/theories/ZArith/ZOdiv.v
+++ /dev/null
@@ -1,563 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \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 Morphisms.
-Require Export Ndiv_def ZOdiv_def.
-Require Zdiv ZBinary ZDivTrunc.
-
-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.
-
-(*
-(** 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 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:
-    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 using Z_of_N_le_0;
-  intros LT; apply (Z_of_N_lt _ _ LT).
-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.
-
-(** We know enough to prove that [ZOdiv] and [ZOmod] are instances of
-    one of the abstract Euclidean divisions of Numbers. *)
-
-Module ZODiv <: ZDivTrunc.ZDiv ZBinary.Z.
- Definition div := ZOdiv.
- Definition modulo := ZOmod.
- Local Obligation Tactic := simpl_relation.
- Program Instance div_wd : Proper (eq==>eq==>eq) div.
- Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
-
- Definition div_mod := fun a b (_:b<>0) => ZO_div_mod_eq a b.
- Definition mod_bound := ZOmod_lt_pos_pos.
- Definition mod_opp_l := fun a b (_:b<>0) => ZOmod_opp_l a b.
- Definition mod_opp_r := fun a b (_:b<>0) => ZOmod_opp_r a b.
-End ZODiv.
-
-Module ZODivMod := ZBinary.Z <+ ZODiv.
-
-(** We hence benefit from generic results about this abstract division. *)
-
-Module Z := ZDivTrunc.ZDivProp ZODivMod ZBinary.Z.
-
-(** * 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. exact Z.div_unique. 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. exact Z.mod_unique. 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. exact Z.mod_1_r. Qed.
-
-Lemma ZOdiv_1_r: forall a, a/1 = a.
-Proof. exact Z.div_1_r. 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. exact Z.div_1_l. Qed.
-
-Lemma ZOmod_1_l: forall a, 1 < a ->  1 mod a = 1.
-Proof. exact Z.mod_1_l. Qed.
-
-Lemma ZO_div_same : forall a:Z, a<>0 -> a/a = 1.
-Proof. exact Z.div_same. Qed.
-
-Ltac zero_or_not a :=
-  destruct (Z_eq_dec a 0);
-  [subst; rewrite ?ZOmod_0_l, ?ZOdiv_0_l, ?ZOmod_0_r, ?ZOdiv_0_r;
-   auto with zarith|].
-
-Lemma ZO_mod_same : forall a, a mod a = 0.
-Proof. intros. zero_or_not a. apply Z.mod_same; auto. Qed.
-
-Lemma ZO_mod_mult : forall a b, (a*b) mod b = 0.
-Proof. intros. zero_or_not b. apply Z.mod_mul; auto. Qed.
-
-Lemma ZO_div_mult : forall a b:Z, b <> 0 -> (a*b)/b = a.
-Proof. exact Z.div_mul. 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. zero_or_not b. apply Z.div_pos; auto with zarith. 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. apply Z.div_lt; auto with zarith. 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. exact Z.div_small. Qed.
-
-(** Same situation, in term of modulo: *)
-
-Theorem ZOmod_small: forall a n, 0 <= a < n -> a mod n = a.
-Proof. exact Z.mod_small. Qed.
-
-(** [Zge] is compatible with a positive division. *)
-
-Lemma ZO_div_monotone : forall a b c, 0<=c -> a<=b -> a/c <= b/c.
-Proof. intros. zero_or_not c. apply Z.div_le_mono; auto with zarith. 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. zero_or_not b. apply Z.mul_div_le; auto with zarith. Qed.
-
-Lemma ZO_mult_div_ge : forall a b:Z, a <= 0 -> a <= b*(a/b) <= 0.
-Proof. intros. zero_or_not b. apply Z.mul_div_ge; 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 : forall a b:Z, a = b*(a/b) <-> a mod b = 0.
-Proof. intros. zero_or_not b. intuition. apply Z.div_exact; auto. 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. zero_or_not b. apply Z.mod_le; auto with zarith. Qed.
-
-(** Some additionnal inequalities about Zdiv. *)
-
-Theorem ZOdiv_le_upper_bound:
-  forall a b q, 0 < b -> a <= q*b -> a/b <= q.
-Proof. intros a b q; rewrite Zmult_comm; apply Z.div_le_upper_bound. 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; rewrite Zmult_comm; apply Z.div_lt_upper_bound. Qed.
-
-Theorem ZOdiv_le_lower_bound:
-  forall a b q, 0 < b -> q*b <= a -> q <= a/b.
-Proof. intros a b q; rewrite Zmult_comm; apply Z.div_le_lower_bound. 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. zero_or_not c. apply Z.mod_add; auto with zarith. 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. apply Z.div_add; auto with zarith. 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. apply Z.div_add_l; 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. zero_or_not b. apply Z.div_mul_cancel_r; auto. 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 b). zero_or_not b.
- rewrite (Zmult_comm b c). apply Z.div_mul_cancel_l; auto.
-Qed.
-
-Lemma ZOmult_mod_distr_l: forall a b c,
-  (c*a) mod (c*b) = c * (a mod b).
-Proof.
- intros. zero_or_not c. rewrite (Zmult_comm c b). zero_or_not b.
- rewrite (Zmult_comm b c). apply Z.mul_mod_distr_l; auto.
-Qed.
-
-Lemma ZOmult_mod_distr_r: forall a b c,
-  (a*c) mod (b*c) = (a mod b) * c.
-Proof.
- intros. zero_or_not b. rewrite (Zmult_comm b c). zero_or_not c.
- rewrite (Zmult_comm c b). apply Z.mul_mod_distr_r; auto.
-Qed.
-
-(** Operations modulo. *)
-
-Theorem ZOmod_mod: forall a n, (a mod n) mod n = a mod n.
-Proof. intros. zero_or_not n. apply Z.mod_mod; auto. Qed.
-
-Theorem ZOmult_mod: forall a b n,
- (a * b) mod n = ((a mod n) * (b mod n)) mod n.
-Proof. intros. zero_or_not n. apply Z.mul_mod; auto. 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. intros. zero_or_not n. apply Z.add_mod; auto. 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. zero_or_not n. apply Z.add_mod_idemp_l; auto. 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. zero_or_not n. apply Z.add_mod_idemp_r; auto.
- rewrite Zmult_comm; auto. Qed.
-
-Lemma ZOmult_mod_idemp_l: forall a b n, (a mod n * b) mod n = (a * b) mod n.
-Proof. intros. zero_or_not n. apply Z.mul_mod_idemp_l; auto. Qed.
-
-Lemma ZOmult_mod_idemp_r: forall a b n, (b * (a mod n)) mod n = (b * a) mod n.
-Proof. intros. zero_or_not n. apply Z.mul_mod_idemp_r; 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.
- intros. zero_or_not b. rewrite Zmult_comm. zero_or_not c.
- rewrite Zmult_comm. apply Z.div_div; auto.
-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. zero_or_not b. apply Z.div_mul_le; 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. intros. zero_or_not b. firstorder. apply Z.mod_divides; auto. 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
deleted file mode 100644
index 1fb238f2be..0000000000
--- a/theories/ZArith/ZOdiv_def.v
+++ /dev/null
@@ -1,56 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \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 Ndiv_def.
-
-Open Scope Z_scope.
-
-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).
-
-(* Proofs of specifications for this euclidean division. *)
-
-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 q r H.
-
-  change (Zpos p) with (Z_of_N (Npos p)). rewrite H.
-   rewrite Z_of_N_plus, Z_of_N_mult. reflexivity.
-
-  change (Zpos p) with (Z_of_N (Npos p)). rewrite H.
-   rewrite Z_of_N_plus, Z_of_N_mult. rewrite Zmult_opp_comm. reflexivity.
-
-  change (Zneg p) with (-(Z_of_N (Npos p))); rewrite H.
-   rewrite Z_of_N_plus, Z_of_N_mult.
-  rewrite Zopp_plus_distr, Zopp_mult_distr_l; trivial.
-
-  change (Zneg p) with (-(Z_of_N (Npos p))); rewrite H.
-   rewrite Z_of_N_plus, Z_of_N_mult.
-  rewrite Zopp_plus_distr, Zopp_mult_distr_r; trivial.
-Qed.
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index 8443325ef6..8543652c61 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -11,8 +11,8 @@
 Require Import Arith_base.
 Require Import BinPos.
 Require Import BinInt.
+Require Import Zcompare.
 Require Import Zorder.
-Require Import Zmax.
 Require Import Znat.
 Require Import ZArith_dec.
 
@@ -149,33 +149,37 @@ Proof.
   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.
+Lemma Zabs_nat_compare :
+ forall x y, 0<=x -> 0<=y -> nat_compare (Zabs_nat x) (Zabs_nat y) = (x?=y).
 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.
+ intros. rewrite <- inj_compare, 2 inj_Zabs_nat, 2 Zabs_eq; trivial.
 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.
+ intros n m (H,H'). apply nat_compare_le. rewrite Zabs_nat_compare; trivial.
+ apply Zle_trans with n; auto.
 Qed.
 
 Lemma Zabs_nat_lt :
   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.
+  intros n m (H,H'). apply nat_compare_lt. rewrite Zabs_nat_compare; trivial.
   apply Zlt_le_weak; apply Zle_lt_trans with n; 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_minus1. rewrite !inj_Zabs_nat, !Zabs_eq; auto.
+  apply Zabs_nat_le. now split.
+Qed.
+
 (** * Some results about the sign function. *)
 
 Lemma Zsgn_Zmult : forall a b, Zsgn (a*b) = Zsgn a * Zsgn b.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index fbedaa3d7c..a14f29308a 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -7,130 +7,20 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Contribution by Claude Marché and Xavier Urbain *)
+(** * Euclidean Division *)
 
-(** Euclidean Division
+(** Initial Contribution by Claude Marché and Xavier Urbain *)
 
-    Defines first of function that allows Coq to normalize.
-    Then only after proves the main required property.
-*)
-
-Require Export ZArith_base.
+Require Export ZArith_base Zdiv_def.
 Require Import Zbool Omega ZArithRing Zcomplements Setoid Morphisms.
 Require ZDivFloor.
-Open Local Scope Z_scope.
-
-(** * Definitions of Euclidian operations *)
-
-(** Euclidean division of a positive by a integer
-    (that is supposed to be positive).
-
-    Total function than returns an arbitrary value when
-    divisor is not positive
-
-*)
-
-Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) : Z * Z :=
-  match a with
-    | xH => if Zge_bool b 2 then (0, 1) else (1, 0)
-    | xO a' =>
-      let (q, r) := Zdiv_eucl_POS a' b in
-	let r' := 2 * r in
-	  if Zgt_bool b r' then (2 * q, r') else (2 * q + 1, r' - b)
-    | xI a' =>
-      let (q, r) := Zdiv_eucl_POS a' b in
-	let r' := 2 * r + 1 in
-	  if Zgt_bool b r' then (2 * q, r') else (2 * q + 1, r' - b)
-  end.
-
-
-(** Euclidean division of integers.
-
-    Total function than returns (0,0) when dividing by 0.
-*)
-
-(**
-
-  The pseudo-code is:
-
-  if b = 0 : (0,0)
-
-  if b <> 0 and a = 0 : (0,0)
-
-  if b > 0 and a < 0 : let (q,r) = div_eucl_pos (-a) b in
-                       if r = 0 then (-q,0) else (-(q+1),b-r)
-
-  if b < 0 and a < 0 : let (q,r) = div_eucl (-a) (-b) in (q,-r)
-
-  if b < 0 and a > 0 : let (q,r) = div_eucl a (-b) in
-                       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| (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 :=
-  match a, b with
-    | Z0, _ => (0, 0)
-    | _, Z0 => (0, 0)
-    | Zpos a', Zpos _ => Zdiv_eucl_POS a' b
-    | Zneg a', Zpos _ =>
-      let (q, r) := Zdiv_eucl_POS a' b in
-	match r with
-	  | Z0 => (- q, 0)
-	  | _ => (- (q + 1), b - r)
-	end
-    | Zneg a', Zneg b' => let (q, r) := Zdiv_eucl_POS a' (Zpos b') in (q, - r)
-    | Zpos a', Zneg b' =>
-      let (q, r) := Zdiv_eucl_POS a' (Zpos b') in
-	match r with
-	  | Z0 => (- q, 0)
-	  | _ => (- (q + 1), b + r)
-	end
-  end.
-
-
-(** 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.
-
-(** Syntax *)
-
-Infix "/" := Zdiv : Z_scope.
-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)).
-
-*)
+Local Open Scope Z_scope.
 
+(** The definition and initial properties are now in file [Zdiv_def] *)
 
-(** * Main division theorem *)
+(** * Main division theorems *)
 
-(** First a lemma for two positive arguments *)
+(** NB: many things are stated twice for compatibility reasons *)
 
 Lemma Z_div_mod_POS :
   forall b:Z,
@@ -138,58 +28,19 @@ 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; 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)).
-case (Zgt_bool b (2 * r + 1));
- (rewrite BinInt.Zpos_xI; rewrite H0; split; [ ring | omega ]).
-
-intros p; case (Zdiv_eucl_POS p b); intros q r [H0 H1].
-generalize (Zgt_cases b (2 * r)).
-case (Zgt_bool b (2 * r)); rewrite BinInt.Zpos_xO;
- change (Zpos (xO p)) with (2 * Zpos p) in |- *; rewrite H0;
- (split; [ ring | omega ]).
-
-generalize (Zge_cases b 2).
-case (Zge_bool b 2); (intros; split; [ try ring | omega ]).
-omega.
+ intros b Hb a. apply Zgt_lt in Hb.
+ generalize (Zdiv_eucl_POS_eq a b Hb) (Zmod_POS_bound a b Hb).
+ destruct Zdiv_eucl_POS. auto.
 Qed.
 
-(** Then the usual situation of a positive [b] and no restriction on [a] *)
-
 Theorem Z_div_mod :
   forall a b:Z,
     b > 0 -> let (q, r) := Zdiv_eucl a b in a = b * q + r /\ 0 <= r < b.
 Proof.
-  intros a b; case a; case b; try (simpl in |- *; intros; omega).
-  unfold Zdiv_eucl in |- *; intros; apply Z_div_mod_POS; trivial.
-
-  intros; discriminate.
-
-  intros.
-  generalize (Z_div_mod_POS (Zpos p) H p0).
-  unfold Zdiv_eucl in |- *.
-  case (Zdiv_eucl_POS p0 (Zpos p)).
-  intros z z0.
-  case z0.
-
-  intros [H1 H2].
-  split; trivial.
-  change (Zneg p0) with (- Zpos p0); rewrite H1; ring.
-
-  intros p1 [H1 H2].
-  split; trivial.
-  change (Zneg p0) with (- Zpos p0); rewrite H1; ring.
-  generalize (Zorder.Zgt_pos_0 p1); omega.
-
-  intros p1 [H1 H2].
-  split; trivial.
-  change (Zneg p0) with (- Zpos p0); rewrite H1; ring.
-  generalize (Zorder.Zlt_neg_0 p1); omega.
-
-  intros; discriminate.
+ intros a b Hb. apply Zgt_lt in Hb.
+ assert (Hb' : b<>0) by (now destruct b).
+ generalize (Zdiv_eucl_eq a b Hb') (Zmod_pos_bound a b Hb).
+ unfold Zmod. destruct Zdiv_eucl. auto.
 Qed.
 
 (** For stating the fully general result, let's give a short name
@@ -217,37 +68,14 @@ 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 *.
+ intros a b Hb.
+ generalize (Zdiv_eucl_eq a b Hb)
+  (Zmod_pos_bound a b) (Zmod_neg_bound a b).
+ unfold Zmod. destruct Zdiv_eucl as (q,r).
+ intros EQ POS NEG.
+ split; auto.
+ red; destruct b.
+  now destruct Hb. left; now apply POS. right; now apply NEG.
 Qed.
 
 (** The same results as before, stated separately in terms of Zdiv and Zmod *)
@@ -258,26 +86,13 @@ Proof.
   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.
+Definition Z_mod_lt : forall a b:Z, b > 0 -> 0 <= a mod b < b
+ := fun a b Hb => Zmod_pos_bound a b (Zgt_lt _ _ Hb).
 
-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.
+Definition Z_mod_neg : forall a b:Z, b < 0 -> b < a mod b <= 0
+ := Zmod_neg_bound.
 
-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.
+Notation Z_div_mod_eq_full := Z_div_mod_eq_full (only parsing).
 
 Lemma Z_div_mod_eq : forall a b:Z, b > 0 -> a = b*(a/b) + (a mod b).
 Proof.
@@ -285,39 +100,10 @@ Proof.
 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.
+Proof. intros. rewrite Zmult_comm. now apply Z.mod_eq. 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.
-
-(** We know enough to prove that [Zdiv] and [Zmod] are instances of
-    one of the abstract Euclidean divisions of Numbers.
-    We hence benefit from generic results about this abstract division. *)
-
-Module Z.
-
- Definition div := Zdiv.
- Definition modulo := Zmod.
- Local Obligation Tactic := simpl_relation.
- Program Instance div_wd : Proper (eq==>eq==>eq) div.
- Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
-
- Definition div_mod := Z_div_mod_eq_full.
- Definition mod_pos_bound : forall a b:Z, 0<b -> 0<=a mod b<b.
- Proof. intros; apply Z_mod_lt; auto with zarith. Qed.
- Definition mod_neg_bound := Z_mod_neg.
-
- Include ZBinary.Z <+ ZDivFloor.ZDivProp.
-
-End Z.
+Proof. intros. apply Zmod_eq_full. now destruct b. Qed.
 
 (** Existence theorem *)
 
@@ -730,7 +516,10 @@ Proof.
 
 Lemma Zmod_divides : forall a b, b<>0 ->
  (a mod b = 0 <-> exists c, a = b*c).
-Proof. exact Z.mod_divides. Qed.
+Proof.
+ intros. rewrite Z.mod_divide; trivial.
+ split; intros (c,Hc); exists c; auto.
+Qed.
 
 (** * Compatibility *)
 
@@ -866,16 +655,6 @@ 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).
-*)
-
 (** * Division and modulo in Z agree with same in nat: *)
 
 Require Import NPeano.
@@ -901,3 +680,10 @@ Proof.
  rewrite <- div_Zdiv, <- inj_mult, <- inj_plus by trivial.
  now apply inj_eq, Nat.div_mod.
 Qed.
+
+
+(** For compatibility *)
+
+Notation Zdiv_eucl := Zdiv_eucl (only parsing).
+Notation Zdiv := Zdiv (only parsing).
+Notation Zmod := Zmod (only parsing).
diff --git a/theories/ZArith/Zdiv_def.v b/theories/ZArith/Zdiv_def.v
new file mode 100644
index 0000000000..a48170fd18
--- /dev/null
+++ b/theories/ZArith/Zdiv_def.v
@@ -0,0 +1,310 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import BinPos BinNat BinInt Zbool Zcompare Zorder Zabs Nnat Ndiv_def.
+Local Open Scope Z_scope.
+
+(** * Definitions of divisions for binary integers *)
+
+(** Concerning the many possible variants of integer divisions, see:
+
+    R. Boute, "The Euclidean definition of the functions div and mod",
+    ACM Transactions on Programming Languages and Systems,
+    Vol. 14, No.2, pp. 127-144, April 1992.
+
+   We provide here two flavours:
+
+    - convention Floor (F) : [Zdiv_eucl], [Zdiv], [Zmod]
+    - convention Trunc (T) : [Zquotrem], [Zquot], [Zrem]
+
+   A third one, the Euclid (E) convention, can be found in file
+   Zeuclid.v
+
+   For non-zero b, they all satisfy [a = b*(a/b) + (a mod b)]
+   and [ |a mod b| < |b| ], but the sign of the modulo will differ
+   when [a<0] and/or [b<0].
+
+*)
+
+(** * Floor *)
+
+(** [Zdiv_eucl] provides a Truncated-Toward-Bottom (a.k.a Floor)
+  Euclidean division. Its projections are named [Zdiv] and [Zmod].
+  These functions correspond to the `div` and `mod` of Haskell.
+  This is the historical convention of Coq.
+
+  The main properties of this convention are :
+    - we have [sgn (a mod b) = sgn (b)]
+    - [div a b] is the greatest integer smaller or equal to the exact
+      fraction [a/b].
+    - there is no easy sign rule.
+
+  In addition, note that we arbitrary take [a/0 = 0] and [a mod 0 = 0].
+*)
+
+(** First, a division for positive numbers. Even if the second
+   argument is a Z, the answer is arbitrary is it isn't a Zpos. *)
+
+Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) : Z * Z :=
+  match a with
+    | xH => if Zge_bool b 2 then (0, 1) else (1, 0)
+    | xO a' =>
+      let (q, r) := Zdiv_eucl_POS a' b in
+	let r' := 2 * r in
+	  if Zgt_bool b r' then (2 * q, r') else (2 * q + 1, r' - b)
+    | xI a' =>
+      let (q, r) := Zdiv_eucl_POS a' b in
+	let r' := 2 * r + 1 in
+	  if Zgt_bool b r' then (2 * q, r') else (2 * q + 1, r' - b)
+  end.
+
+(** Then the general euclidean division *)
+
+Definition Zdiv_eucl (a b:Z) : Z * Z :=
+  match a, b with
+    | 0, _ => (0, 0)
+    | _, 0 => (0, 0)
+    | Zpos a', Zpos _ => Zdiv_eucl_POS a' b
+    | Zneg a', Zpos _ =>
+      let (q, r) := Zdiv_eucl_POS a' b in
+	match r with
+	  | 0 => (- q, 0)
+	  | _ => (- (q + 1), b - r)
+	end
+    | Zneg a', Zneg b' =>
+      let (q, r) := Zdiv_eucl_POS a' (Zpos b') in (q, - r)
+    | Zpos a', Zneg b' =>
+      let (q, r) := Zdiv_eucl_POS a' (Zpos b') in
+	match r with
+	  | 0 => (- q, 0)
+	  | _ => (- (q + 1), b + r)
+	end
+  end.
+
+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.
+
+Infix "/" := Zdiv : Z_scope.
+Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
+
+
+(** * Trunc *)
+
+(** [Zquotrem] provides a Truncated-Toward-Zero Euclidean division.
+  Its projections are named [Zquot] and [Zrem]. These functions
+  correspond to the `quot` and `rem` of Haskell, and this division
+  convention is used in most programming languages, e.g. Ocaml.
+
+  With this convention:
+   - we have [sgn(a rem b) = sgn(a)]
+   - sign rule for division: [quot (-a) b = quot a (-b) = -(quot a b)]
+   - and for modulo: [a rem (-b) = a rem b] and [(-a) rem b = -(a rem b)]
+
+ Note that we arbitrary take here [quot a 0 = 0] and [a rem 0 = a].
+*)
+
+Definition Zquotrem (a b:Z) : Z * Z :=
+  match a, b with
+   | 0,  _ => (0, 0)
+   | _, 0  => (0, a)
+   | Zpos a, Zpos b =>
+     let (q, r) := Pdiv_eucl a b in (Z_of_N q, Z_of_N r)
+   | Zneg a, Zpos b =>
+     let (q, r) := Pdiv_eucl a b in (- Z_of_N q, - Z_of_N r)
+   | Zpos a, Zneg b =>
+     let (q, r) := Pdiv_eucl a b in (- Z_of_N q, Z_of_N r)
+   | Zneg a, Zneg b =>
+     let (q, r) := Pdiv_eucl a b in (Z_of_N q, - Z_of_N r)
+  end.
+
+Definition Zquot a b := fst (Zquotrem a b).
+Definition Zrem a b := snd (Zquotrem a b).
+
+Infix "÷" := Zquot (at level 40, left associativity) : Z_scope.
+Infix "rem" := Zrem (at level 40, no associativity) : Z_scope.
+
+
+
+(** * Euclid *)
+
+(** In this last convention, the remainder is always non-negative *)
+
+Definition Zeuclid_mod a b := Zmod a (Zabs b).
+Definition Zeuclid_div a b := (Zsgn b) * (Zdiv a (Zabs b)).
+
+
+
+(** * Correctness proofs *)
+
+(** Correctness proofs for Trunc *)
+
+Lemma Zdiv_eucl_POS_eq : forall a b, 0 < b ->
+  let (q, r) := Zdiv_eucl_POS a b in Zpos a = b * q + r.
+Proof.
+ intros a b Hb.
+ induction a; cbv beta iota delta [Zdiv_eucl_POS]; fold Zdiv_eucl_POS.
+ (* ~1 *)
+ destruct Zdiv_eucl_POS as (q,r); cbv zeta.
+ rewrite Zpos_xI, IHa, Zmult_plus_distr_r, Zmult_permute.
+ destruct Zgt_bool.
+ now rewrite Zplus_assoc.
+ now rewrite Zmult_plus_distr_r, Zmult_1_r, <- !Zplus_assoc, Zplus_minus.
+ (* ~0 *)
+ destruct Zdiv_eucl_POS as (q,r); cbv zeta.
+ rewrite (Zpos_xO a), IHa, Zmult_plus_distr_r, Zmult_permute.
+ destruct Zgt_bool; trivial.
+ now rewrite Zmult_plus_distr_r, Zmult_1_r, <- !Zplus_assoc, Zplus_minus.
+ (* ~1 *)
+ generalize (Zge_cases b 2); destruct Zge_bool; intros Hb'.
+ now rewrite Zmult_0_r.
+ replace b with 1. reflexivity.
+ apply Zle_antisym. now apply Zlt_le_succ in Hb. now apply Zlt_succ_le.
+Qed.
+
+Lemma Zdiv_eucl_eq : forall a b, b<>0 ->
+ let (q, r) := Zdiv_eucl a b in a = b * q + r.
+Proof.
+ intros [ |a|a] [ |b|b]; unfold Zdiv_eucl; trivial;
+  (now destruct 1) || intros _;
+  generalize (Zdiv_eucl_POS_eq a (Zpos b) (eq_refl _));
+  destruct Zdiv_eucl_POS as (q,r); try change (Zneg a) with (-Zpos a);
+  intros ->.
+ (* Zpos Zpos *)
+ reflexivity.
+ (* Zpos Zneg *)
+ rewrite <- (Zopp_neg b), Zmult_opp_comm.
+ destruct r as [ |r|r]; trivial.
+ rewrite Zopp_plus_distr, Zmult_plus_distr_r, <- Zplus_assoc. f_equal.
+ now rewrite <- Zmult_opp_comm, Zmult_1_r, Zplus_assoc, Zplus_opp_l.
+ rewrite Zopp_plus_distr, Zmult_plus_distr_r, <- Zplus_assoc. f_equal.
+ now rewrite <- Zmult_opp_comm, Zmult_1_r, Zplus_assoc, Zplus_opp_l.
+ (* Zneg Zpos *)
+ rewrite (Zopp_plus_distr _ r), Zopp_mult_distr_r.
+ destruct r as [ |r|r]; trivial; unfold Zminus.
+ rewrite Zopp_plus_distr, Zmult_plus_distr_r, <- Zplus_assoc. f_equal.
+ now rewrite <- Zmult_opp_comm, Zmult_1_r, Zplus_assoc, Zplus_opp_l.
+ rewrite Zopp_plus_distr, Zmult_plus_distr_r, <- Zplus_assoc. f_equal.
+ now rewrite <- Zmult_opp_comm, Zmult_1_r, Zplus_assoc, Zplus_opp_l.
+ (* Zneg Zneg *)
+ now rewrite (Zopp_plus_distr _ r), Zopp_mult_distr_l.
+Qed.
+
+Lemma Z_div_mod_eq_full : forall a b, b<>0 -> a = b*(a/b) + (a mod b).
+Proof.
+ intros a b Hb. generalize (Zdiv_eucl_eq a b Hb).
+ unfold Zdiv, Zmod. now destruct Zdiv_eucl.
+Qed.
+
+Lemma Zmod_POS_bound : forall a b, 0<b -> 0 <= snd (Zdiv_eucl_POS a b) < b.
+Proof.
+ assert (AUX : forall a p, a < Zpos (p~0) -> a - Zpos p < Zpos p).
+  intros. unfold Zminus. apply Zlt_plus_swap. unfold Zminus.
+  now rewrite Zopp_involutive, Zplus_diag_eq_mult_2, Zmult_comm.
+ intros a [|b|b] Hb; discriminate Hb || clear Hb.
+ induction a; cbv beta iota delta [Zdiv_eucl_POS]; fold Zdiv_eucl_POS.
+ (* ~1 *)
+ destruct Zdiv_eucl_POS as (q,r). cbv zeta.
+ simpl in IHa; destruct IHa as (Hr,Hr').
+ generalize (Zgt_cases (Zpos b) (2*r+1)). destruct Zgt_bool.
+ unfold snd in *.
+ split. apply Zplus_le_0_compat. now apply Zmult_le_0_compat. easy.
+  now apply Zgt_lt.
+ unfold snd in *.
+ split. now apply Zle_minus_le_0.
+  apply AUX.
+  destruct r as [|r|r]; try (now destruct Hr); try easy.
+  red. simpl. apply Pcompare_eq_Lt. exact Hr'.
+ (* ~0 *)
+ destruct Zdiv_eucl_POS as (q,r). cbv zeta.
+ simpl in IHa; destruct IHa as (Hr,Hr').
+ generalize (Zgt_cases (Zpos b) (2*r)). destruct Zgt_bool.
+ unfold snd in *.
+ split. now apply Zmult_le_0_compat.
+  now apply Zgt_lt.
+ unfold snd in *.
+ split. now apply Zle_minus_le_0.
+  apply AUX.
+  destruct r as [|r|r]; try (now destruct Hr); try easy.
+ (* 1 *)
+ generalize (Zge_cases (Zpos b) 2). destruct Zge_bool; simpl.
+ split. easy. now apply Zle_succ_l, Zge_le.
+ now split.
+Qed.
+
+Lemma Zmod_pos_bound : forall a b, 0 < b -> 0 <= a mod b < b.
+Proof.
+ intros a [|b|b] Hb; discriminate Hb || clear Hb.
+ destruct a as [|a|a]; unfold Zmod, Zdiv_eucl.
+ now split.
+ now apply Zmod_POS_bound.
+ generalize (Zmod_POS_bound a (Zpos b) (eq_refl _)).
+ destruct Zdiv_eucl_POS as (q,r). unfold snd. intros (Hr,Hr').
+ destruct r as [|r|r]; (now destruct Hr) || clear Hr.
+ now split.
+ split. now apply Zlt_le_weak, Zlt_plus_swap.
+ now apply Zlt_minus_simpl_swap.
+Qed.
+
+Lemma Zmod_neg_bound : forall a b, b < 0 -> b < a mod b <= 0.
+Proof.
+ intros a [|b|b] Hb; discriminate Hb || clear Hb.
+ destruct a as [|a|a]; unfold Zmod, Zdiv_eucl.
+ now split.
+ generalize (Zmod_POS_bound a (Zpos b) (eq_refl _)).
+ destruct Zdiv_eucl_POS as (q,r). unfold snd. intros (Hr,Hr').
+ destruct r as [|r|r]; (now destruct Hr) || clear Hr.
+ now split.
+ split. rewrite Zplus_comm. now apply (Zplus_lt_compat_r 0).
+ rewrite Zplus_comm. apply Zle_plus_swap. simpl. now apply Zlt_le_weak.
+ generalize (Zmod_POS_bound a (Zpos b) (eq_refl _)).
+ destruct Zdiv_eucl_POS as (q,r). unfold snd. intros (Hr,Hr').
+ split. red in Hr'. now rewrite Zcompare_opp in Hr'. now destruct r.
+Qed.
+
+(** Correctness proofs for Floor *)
+
+Theorem Zquotrem_eq: forall a b,
+  let (q,r) := Zquotrem a b in a = q * b + r.
+Proof.
+ destruct a, b; simpl; trivial;
+ generalize (Pdiv_eucl_correct p p0); case Pdiv_eucl; trivial;
+  intros q r H; try change (Zneg p) with (-Zpos p);
+  rewrite <- (Z_of_N_pos p), H, Z_of_N_plus, Z_of_N_mult; f_equal.
+ now rewrite Zmult_opp_comm.
+ now rewrite Zopp_plus_distr, Zopp_mult_distr_l.
+ now rewrite Zopp_plus_distr, Zopp_mult_distr_r.
+Qed.
+
+Lemma Z_quot_rem_eq : forall a b, a = b*(a÷b) + a rem b.
+Proof.
+ intros a b. rewrite Zmult_comm. generalize (Zquotrem_eq a b).
+ unfold Zquot, Zrem. now destruct Zquotrem.
+Qed.
+
+Lemma Zrem_bound : forall a b, 0<=a -> 0<b -> 0 <= a rem b < b.
+Proof.
+ intros a [|b|b] Ha Hb; discriminate Hb || clear Hb.
+ destruct a as [|a|a]; (now destruct Ha) || clear Ha.
+ compute. now split.
+ unfold Zrem, Zquotrem.
+ generalize (Pdiv_eucl_remainder a b). destruct Pdiv_eucl as (q,r).
+ simpl. split. apply Z_of_N_le_0.
+ destruct r; red; simpl; trivial.
+Qed.
+
+Lemma Zrem_opp_l : forall a b, (-a) rem b = - (a rem b).
+Proof.
+ intros [|a|a] [|b|b]; trivial; unfold Zrem;
+  simpl; destruct Pdiv_eucl; simpl; try rewrite Zopp_involutive; trivial.
+Qed.
+
+Lemma Zrem_opp_r : forall a b, a rem (-b) = a rem b.
+Proof.
+ intros [|a|a] [|b|b]; trivial; unfold Zrem; simpl;
+  destruct Pdiv_eucl; simpl; try rewrite Zopp_involutive; trivial.
+Qed.
diff --git a/theories/ZArith/Zeuclid.v b/theories/ZArith/Zeuclid.v
new file mode 100644
index 0000000000..ece227e100
--- /dev/null
+++ b/theories/ZArith/Zeuclid.v
@@ -0,0 +1,54 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Morphisms BinInt Zdiv_def ZBinary ZDivEucl.
+Local Open Scope Z_scope.
+
+(** * Definitions of division for binary integers, Euclid convention. *)
+
+(** In this convention, the remainder is always positive.
+    For other conventions, see file Zdiv_def.
+    To avoid collision with the other divisions, we place this one
+    under a module.
+*)
+
+Module ZEuclid.
+
+ Definition modulo a b := Zmod a (Zabs b).
+ Definition div a b := (Zsgn b) * (Zdiv a (Zabs b)).
+
+ Instance mod_wd : Proper (eq==>eq==>eq) modulo.
+ Proof. congruence. Qed.
+ Instance div_wd : Proper (eq==>eq==>eq) div.
+ Proof. congruence. Qed.
+
+ Theorem div_mod : forall a b, b<>0 ->
+  a = b*(div a b) + modulo a b.
+ Proof.
+  intros a b Hb. unfold div, modulo.
+  rewrite Zmult_assoc. rewrite Z.sgn_abs. apply Z.div_mod.
+  now destruct b.
+ Qed.
+
+ Lemma mod_always_pos : forall a b, b<>0 ->
+  0 <= modulo a b < Zabs b.
+ Proof.
+  intros a b Hb. unfold modulo.
+  apply Z.mod_pos_bound.
+  destruct b; compute; trivial. now destruct Hb.
+ Qed.
+
+ Lemma mod_bound_pos : forall a b, 0<=a -> 0<b -> 0 <= modulo a b < b.
+ Proof.
+  intros a b _ Hb. rewrite <- (Z.abs_eq b) at 3 by z_order.
+  apply mod_always_pos. z_order.
+ Qed.
+
+ Include ZEuclidProp Z Z Z.
+
+End ZEuclid.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 2866a38fda..c7e6d5750b 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -16,7 +16,7 @@ Require Import Zcompare.
 Require Import Zorder.
 Require Import Decidable.
 Require Import Peano_dec.
-Require Import Min Max Zmin Zmax.
+Require Import Min Max.
 Require Export Compare_dec.
 
 Open Local Scope Z_scope.
@@ -76,96 +76,62 @@ 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.
+Theorem inj_compare : forall n m:nat,
+ (Z_of_nat n ?= Z_of_nat m) = nat_compare n m.
 Proof.
-  intros x y; intros H; elim H;
-    [ unfold Zle in |- *; elim (Zcompare_Eq_iff_eq (Z_of_nat x) (Z_of_nat x));
-      intros H1 H2; rewrite H2; [ discriminate | trivial with arith ]
-      | intros m H1 H2; apply Zle_trans with (Z_of_nat m);
-	[ assumption | rewrite inj_S; apply Zle_succ ] ].
+ induction n; destruct m; trivial.
+ rewrite 2 inj_S, Zcompare_succ_compat. now simpl.
 Qed.
 
-Theorem inj_lt : forall n m:nat, (n < m)%nat -> Z_of_nat n < Z_of_nat m.
-Proof.
-  intros x y H; apply Zgt_lt; apply Zle_succ_gt; rewrite <- inj_S; apply inj_le;
-    exact H.
-Qed.
+(* Both ways ... *)
 
-Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m.
+Theorem inj_le_iff : 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.
+ intros. unfold Zle. rewrite inj_compare. apply nat_compare_le.
 Qed.
 
-Theorem inj_gt : forall n m:nat, (n > m)%nat -> Z_of_nat n > Z_of_nat m.
+Theorem inj_lt_iff : 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.
+ intros. unfold Zlt. rewrite inj_compare. apply nat_compare_lt.
 Qed.
 
-(** The other way ... *)
-
-Theorem inj_le_rev : forall n m:nat, Z_of_nat n <= Z_of_nat m -> (n <= m)%nat.
+Theorem inj_ge_iff : forall n m:nat, (n>=m)%nat <-> Z_of_nat n >= Z_of_nat m.
 Proof.
-  intros x y H.
-  destruct (le_lt_dec x y) as [H0|H0]; auto.
-  exfalso.
-  assert (H1:=inj_lt _ _ H0).
-  red in H; red in H1.
-  rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto.
+ intros. unfold Zge. rewrite inj_compare. apply nat_compare_ge.
 Qed.
 
-Theorem inj_lt_rev : forall n m:nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat.
+Theorem inj_gt_iff : forall n m:nat, (n>m)%nat <-> Z_of_nat n > Z_of_nat m.
 Proof.
-  intros x y H.
-  destruct (le_lt_dec y x) as [H0|H0]; auto.
-  exfalso.
-  assert (H1:=inj_le _ _ H0).
-  red in H; red in H1.
-  rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto.
+ intros. unfold Zgt. rewrite inj_compare. apply nat_compare_gt.
 Qed.
 
-Theorem inj_ge_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 y x) as [H0|H0]; auto.
-  exfalso.
-  assert (H1:=inj_gt _ _ H0).
-  red in H; red in H1.
-  rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto.
-Qed.
+(** One way ... *)
 
-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.
-  exfalso.
-  assert (H1:=inj_ge _ _ H0).
-  red in H; red in H1.
-  rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto.
-Qed.
+Theorem inj_le : forall n m:nat, (n <= m)%nat -> Z_of_nat n <= Z_of_nat m.
+Proof. apply inj_le_iff. Qed.
 
-(* Both ways ... *)
+Theorem inj_lt : forall n m:nat, (n < m)%nat -> Z_of_nat n < Z_of_nat m.
+Proof. apply inj_lt_iff. Qed.
 
-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_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m.
+Proof. apply inj_ge_iff. 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_gt : forall n m:nat, (n > m)%nat -> Z_of_nat n > Z_of_nat m.
+Proof. apply inj_gt_iff. 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.
+(** The other way ... *)
 
-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.
+Theorem inj_le_rev : forall n m:nat, Z_of_nat n <= Z_of_nat m -> (n <= m)%nat.
+Proof. apply inj_le_iff. Qed.
+
+Theorem inj_lt_rev : forall n m:nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat.
+Proof. apply inj_lt_iff. Qed.
+
+Theorem inj_ge_rev : forall n m:nat, Z_of_nat n >= Z_of_nat m -> (n >= m)%nat.
+Proof. apply inj_ge_iff. Qed.
+
+Theorem inj_gt_rev : forall n m:nat, Z_of_nat n > Z_of_nat m -> (n > m)%nat.
+Proof. apply inj_gt_iff. Qed.
 
 (** Injection and usual operations *)
 
@@ -208,38 +174,38 @@ 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_minus1; trivial.
+ apply inj_le, Zle_minus_le_0 in H. revert H. unfold Zle.
+ case Zcompare_spec; 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.
+ rewrite inj_minus2; trivial.
+ apply inj_lt, Zlt_gt in H.
+ apply (Zplus_gt_compat_r _ _ (- Z_of_nat m)) in 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.
+ intros n m. unfold Zmin. rewrite inj_compare.
+ case nat_compare_spec; intros; f_equal.
+ subst. apply min_idempotent.
+ apply min_l. auto with arith.
+ apply min_r. auto with arith.
 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.
+ intros n m. unfold Zmax. rewrite inj_compare.
+ case nat_compare_spec; intros; f_equal.
+ subst. apply max_idempotent.
+ apply max_r. auto with arith.
+ apply max_l. auto with arith.
 Qed.
 
 (** Composition of injections **)
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
new file mode 100644
index 0000000000..307faccfee
--- /dev/null
+++ b/theories/ZArith/Zquot.v
@@ -0,0 +1,511 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \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 Morphisms Zdiv.
+Require Export Ndiv_def Zdiv_def.
+Require ZBinary ZDivTrunc.
+
+Local Open Scope Z_scope.
+
+(** This file provides results about the Round-Toward-Zero Euclidean
+  division [Zquotrem], whose projections are [Zquot] and [Zrem].
+  Definition of this division can be found in file [Zdiv_def].
+
+  This division and the one defined in Zdiv agree only on positive
+  numbers. Otherwise, Zdiv performs Round-Toward-Bottom (a.k.a Floor).
+
+  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.
+*)
+
+(** * Relation between division on N and on Z. *)
+
+Lemma Ndiv_Zquot : 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, Zquot; simpl; destruct Pdiv_eucl; auto.
+Qed.
+
+Lemma Nmod_Zrem : forall a b:N,
+  Z_of_N (a mod b) = (Z_of_N a) rem (Z_of_N b).
+Proof.
+  intros.
+  destruct a; destruct b; simpl; auto.
+  unfold Nmod, Zrem; 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].
+*)
+
+Notation Z_quot_rem_eq := Z_quot_rem_eq (only parsing).
+
+(** Then, the inequalities constraining the remainder:
+    The remainder is bounded by the divisor, in term of absolute values *)
+
+Theorem Zrem_lt : forall a b:Z, b<>0 ->
+  Zabs (a rem 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 Zrem, Zquotrem;
+  generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl;
+  try rewrite Zabs_Zopp; rewrite Zabs_eq; auto using Z_of_N_le_0;
+  intros LT; apply (Z_of_N_lt _ _ LT).
+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 Zrem_sgn : forall a b:Z,
+  0 <= Zsgn (a rem b) * Zsgn a.
+Proof.
+  destruct b as [ |b|b]; destruct a as [ |a|a]; simpl; auto with zarith;
+  unfold Zrem, Zquotrem; 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 Zrem_sgn2 : forall a b:Z,
+  0 <= (a rem b) * a.
+Proof.
+  intros; rewrite <-Zsgn_pos_iff, Zsgn_Zmult; apply Zrem_sgn.
+Qed.
+
+(** Reformulation of [Zquot_lt] and [Zrem_sgn] in 2
+  then 4 particular cases. *)
+
+Theorem Zrem_lt_pos : forall a b:Z, 0<=a -> b<>0 ->
+  0 <= a rem b < Zabs b.
+Proof.
+  intros.
+  assert (0 <= a rem b).
+   generalize (Zrem_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 (Zrem_lt a b H0); romega with *.
+Qed.
+
+Theorem Zrem_lt_neg : forall a b:Z, a<=0 -> b<>0 ->
+  -Zabs b < a rem b <= 0.
+Proof.
+  intros.
+  assert (a rem b <= 0).
+   generalize (Zrem_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 (Zrem_lt a b H0); romega with *.
+Qed.
+
+Theorem Zrem_lt_pos_pos : forall a b:Z, 0<=a -> 0<b -> 0 <= a rem b < b.
+Proof.
+  intros; generalize (Zrem_lt_pos a b); romega with *.
+Qed.
+
+Theorem Zrem_lt_pos_neg : forall a b:Z, 0<=a -> b<0 -> 0 <= a rem b < -b.
+Proof.
+  intros; generalize (Zrem_lt_pos a b); romega with *.
+Qed.
+
+Theorem Zrem_lt_neg_pos : forall a b:Z, a<=0 -> 0<b -> -b < a rem b <= 0.
+Proof.
+  intros; generalize (Zrem_lt_neg a b); romega with *.
+Qed.
+
+Theorem Zrem_lt_neg_neg : forall a b:Z, a<=0 -> b<0 -> b < a rem b <= 0.
+Proof.
+  intros; generalize (Zrem_lt_neg a b); romega with *.
+Qed.
+
+(** * Division and Opposite *)
+
+(* The precise equalities that are invalid with "historic" Zdiv. *)
+
+Theorem Zquot_opp_l : forall a b:Z, (-a)÷b = -(a÷b).
+Proof.
+ destruct a; destruct b; simpl; auto;
+  unfold Zquot, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith.
+Qed.
+
+Theorem Zquot_opp_r : forall a b:Z, a÷(-b) = -(a÷b).
+Proof.
+ destruct a; destruct b; simpl; auto;
+  unfold Zquot, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith.
+Qed.
+
+Theorem Zrem_opp_l : forall a b:Z, (-a) rem b = -(a rem b).
+Proof.
+ destruct a; destruct b; simpl; auto;
+  unfold Zrem, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith.
+Qed.
+
+Theorem Zrem_opp_r : forall a b:Z, a rem (-b) = a rem b.
+Proof.
+ destruct a; destruct b; simpl; auto;
+  unfold Zrem, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith.
+Qed.
+
+Theorem Zquot_opp_opp : forall a b:Z, (-a)÷(-b) = a÷b.
+Proof.
+ destruct a; destruct b; simpl; auto;
+  unfold Zquot, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith.
+Qed.
+
+Theorem Zrem_opp_opp : forall a b:Z, (-a) rem (-b) = -(a rem b).
+Proof.
+ destruct a; destruct b; simpl; auto;
+  unfold Zrem, Zquotrem; 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 Zquot_mod_unique_full:
+ forall a b q r, Remainder a b r ->
+   a = b*q + r -> q = a÷b /\ r = a rem b.
+Proof.
+  destruct 1 as [(H,H0)|(H,H0)]; intros.
+  apply Zdiv_mod_unique with b; auto.
+  apply Zrem_lt_pos; auto.
+  romega with *.
+  rewrite <- H1; apply Z_quot_rem_eq.
+
+  rewrite <- (Zopp_involutive a).
+  rewrite Zquot_opp_l, Zrem_opp_l.
+  generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (-a rem b)).
+  generalize (Zrem_lt_pos (-a) b).
+  rewrite <-Z_quot_rem_eq, <-Zopp_mult_distr_r, <-Zopp_plus_distr, <-H1.
+  romega with *.
+Qed.
+
+Theorem Zquot_unique_full:
+ forall a b q r, Remainder a b r ->
+  a = b*q + r -> q = a÷b.
+Proof.
+ intros; destruct (Zquot_mod_unique_full a b q r); auto.
+Qed.
+
+Theorem Zquot_unique:
+ forall a b q r, 0 <= a -> 0 <= r < b ->
+   a = b*q + r -> q = a÷b.
+Proof. exact Z.quot_unique. Qed.
+
+Theorem Zrem_unique_full:
+ forall a b q r, Remainder a b r ->
+  a = b*q + r -> r = a rem b.
+Proof.
+ intros; destruct (Zquot_mod_unique_full a b q r); auto.
+Qed.
+
+Theorem Zrem_unique:
+ forall a b q r, 0 <= a -> 0 <= r < b ->
+   a = b*q + r -> r = a rem b.
+Proof. exact Z.rem_unique. Qed.
+
+(** * Basic values of divisions and modulo. *)
+
+Lemma Zrem_0_l: forall a, 0 rem a = 0.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zrem_0_r: forall a, a rem 0 = a.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zquot_0_l: forall a, 0÷a = 0.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zquot_0_r: forall a, a÷0 = 0.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zrem_1_r: forall a, a rem 1 = 0.
+Proof. exact Z.rem_1_r. Qed.
+
+Lemma Zquot_1_r: forall a, a÷1 = a.
+Proof. exact Z.quot_1_r. Qed.
+
+Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Zquot_1_r Zrem_1_r
+ : zarith.
+
+Lemma Zquot_1_l: forall a, 1 < a -> 1÷a = 0.
+Proof. exact Z.quot_1_l. Qed.
+
+Lemma Zrem_1_l: forall a, 1 < a ->  1 rem a = 1.
+Proof. exact Z.rem_1_l. Qed.
+
+Lemma Z_quot_same : forall a:Z, a<>0 -> a÷a = 1.
+Proof. exact Z.quot_same. Qed.
+
+Ltac zero_or_not a :=
+  destruct (Z_eq_dec a 0);
+  [subst; rewrite ?Zrem_0_l, ?Zquot_0_l, ?Zrem_0_r, ?Zquot_0_r;
+   auto with zarith|].
+
+Lemma Z_rem_same : forall a, a rem a = 0.
+Proof. intros. zero_or_not a. apply Z.rem_same; auto. Qed.
+
+Lemma Z_rem_mult : forall a b, (a*b) rem b = 0.
+Proof. intros. zero_or_not b. apply Z.rem_mul; auto. Qed.
+
+Lemma Z_quot_mult : forall a b:Z, b <> 0 -> (a*b)÷b = a.
+Proof. exact Z.quot_mul. Qed.
+
+(** * Order results about Zrem and Zquot *)
+
+(* Division of positive numbers is positive. *)
+
+Lemma Z_quot_pos: forall a b, 0 <= a -> 0 <= b -> 0 <= a÷b.
+Proof. intros. zero_or_not b. apply Z.quot_pos; auto with zarith. Qed.
+
+(** As soon as the divisor is greater or equal than 2,
+    the division is strictly decreasing. *)
+
+Lemma Z_quot_lt : forall a b:Z, 0 < a -> 2 <= b -> a÷b < a.
+Proof. intros. apply Z.quot_lt; auto with zarith. Qed.
+
+(** A division of a small number by a bigger one yields zero. *)
+
+Theorem Zquot_small: forall a b, 0 <= a < b -> a÷b = 0.
+Proof. exact Z.quot_small. Qed.
+
+(** Same situation, in term of modulo: *)
+
+Theorem Zrem_small: forall a n, 0 <= a < n -> a rem n = a.
+Proof. exact Z.rem_small. Qed.
+
+(** [Zge] is compatible with a positive division. *)
+
+Lemma Z_quot_monotone : forall a b c, 0<=c -> a<=b -> a÷c <= b÷c.
+Proof. intros. zero_or_not c. apply Z.quot_le_mono; auto with zarith. Qed.
+
+(** With our choice of division, rounding of (a÷b) is always done toward zero: *)
+
+Lemma Z_mult_quot_le : forall a b:Z, 0 <= a -> 0 <= b*(a÷b) <= a.
+Proof. intros. zero_or_not b. apply Z.mul_quot_le; auto with zarith. Qed.
+
+Lemma Z_mult_quot_ge : forall a b:Z, a <= 0 -> a <= b*(a÷b) <= 0.
+Proof. intros. zero_or_not b. apply Z.mul_quot_ge; auto with zarith. Qed.
+
+(** The previous inequalities between [b*(a÷b)] and [a] are exact
+    iff the modulo is zero. *)
+
+Lemma Z_quot_exact_full : forall a b:Z, a = b*(a÷b) <-> a rem b = 0.
+Proof. intros. zero_or_not b. intuition. apply Z.quot_exact; auto. Qed.
+
+(** A modulo cannot grow beyond its starting point. *)
+
+Theorem Zrem_le: forall a b, 0 <= a -> 0 <= b -> a rem b <= a.
+Proof. intros. zero_or_not b. apply Z.rem_le; auto with zarith. Qed.
+
+(** Some additionnal inequalities about Zdiv. *)
+
+Theorem Zquot_le_upper_bound:
+  forall a b q, 0 < b -> a <= q*b -> a÷b <= q.
+Proof. intros a b q; rewrite Zmult_comm; apply Z.quot_le_upper_bound. Qed.
+
+Theorem Zquot_lt_upper_bound:
+  forall a b q, 0 <= a -> 0 < b -> a < q*b -> a÷b < q.
+Proof. intros a b q; rewrite Zmult_comm; apply Z.quot_lt_upper_bound. Qed.
+
+Theorem Zquot_le_lower_bound:
+  forall a b q, 0 < b -> q*b <= a -> q <= a÷b.
+Proof. intros a b q; rewrite Zmult_comm; apply Z.quot_le_lower_bound. Qed.
+
+Theorem Zquot_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 Zquot; 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) rem 2 = -1 <> 1 = 9 rem 2 *)
+
+Lemma Z_rem_plus : forall a b c:Z,
+ 0 <= (a+b*c) * a ->
+ (a + b * c) rem c = a rem c.
+Proof. intros. zero_or_not c. apply Z.rem_add; auto with zarith. Qed.
+
+Lemma Z_quot_plus : forall a b c:Z,
+ 0 <= (a+b*c) * a -> c<>0 ->
+ (a + b * c) ÷ c = a ÷ c + b.
+Proof. intros. apply Z.quot_add; auto with zarith. Qed.
+
+Theorem Z_quot_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. apply Z.quot_add_l; auto with zarith. Qed.
+
+(** Cancellations. *)
+
+Lemma Zquot_mult_cancel_r : forall a b c:Z,
+ c<>0 -> (a*c)÷(b*c) = a÷b.
+Proof. intros. zero_or_not b. apply Z.quot_mul_cancel_r; auto. Qed.
+
+Lemma Zquot_mult_cancel_l : forall a b c:Z,
+ c<>0 -> (c*a)÷(c*b) = a÷b.
+Proof.
+ intros. rewrite (Zmult_comm c b). zero_or_not b.
+ rewrite (Zmult_comm b c). apply Z.quot_mul_cancel_l; auto.
+Qed.
+
+Lemma Zmult_rem_distr_l: forall a b c,
+  (c*a) rem (c*b) = c * (a rem b).
+Proof.
+ intros. zero_or_not c. rewrite (Zmult_comm c b). zero_or_not b.
+ rewrite (Zmult_comm b c). apply Z.mul_rem_distr_l; auto.
+Qed.
+
+Lemma Zmult_rem_distr_r: forall a b c,
+  (a*c) rem (b*c) = (a rem b) * c.
+Proof.
+ intros. zero_or_not b. rewrite (Zmult_comm b c). zero_or_not c.
+ rewrite (Zmult_comm c b). apply Z.mul_rem_distr_r; auto.
+Qed.
+
+(** Operations modulo. *)
+
+Theorem Zrem_rem: forall a n, (a rem n) rem n = a rem n.
+Proof. intros. zero_or_not n. apply Z.rem_rem; auto. Qed.
+
+Theorem Zmult_rem: forall a b n,
+ (a * b) rem n = ((a rem n) * (b rem n)) rem n.
+Proof. intros. zero_or_not n. apply Z.mul_rem; auto. Qed.
+
+(** addition and modulo
+
+  Generally speaking, unlike with Zdiv, we don't have
+       (a+b) rem n = (a rem n + b rem n) rem n
+  for any a and b.
+  For instance, take (8 + (-10)) rem 3 = -2 whereas
+  (8 rem 3 + (-10 rem 3)) rem 3 = 1. *)
+
+Theorem Zplus_rem: forall a b n,
+ 0 <= a * b ->
+ (a + b) rem n = (a rem n + b rem n) rem n.
+Proof. intros. zero_or_not n. apply Z.add_rem; auto. Qed.
+
+Lemma Zplus_rem_idemp_l: forall a b n,
+ 0 <= a * b ->
+ (a rem n + b) rem n = (a + b) rem n.
+Proof. intros. zero_or_not n. apply Z.add_rem_idemp_l; auto. Qed.
+
+Lemma Zplus_rem_idemp_r: forall a b n,
+ 0 <= a*b ->
+ (b + a rem n) rem n = (b + a) rem n.
+Proof.
+ intros. zero_or_not n. apply Z.add_rem_idemp_r; auto.
+ rewrite Zmult_comm; auto. Qed.
+
+Lemma Zmult_rem_idemp_l: forall a b n, (a rem n * b) rem n = (a * b) rem n.
+Proof. intros. zero_or_not n. apply Z.mul_rem_idemp_l; auto. Qed.
+
+Lemma Zmult_rem_idemp_r: forall a b n, (b * (a rem n)) rem n = (b * a) rem n.
+Proof. intros. zero_or_not n. apply Z.mul_rem_idemp_r; auto. Qed.
+
+(** Unlike with Zdiv, the following result is true without restrictions. *)
+
+Lemma Zquot_Zquot : forall a b c, (a÷b)÷c = a÷(b*c).
+Proof.
+ intros. zero_or_not b. rewrite Zmult_comm. zero_or_not c.
+ rewrite Zmult_comm. apply Z.quot_quot; auto.
+Qed.
+
+(** A last inequality: *)
+
+Theorem Zquot_mult_le:
+ forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a÷b) <= (c*a)÷b.
+Proof. intros. zero_or_not b. apply Z.quot_mul_le; auto with zarith. Qed.
+
+(** Zrem is related to divisibility (see more in Znumtheory) *)
+
+Lemma Zrem_divides : forall a b,
+ a rem b = 0 <-> exists c, a = b*c.
+Proof.
+ intros. zero_or_not b. firstorder.
+ rewrite Z.rem_divide; trivial. split; intros (c,Hc); exists c; auto.
+Qed.
+
+(** * Interaction with "historic" Zdiv *)
+
+(** They agree at least on positive numbers: *)
+
+Theorem Zquotrem_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b ->
+  a÷b = a/b /\ a rem b = a mod b.
+Proof.
+  intros.
+  apply Zdiv_mod_unique with b.
+  apply Zrem_lt_pos; auto with zarith.
+  rewrite Zabs_eq; auto with *; apply Z_mod_lt; auto with *.
+  rewrite <- Z_div_mod_eq; auto with *.
+  symmetry; apply Z_quot_rem_eq; auto with *.
+Qed.
+
+Theorem Zquot_Zdiv_pos : forall a b, 0 <= a -> 0 <= b ->
+  a÷b = a/b.
+Proof.
+ intros a b Ha Hb.
+ destruct (Zle_lt_or_eq _ _ Hb).
+ generalize (Zquotrem_Zdiv_eucl_pos a b Ha H); intuition.
+ subst; rewrite Zquot_0_r, Zdiv_0_r; reflexivity.
+Qed.
+
+Theorem Zrem_Zmod_pos : forall a b, 0 <= a -> 0 < b ->
+  a rem b = a mod b.
+Proof.
+ intros a b Ha Hb; generalize (Zquotrem_Zdiv_eucl_pos a b Ha Hb);
+ intuition.
+Qed.
+
+(** Modulos are null at the same places *)
+
+Theorem Zrem_Zmod_zero : forall a b, b<>0 ->
+ (a rem b = 0 <-> a mod b = 0).
+Proof.
+ intros.
+ rewrite Zrem_divides, Zmod_divides; intuition.
+Qed.
diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget
index bfc52d3e41..ef18d67c7b 100644
--- a/theories/ZArith/vo.itarget
+++ b/theories/ZArith/vo.itarget
@@ -21,8 +21,8 @@ Zmin.vo
 Zmisc.vo
 Znat.vo
 Znumtheory.vo
-ZOdiv_def.vo
-ZOdiv.vo
+Zdiv_def.vo
+Zquot.vo
 Zorder.vo
 Zpow_def.vo
 Zpower.vo
@@ -31,4 +31,5 @@ Zsqrt_compat.vo
 Zwf.vo
 Zsqrt_def.vo
 Zlog_def.vo
-Zgcd_def.vo
\ No newline at end of file
+Zgcd_def.vo
+Zeuclid.vo