Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def

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

9 files changed, 199 insertions, 255 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index f19baf4d1..0e54c453b 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -88,7 +88,7 @@ Theorem div_unique_pos:
 Proof. intros; apply div_unique with r; auto. Qed.
 
 Theorem div_unique_neg:
- forall a b q r, 0<=r<b -> a == b*q + r -> q == a/b.
+ forall a b q r, b<r<=0 -> a == b*q + r -> q == a/b.
 Proof. intros; apply div_unique with r; auto. Qed.
 
 Theorem mod_unique:
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 8e53e4d62..173a8f177 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-Require Import ZArith Zquot.
+Require Import ZArith.
 Require Import BigNumPrelude.
 Require Import NSig.
 Require Import ZSig.
@@ -503,22 +503,28 @@ Module Make (N:NType) <: ZType.
 
  Lemma spec_quot : forall x y, to_Z (quot x y) = (to_Z x) ÷ (to_Z y).
  Proof.
-  intros [x|x] [y|y]; simpl; symmetry;
-   rewrite N.spec_div, ?Zquot_opp_r, ?Zquot_opp_l, ?Zopp_involutive;
-   rewrite Zquot_Zdiv_pos; trivial using N.spec_pos.
+  intros [x|x] [y|y]; simpl; symmetry; rewrite N.spec_div;
+  (* Nota: we rely here on [forall a b, a ÷ 0 = b / 0] *)
+  destruct (Z.eq_dec (N.to_Z y) 0) as [EQ|NEQ];
+    try (rewrite EQ; now destruct (N.to_Z x));
+  rewrite ?Z.quot_opp_r, ?Z.quot_opp_l, ?Z.opp_involutive, ?Z.opp_inj_wd;
+  trivial; apply Z.quot_div_nonneg;
+   generalize (N.spec_pos x) (N.spec_pos y); Z.order.
  Qed.
 
  Lemma spec_rem : forall x y,
-   to_Z (rem x y) = Zrem (to_Z x) (to_Z y).
+   to_Z (rem x y) = Z.rem (to_Z x) (to_Z y).
  Proof.
   intros x y. unfold rem. rewrite spec_eqb, spec_0.
   case Z.eqb_spec; intros Hy.
-  now rewrite Hy, Zrem_0_r.
+  (* Nota: we rely here on [Z.rem a 0 = a] *)
+  rewrite Hy. now destruct (to_Z x).
   destruct x as [x|x], y as [y|y]; simpl in *; symmetry;
-   rewrite N.spec_modulo, ?Zrem_opp_r, ?Zrem_opp_l, ?Zopp_involutive;
-   try rewrite Z.eq_opp_l, Z.opp_0 in Hy;
-   rewrite Zrem_Zmod_pos; generalize (N.spec_pos x) (N.spec_pos y);
-   Z.order.
+   rewrite ?Z.eq_opp_l, ?Z.opp_0 in Hy;
+   rewrite N.spec_modulo, ?Z.rem_opp_r, ?Z.rem_opp_l, ?Z.opp_involutive,
+    ?Z.opp_inj_wd;
+   trivial; apply Z.rem_mod_nonneg;
+    generalize (N.spec_pos x) (N.spec_pos y); Z.order.
  Qed.
 
  Definition gcd x y :=
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 6facd3c3a..390b52ebe 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -10,7 +10,7 @@ Require Import Bool ZArith OrdersFacts Nnat ZAxioms ZSig.
 
 (** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *)
 
-Module ZTypeIsZAxioms (Import Z : ZType').
+Module ZTypeIsZAxioms (Import ZZ : ZType').
 
 Hint Rewrite
  spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
@@ -53,7 +53,7 @@ Qed.
 
 Section Induction.
 
-Variable A : Z.t -> Prop.
+Variable A : ZZ.t -> Prop.
 Hypothesis A_wd : Proper (eq==>iff) A.
 Hypothesis A0 : A 0.
 Hypothesis AS : forall n, A n <-> A (succ n).
@@ -173,7 +173,7 @@ Proof.
  intros. zify. apply Z.compare_antisym.
 Qed.
 
-Include BoolOrderFacts Z Z Z [no inline].
+Include BoolOrderFacts ZZ ZZ ZZ [no inline].
 
 Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare.
 Proof.
@@ -388,23 +388,23 @@ Program Instance rem_wd : Proper (eq==>eq==>eq) rem.
 
 Theorem quot_rem : forall a b, ~b==0 -> a == b*(quot a b) + rem a b.
 Proof.
-intros a b _. zify. apply Z_quot_rem_eq.
+intros a b. zify. apply Z.quot_rem.
 Qed.
 
 Theorem rem_bound_pos :
  forall a b, 0<=a -> 0<b -> 0 <= rem a b /\ rem a b < b.
 Proof.
-intros a b. zify. intros. now apply Zrem_bound.
+intros a b. zify. apply Z.rem_bound_pos.
 Qed.
 
 Theorem rem_opp_l : forall a b, ~b==0 -> rem (-a) b == -(rem a b).
 Proof.
-intros a b _. zify. apply Zrem_opp_l.
+intros a b. zify. apply Z.rem_opp_l.
 Qed.
 
 Theorem rem_opp_r : forall a b, ~b==0 -> rem a (-b) == rem a b.
 Proof.
-intros a b _. zify. apply Zrem_opp_r.
+intros a b. zify. apply Z.rem_opp_r.
 Qed.
 
 (** Gcd *)
@@ -520,6 +520,6 @@ Qed.
 
 End ZTypeIsZAxioms.
 
-Module ZType_ZAxioms (Z : ZType)
- <: ZAxiomsSig <: OrderFunctions Z <: HasMinMax Z
- := Z <+ ZTypeIsZAxioms.
+Module ZType_ZAxioms (ZZ : ZType)
+ <: ZAxiomsSig <: OrderFunctions ZZ <: HasMinMax ZZ
+ := ZZ <+ ZTypeIsZAxioms.
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index a935c7dac..239d55cdc 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -13,7 +13,7 @@ Require Export ZArith_base.
 (** Extra definitions *)
 
 Require Export
- Zpow_def Zsqrt_def Zlog_def Zdiv_def Zdigits_def.
+ Zpow_def Zsqrt_def Zlog_def Zdigits_def.
 
 (** Extra modules using [Omega] or [Ring]. *)
 
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 477e2e122..e5a92024f 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -13,10 +13,21 @@
 
 Require Export ZArith_base.
 Require Import Zbool Omega ZArithRing Zcomplements Setoid Morphisms.
-Require Import Zdiv_def.
 Local Open Scope Z_scope.
 
-(** The definition and initial properties are now in file [Zdiv_def] *)
+(** The definition of the division is now in [BinIntDef], the initial
+    specifications and properties are in [BinInt]. *)
+
+Notation Zdiv_eucl_POS := Z.pos_div_eucl (only parsing).
+Notation Zdiv_eucl := Z.div_eucl (only parsing).
+Notation Zdiv := Z.div (only parsing).
+Notation Zmod := Z.modulo (only parsing).
+
+Notation Zdiv_eucl_eq := Z.div_eucl_eq (only parsing).
+Notation Z_div_mod_eq_full := Z.div_mod (only parsing).
+Notation Zmod_POS_bound := Z.pos_div_eucl_bound (only parsing).
+Notation Zmod_pos_bound := Z.mod_pos_bound (only parsing).
+Notation Zmod_neg_bound := Z.mod_neg_bound (only parsing).
 
 (** * Main division theorems *)
 
@@ -26,21 +37,21 @@ Lemma Z_div_mod_POS :
   forall b:Z,
     b > 0 ->
     forall a:positive,
-      let (q, r) := Zdiv_eucl_POS a b in Zpos a = b * q + r /\ 0 <= r < b.
+      let (q, r) := Z.pos_div_eucl a b in Zpos a = b * q + r /\ 0 <= r < b.
 Proof.
- 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.
+ intros b Hb a. Z.swap_greater.
+ generalize (Z.pos_div_eucl_eq a b Hb) (Z.pos_div_eucl_bound a b Hb).
+ destruct Z.pos_div_eucl. rewrite Z.mul_comm. auto.
 Qed.
 
-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.
+Theorem Z_div_mod a b :
+  b > 0 ->
+  let (q, r) := Z.div_eucl a b in a = b * q + r /\ 0 <= r < b.
 Proof.
- intros a b Hb. apply Zgt_lt in Hb.
+ Z.swap_greater. intros 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.
+ generalize (Z.div_eucl_eq a b Hb') (Z.mod_pos_bound a b Hb).
+ unfold Z.modulo. destruct Z.div_eucl. auto.
 Qed.
 
 (** For stating the fully general result, let's give a short name
@@ -50,7 +61,7 @@ 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.
+Definition Remainder_alt r b :=  Z.abs r < Z.abs b /\ Z.sgn r <> - Z.sgn 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. *)
@@ -64,14 +75,14 @@ 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.
+Theorem Z_div_mod_full a b :
+  b <> 0 ->
+  let (q, r) := Z.div_eucl a b in a = b * q + r /\ Remainder r b.
 Proof.
- 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 Hb.
+ generalize (Z.div_eucl_eq a b Hb)
+  (Z.mod_pos_bound a b) (Z.mod_neg_bound a b).
+ unfold Z.modulo. destruct Z.div_eucl as (q,r).
  intros EQ POS NEG.
  split; auto.
  red; destruct b.
@@ -80,29 +91,27 @@ 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.
+Lemma Z_mod_remainder a b : 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.
+  unfold Z.modulo; intros Hb; generalize (Z_div_mod_full a b Hb); auto.
+  destruct Z.div_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).
-
-Definition Z_mod_neg : forall a b:Z, b < 0 -> b < a mod b <= 0
- := Zmod_neg_bound.
+Lemma Z_mod_lt a b : b > 0 -> 0 <= a mod b < b.
+Proof (fun Hb => Z.mod_pos_bound a b (Zgt_lt _ _ Hb)).
 
-Notation Z_div_mod_eq_full := Z_div_mod_eq_full (only parsing).
+Lemma Z_mod_neg a b : b < 0 -> b < a mod b <= 0.
+Proof (Z.mod_neg_bound a b).
 
-Lemma Z_div_mod_eq : forall a b:Z, b > 0 -> a = b*(a/b) + (a mod b).
+Lemma Z_div_mod_eq a b : b > 0 -> a = b*(a/b) + (a mod b).
 Proof.
-  intros; apply Z_div_mod_eq_full; auto with zarith.
+  intros Hb; apply Z.div_mod; auto with zarith.
 Qed.
 
-Lemma Zmod_eq_full : forall a b:Z, b<>0 -> a mod b = a - (a/b)*b.
-Proof. intros. rewrite Zmult_comm. now apply Z.mod_eq. Qed.
+Lemma Zmod_eq_full a b : b<>0 -> a mod b = a - (a/b)*b.
+Proof. intros. rewrite Z.mul_comm. now apply Z.mod_eq. Qed.
 
-Lemma Zmod_eq : forall a b:Z, b>0 -> a mod b = a - (a/b)*b.
+Lemma Zmod_eq a b : b>0 -> a mod b = a - (a/b)*b.
 Proof. intros. apply Zmod_eq_full. now destruct b. Qed.
 
 (** Existence theorem *)
@@ -111,7 +120,7 @@ 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).
+  exists (Z.div_eucl a b).
   exact (Z_div_mod a b Hb).
 Qed.
 
@@ -120,34 +129,27 @@ Implicit Arguments Zdiv_eucl_exist.
 
 (** Uniqueness theorems *)
 
-Theorem Zdiv_mod_unique :
- forall b q1 q2 r1 r2:Z,
-  0 <= r1 < Zabs b -> 0 <= r2 < Zabs b ->
+Theorem Zdiv_mod_unique b q1 q2 r1 r2 :
+  0 <= r1 < Z.abs b -> 0 <= r2 < Z.abs b ->
   b*q1+r1 = b*q2+r2 -> q1=q2 /\ r1=r2.
 Proof.
-intros b q1 q2 r1 r2 Hr1 Hr2 H.
-destruct (Z_eq_dec q1 q2) as [Hq|Hq].
+intros Hr1 Hr2 H. rewrite <- (Z.abs_sgn b), <- !Z.mul_assoc in H.
+destruct (Z.div_mod_unique (Z.abs b) (Z.sgn b * q1) (Z.sgn b * q2) r1 r2); auto.
 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 *.
+apply Z.mul_cancel_l with (Z.sgn b); trivial.
+rewrite Z.sgn_null_iff, <- Z.abs_0_iff. destruct Hr1; Z.order.
 Qed.
 
 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. exact Z.div_mod_unique. Qed.
+Proof Z.div_mod_unique.
 
 Theorem Zdiv_unique_full:
  forall a b q r, Remainder r b ->
    a = b*q + r -> q = a/b.
-Proof. exact Z.div_unique. Qed.
+Proof Z.div_unique.
 
 Theorem Zdiv_unique:
  forall a b q r, 0 <= r < b ->
@@ -157,7 +159,7 @@ Proof. intros; eapply Zdiv_unique_full; eauto. Qed.
 Theorem Zmod_unique_full:
  forall a b q r, Remainder r b ->
   a = b*q + r ->  r = a mod b.
-Proof. exact Z.mod_unique. Qed.
+Proof Z.mod_unique.
 
 Theorem Zmod_unique:
  forall a b q r, 0 <= r < b ->
@@ -187,7 +189,7 @@ Proof.
 Qed.
 
 Ltac zero_or_not a :=
-  destruct (Z_eq_dec a 0);
+  destruct (Z.eq_dec a 0);
   [subst; rewrite ?Zmod_0_l, ?Zdiv_0_l, ?Zmod_0_r, ?Zdiv_0_r;
    auto with zarith|].
 
@@ -201,13 +203,13 @@ 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. exact Z.div_1_l. Qed.
+Proof Z.div_1_l.
 
 Lemma Zmod_1_l: forall a, 1 < a ->  1 mod a = 1.
-Proof. exact Z.mod_1_l. Qed.
+Proof Z.mod_1_l.
 
 Lemma Z_div_same_full : forall a:Z, a<>0 -> a/a = 1.
-Proof. exact Z.div_same. Qed.
+Proof Z.div_same.
 
 Lemma Z_mod_same_full : forall a, a mod a = 0.
 Proof. intros. zero_or_not a. apply Z.mod_same; auto. Qed.
@@ -216,7 +218,7 @@ Lemma Z_mod_mult : forall a b, (a*b) mod b = 0.
 Proof. intros. zero_or_not b. apply Z.mod_mul. auto. Qed.
 
 Lemma Z_div_mult_full : forall a b:Z, b <> 0 -> (a*b)/b = a.
-Proof. exact Z.div_mul. Qed.
+Proof Z.div_mul.
 
 (** * Order results about Zmod and Zdiv *)
 
@@ -239,12 +241,12 @@ Proof. intros. apply Z.div_lt; auto with zarith. Qed.
 (** 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. exact Z.div_small. Qed.
+Proof Z.div_small.
 
 (** Same situation, in term of modulo: *)
 
 Theorem Zmod_small: forall a n, 0 <= a < n -> a mod n = a.
-Proof. exact Z.mod_small. Qed.
+Proof Z.mod_small.
 
 (** [Zge] is compatible with a positive division. *)
 
@@ -281,15 +283,15 @@ Proof. intros. apply Z.mod_le; auto. Qed.
 
 Theorem Zdiv_lt_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_lt_upper_bound. Qed.
+Proof. intros a b q; rewrite Z.mul_comm; apply Z.div_lt_upper_bound. Qed.
 
 Theorem Zdiv_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.
+Proof. intros a b q; rewrite Z.mul_comm; apply Z.div_le_upper_bound. Qed.
 
 Theorem Zdiv_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.
+Proof. intros a b q; rewrite Z.mul_comm; apply Z.div_le_lower_bound. Qed.
 
 (** A division of respect opposite monotonicity for the divisor *)
 
@@ -298,11 +300,11 @@ Lemma Zdiv_le_compat_l: forall p q r, 0 <= p -> 0 < q < r ->
 Proof. intros; apply Z.div_le_compat_l; auto with zarith. Qed.
 
 Theorem Zdiv_sgn: forall a b,
-  0 <= Zsgn (a/b) * Zsgn a * Zsgn b.
+  0 <= Z.sgn (a/b) * Z.sgn a * Z.sgn 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 *.
+  generalize (Z.div_pos (Zpos a) (Zpos b)); unfold Z.div, Z.div_eucl;
+  destruct Z.pos_div_eucl as (q,r); destruct r; omega with *.
 Qed.
 
 (** * Relations between usual operations and Zmod and Zdiv *)
@@ -311,10 +313,10 @@ Lemma Z_mod_plus_full : forall a b c:Z, (a + b * c) mod c = a mod c.
 Proof. intros. zero_or_not c. apply Z.mod_add; auto. Qed.
 
 Lemma Z_div_plus_full : forall a b c:Z, c <> 0 -> (a + b * c) / c = a / c + b.
-Proof. exact Z.div_add. Qed.
+Proof Z.div_add.
 
 Theorem Z_div_plus_full_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b.
-Proof. exact Z.div_add_l. Qed.
+Proof Z.div_add_l.
 
 (** [Zopp] and [Zdiv], [Zmod].
     Due to the choice of convention for our Euclidean division,
@@ -500,7 +502,7 @@ End EqualityModulo.
 Lemma Zdiv_Zdiv : forall a b c, 0<=b -> 0<=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 with zarith.
+ rewrite Z.mul_comm. apply Z.div_div; auto with zarith.
 Qed.
 
 (** Unfortunately, the previous result isn't always true on negative numbers.
@@ -524,27 +526,25 @@ Qed.
 
 (** Particular case : dividing by 2 is related with parity *)
 
-Lemma Zdiv2_div : forall a, Zdiv2 a = a/2.
-Proof.
- apply Z.div2_div.
-Qed.
+Lemma Zdiv2_div : forall a, Z.div2 a = a/2.
+Proof Z.div2_div.
 
-Lemma Zmod_odd : forall a, a mod 2 = if Zodd_bool a then 1 else 0.
+Lemma Zmod_odd : forall a, a mod 2 = if Z.odd a then 1 else 0.
 Proof.
  intros a. now rewrite <- Z.bit0_odd, <- Z.bit0_mod.
 Qed.
 
-Lemma Zmod_even : forall a, a mod 2 = if Zeven_bool a then 0 else 1.
+Lemma Zmod_even : forall a, a mod 2 = if Z.even a then 0 else 1.
 Proof.
  intros a. rewrite Zmod_odd, Zodd_even_bool. now destruct Zeven_bool.
 Qed.
 
-Lemma Zodd_mod : forall a, Zodd_bool a = Zeq_bool (a mod 2) 1.
+Lemma Zodd_mod : forall a, Z.odd a = Zeq_bool (a mod 2) 1.
 Proof.
  intros a. rewrite Zmod_odd. now destruct Zodd_bool.
 Qed.
 
-Lemma Zeven_mod : forall a, Zeven_bool a = Zeq_bool (a mod 2) 0.
+Lemma Zeven_mod : forall a, Z.even a = Zeq_bool (a mod 2) 0.
 Proof.
  intros a. rewrite Zmod_even. now destruct Zeven_bool.
 Qed.
@@ -630,7 +630,7 @@ Definition Zmod' a b :=
   end.
 
 
-Theorem Zmod_POS_correct a b : Zmod_POS a b = snd (Zdiv_eucl_POS a b).
+Theorem Zmod_POS_correct a b : Zmod_POS a b = snd (Z.pos_div_eucl a b).
 Proof.
   induction a as [a IH|a IH| ]; simpl; rewrite ?IH.
   destruct (Z.pos_div_eucl a b) as (p,q); simpl;
@@ -640,18 +640,18 @@ Proof.
   case Z.leb_spec; trivial.
 Qed.
 
-Theorem Zmod'_correct: forall a b, Zmod' a b = Zmod a b.
+Theorem Zmod'_correct: forall a b, Zmod' a b = a mod b.
 Proof.
-  intros a b; unfold Zmod; case a; simpl; auto.
+  intros a b; unfold Z.modulo; 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.
+  case (Z.pos_div_eucl 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.
+  case (Z.pos_div_eucl 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.
+  case (Z.pos_div_eucl p (Zpos p1)); auto.
 Qed.
 
 
@@ -663,12 +663,12 @@ 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}.
+      {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs 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 ].
+  rewrite Z.abs_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.
@@ -676,7 +676,7 @@ Proof.
   elim Hqr; intros.
   split.
   rewrite <- Zmult_opp_comm; assumption.
-  rewrite Zabs_non_eq; [ assumption | omega ].
+  rewrite Z.abs_neq; [ assumption | omega ].
 Qed.
 
 Implicit Arguments Zdiv_eucl_extended.
@@ -686,10 +686,10 @@ Implicit Arguments Zdiv_eucl_extended.
 Require Import NPeano.
 
 Lemma div_Zdiv (n m: nat): m <> O ->
-  Z_of_nat (n / m) = Z_of_nat n / Z_of_nat m.
+  Z.of_nat (n / m) = Z.of_nat n / Z.of_nat m.
 Proof.
  intros.
- apply (Zdiv_unique _ _ _ (Z_of_nat (n mod m)%nat)).
+ apply (Zdiv_unique _ _ _ (Z.of_nat (n mod m))).
   split. auto with zarith.
   now apply inj_lt, Nat.mod_upper_bound.
  rewrite <- inj_mult, <- inj_plus.
@@ -697,19 +697,12 @@ Proof.
 Qed.
 
 Lemma mod_Zmod (n m: nat): m <> O ->
-  Z_of_nat (n mod m)%nat = (Z_of_nat n mod Z_of_nat m).
+  Z.of_nat (n mod m) = (Z.of_nat n) mod (Z.of_nat m).
 Proof.
  intros.
- apply (Zmod_unique _ _ (Z_of_nat n / Z_of_nat m)).
+ apply (Zmod_unique _ _ (Z.of_nat n / Z.of_nat m)).
   split. auto with zarith.
   now apply inj_lt, Nat.mod_upper_bound.
  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
deleted file mode 100644
index 0f375e144..000000000
--- a/theories/ZArith/Zdiv_def.v
+++ /dev/null
@@ -1,37 +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 BinInt Zbool Zcompare Zorder Zabs Znat.
-Local Open Scope Z_scope.
-
-Notation Zdiv_eucl_POS := Z.pos_div_eucl (only parsing).
-Notation Zdiv_eucl := Z.div_eucl (only parsing).
-Notation Zdiv := Z.div (only parsing).
-Notation Zmod := Z.modulo (only parsing).
-Notation Zquotrem := Z.quotrem (only parsing).
-Notation Zquot := Z.quot (only parsing).
-Notation Zrem := Z.rem (only parsing).
-
-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. generalize (Z.pos_div_eucl_eq a b Hb).
- destruct Z.pos_div_eucl. now rewrite Z.mul_comm.
-Qed.
-
-Notation Zdiv_eucl_eq := Z.div_eucl_eq (only parsing).
-Notation Z_div_mod_eq_full := Z.div_mod (only parsing).
-Notation Zmod_POS_bound := Z.pos_div_eucl_bound (only parsing).
-Notation Zmod_pos_bound := Z.mod_pos_bound (only parsing).
-Notation Zmod_neg_bound := Z.mod_neg_bound (only parsing).
-
-Notation Zquotrem_eq := Z.quotrem_eq (only parsing).
-Notation Z_quot_rem_eq := Z.quot_rem' (only parsing).
-Notation Zrem_bound := Z.rem_bound_pos (only parsing).
-Notation Zrem_opp_l := Z.rem_opp_l' (only parsing).
-Notation Zrem_opp_r := Z.rem_opp_r' (only parsing).
diff --git a/theories/ZArith/Zeuclid.v b/theories/ZArith/Zeuclid.v
index cd46ea36b..f1b597491 100644
--- a/theories/ZArith/Zeuclid.v
+++ b/theories/ZArith/Zeuclid.v
@@ -6,46 +6,44 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Morphisms BinInt Zdiv_def ZDivEucl.
+Require Import Morphisms BinInt 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.
+    For other conventions, see [Z.div] and [Z.quot] in file [BinIntDef].
     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)).
+ Definition modulo a b := Z.modulo a (Z.abs b).
+ Definition div a b := (Z.sgn b) * (Z.div a (Z.abs 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.
+ Theorem div_mod 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.
+  intros Hb. unfold div, modulo.
+  rewrite Z.mul_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.
+ Lemma mod_always_pos a b : b<>0 -> 0 <= modulo a b < Z.abs b.
  Proof.
-  intros a b Hb. unfold modulo.
+  intros 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.
+ Lemma mod_bound_pos 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.
+  intros _ Hb. rewrite <- (Z.abs_eq b) at 3 by Z.order.
   apply mod_always_pos. Z.order.
  Qed.
 
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index 6b6ad7423..9a95669f5 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -6,13 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Nnat ZArith_base ROmega ZArithRing Zdiv_def Zdiv Morphisms.
+Require Import Nnat ZArith_base ROmega ZArithRing Zdiv Morphisms.
 
 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].
+  Definition of this division can be found in file [BinIntDef].
 
   This division and the one defined in Zdiv agree only on positive
   numbers. Otherwise, Zdiv performs Round-Toward-Bottom (a.k.a Floor).
@@ -29,15 +29,15 @@ Lemma Ndiv_Zquot : forall a b:N,
 Proof.
   intros.
   destruct a; destruct b; simpl; auto.
-  unfold N.div, Zquot; simpl. destruct N.pos_div_eucl; auto.
+  unfold N.div, Z.quot; simpl. destruct N.pos_div_eucl; auto.
 Qed.
 
 Lemma Nmod_Zrem : forall a b:N,
-  Z_of_N (a mod b) = Zrem (Z_of_N a) (Z_of_N b).
+  Z.of_N (a mod b) = Z.rem (Z.of_N a) (Z.of_N b).
 Proof.
   intros.
   destruct a; destruct b; simpl; auto.
-  unfold N.modulo, Zrem; simpl; destruct N.pos_div_eucl; auto.
+  unfold N.modulo, Z.rem; simpl; destruct N.pos_div_eucl; auto.
 Qed.
 
 (** * Characterization of this euclidean division. *)
@@ -46,13 +46,13 @@ Qed.
    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).
+Notation Z_quot_rem_eq := Z.quot_rem' (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 (Zrem a b) < Zabs b.
+  Z.abs (Z.rem a b) < Z.abs b.
 Proof.
   apply Z.rem_bound_abs.
 Qed.
@@ -61,35 +61,27 @@ Qed.
    nullity of [a], a general result is to be stated in the following form:
 *)
 
-Theorem Zrem_sgn : forall a b:Z,
-  0 <= Zsgn (Zrem a b) * Zsgn a.
+Theorem Zrem_sgn a b : 0 <= Z.sgn (Z.rem a b) * Z.sgn a.
 Proof.
   destruct b as [ |b|b]; destruct a as [ |a|a]; simpl; auto with zarith;
-  unfold Zrem, Zquotrem; destruct N.pos_div_eucl;
+  unfold Z.rem, Z.quotrem; destruct N.pos_div_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.
+Theorem Zrem_sgn2 a b : 0 <= (Z.rem a b) * a.
 Proof.
- destruct z; simpl; intuition auto with zarith.
-Qed.
-
-Theorem Zrem_sgn2 : forall a b:Z,
-  0 <= (Zrem a b) * a.
-Proof.
-  intros; rewrite <-Zsgn_pos_iff, Zsgn_Zmult; apply Zrem_sgn.
+  rewrite <-Z.sgn_nonneg, Z.sgn_mul; 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 <= Zrem a b < Zabs b.
+Theorem Zrem_lt_pos a b : 0<=a -> b<>0 -> 0 <= Z.rem a b < Z.abs b.
 Proof.
   intros.
-  assert (0 <= Zrem a b).
+  assert (0 <= Z.rem a b).
    generalize (Zrem_sgn a b).
    destruct (Zle_lt_or_eq 0 a H).
    rewrite <- Zsgn_pos in H1; rewrite H1. romega with *.
@@ -97,11 +89,10 @@ Proof.
   generalize (Zrem_lt a b H0); romega with *.
 Qed.
 
-Theorem Zrem_lt_neg : forall a b:Z, a<=0 -> b<>0 ->
-  -Zabs b < Zrem a b <= 0.
+Theorem Zrem_lt_neg a b : a<=0 -> b<>0 -> -Z.abs b < Z.rem a b <= 0.
 Proof.
   intros.
-  assert (Zrem a b <= 0).
+  assert (Z.rem a b <= 0).
    generalize (Zrem_sgn a b).
    destruct (Zle_lt_or_eq a 0 H).
    rewrite <- Zsgn_neg in H1; rewrite H1; romega with *.
@@ -109,22 +100,22 @@ Proof.
   generalize (Zrem_lt a b H0); romega with *.
 Qed.
 
-Theorem Zrem_lt_pos_pos : forall a b:Z, 0<=a -> 0<b -> 0 <= Zrem a b < b.
+Theorem Zrem_lt_pos_pos a b : 0<=a -> 0<b -> 0 <= Z.rem a 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 <= Zrem a b < -b.
+Theorem Zrem_lt_pos_neg a b : 0<=a -> b<0 -> 0 <= Z.rem a 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 < Zrem a b <= 0.
+Theorem Zrem_lt_neg_pos a b : a<=0 -> 0<b -> -b < Z.rem a 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 < Zrem a b <= 0.
+Theorem Zrem_lt_neg_neg a b : a<=0 -> b<0 -> b < Z.rem a b <= 0.
 Proof.
   intros; generalize (Zrem_lt_neg a b); romega with *.
 Qed.
@@ -133,49 +124,49 @@ Qed.
 
 (* The precise equalities that are invalid with "historic" Zdiv. *)
 
-Theorem Zquot_opp_l : forall a b:Z, (-a)÷b = -(a÷b).
+Theorem Zquot_opp_l a b : (-a)÷b = -(a÷b).
 Proof.
  destruct a; destruct b; simpl; auto;
-  unfold Zquot, Zquotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
+  unfold Z.quot, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
 Qed.
 
-Theorem Zquot_opp_r : forall a b:Z, a÷(-b) = -(a÷b).
+Theorem Zquot_opp_r a b : a÷(-b) = -(a÷b).
 Proof.
  destruct a; destruct b; simpl; auto;
-  unfold Zquot, Zquotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
+  unfold Z.quot, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
 Qed.
 
-Theorem Zrem_opp_l : forall a b:Z, Zrem (-a) b = -(Zrem a b).
+Theorem Zrem_opp_l a b : Z.rem (-a) b = -(Z.rem a b).
 Proof.
  destruct a; destruct b; simpl; auto;
-  unfold Zrem, Zquotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
+  unfold Z.rem, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
 Qed.
 
-Theorem Zrem_opp_r : forall a b:Z, Zrem a (-b) = Zrem a b.
+Theorem Zrem_opp_r a b : Z.rem a (-b) = Z.rem a b.
 Proof.
  destruct a; destruct b; simpl; auto;
-  unfold Zrem, Zquotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
+  unfold Z.rem, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
 Qed.
 
-Theorem Zquot_opp_opp : forall a b:Z, (-a)÷(-b) = a÷b.
+Theorem Zquot_opp_opp a b : (-a)÷(-b) = a÷b.
 Proof.
  destruct a; destruct b; simpl; auto;
-  unfold Zquot, Zquotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
+  unfold Z.quot, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
 Qed.
 
-Theorem Zrem_opp_opp : forall a b:Z, Zrem (-a) (-b) = -(Zrem a b).
+Theorem Zrem_opp_opp a b : Z.rem (-a) (-b) = -(Z.rem a b).
 Proof.
  destruct a; destruct b; simpl; auto;
-  unfold Zrem, Zquotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
+  unfold Z.rem, Z.quotrem; destruct N.pos_div_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).
+  (0 <= a /\ 0 <= r < Z.abs b) \/ (a <= 0 /\ -Z.abs b < r <= 0).
 
 Definition Remainder_alt a b r :=
-  Zabs r < Zabs b /\ 0 <= r * a.
+  Z.abs r < Z.abs b /\ 0 <= r * a.
 
 Lemma Remainder_equiv : forall a b r,
  Remainder a b r <-> Remainder_alt a b r.
@@ -185,13 +176,13 @@ Proof.
   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 *.
+  assert (0 <= Z.sgn r * Z.sgn a) by (rewrite <-Z.sgn_mul, Z.sgn_nonneg; auto).
+  destruct r; simpl Z.sgn 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 = Zrem a b.
+   a = b*q + r -> q = a÷b /\ r = Z.rem a b.
 Proof.
   destruct 1 as [(H,H0)|(H,H0)]; intros.
   apply Zdiv_mod_unique with b; auto.
@@ -201,7 +192,7 @@ Proof.
 
   rewrite <- (Zopp_involutive a).
   rewrite Zquot_opp_l, Zrem_opp_l.
-  generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Zrem (-a) b)).
+  generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Z.rem (-a) b)).
   generalize (Zrem_lt_pos (-a) b).
   rewrite <-Z_quot_rem_eq, <-Zopp_mult_distr_r, <-Zopp_plus_distr, <-H1.
   romega with *.
@@ -221,24 +212,24 @@ Proof. exact Z.quot_unique. Qed.
 
 Theorem Zrem_unique_full:
  forall a b q r, Remainder a b r ->
-  a = b*q + r -> r = Zrem a b.
+  a = b*q + r -> r = Z.rem a 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 = Zrem a b.
+   a = b*q + r -> r = Z.rem a b.
 Proof. exact Z.rem_unique. Qed.
 
 (** * Basic values of divisions and modulo. *)
 
-Lemma Zrem_0_l: forall a, Zrem 0 a = 0.
+Lemma Zrem_0_l: forall a, Z.rem 0 a = 0.
 Proof.
   destruct a; simpl; auto.
 Qed.
 
-Lemma Zrem_0_r: forall a, Zrem a 0 = a.
+Lemma Zrem_0_r: forall a, Z.rem a 0 = a.
 Proof.
   destruct a; simpl; auto.
 Qed.
@@ -253,7 +244,7 @@ Proof.
   destruct a; simpl; auto.
 Qed.
 
-Lemma Zrem_1_r: forall a, Zrem a 1 = 0.
+Lemma Zrem_1_r: forall a, Z.rem a 1 = 0.
 Proof. exact Z.rem_1_r. Qed.
 
 Lemma Zquot_1_r: forall a, a÷1 = a.
@@ -265,21 +256,21 @@ Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Zquot_1_r Zrem_1_r
 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 -> Zrem 1 a = 1.
+Lemma Zrem_1_l: forall a, 1 < a -> Z.rem 1 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);
+  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, Zrem a a = 0.
+Lemma Z_rem_same : forall a, Z.rem a a = 0.
 Proof. intros. zero_or_not a. apply Z.rem_same; auto. Qed.
 
-Lemma Z_rem_mult : forall a b, Zrem (a*b) b = 0.
+Lemma Z_rem_mult : forall a b, Z.rem (a*b) 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.
@@ -305,7 +296,7 @@ Proof. exact Z.quot_small. Qed.
 
 (** Same situation, in term of modulo: *)
 
-Theorem Zrem_small: forall a n, 0 <= a < n -> Zrem a n = a.
+Theorem Zrem_small: forall a n, 0 <= a < n -> Z.rem a n = a.
 Proof. exact Z.rem_small. Qed.
 
 (** [Zge] is compatible with a positive division. *)
@@ -324,12 +315,12 @@ 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) <-> Zrem a b = 0.
+Lemma Z_quot_exact_full : forall a b:Z, a = b*(a÷b) <-> Z.rem a 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 -> Zrem a b <= a.
+Theorem Zrem_le: forall a b, 0 <= a -> 0 <= b -> Z.rem a b <= a.
 Proof. intros. zero_or_not b. apply Z.rem_le; auto with zarith. Qed.
 
 (** Some additionnal inequalities about Zdiv. *)
@@ -347,10 +338,10 @@ Theorem Zquot_le_lower_bound:
 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.
+  0 <= Z.sgn (a÷b) * Z.sgn a * Z.sgn b.
 Proof.
   destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith;
-  unfold Zquot; simpl; destruct N.pos_div_eucl; simpl; destruct n; simpl; auto with zarith.
+  unfold Z.quot; simpl; destruct N.pos_div_eucl; simpl; destruct n; simpl; auto with zarith.
 Qed.
 
 (** * Relations between usual operations and Zmod and Zdiv *)
@@ -361,7 +352,7 @@ Qed.
 
 Lemma Z_rem_plus : forall a b c:Z,
  0 <= (a+b*c) * a ->
- Zrem (a + b * c) c = Zrem a c.
+ Z.rem (a + b * c) c = Z.rem a c.
 Proof. intros. zero_or_not c. apply Z.rem_add; auto with zarith. Qed.
 
 Lemma Z_quot_plus : forall a b c:Z,
@@ -388,14 +379,14 @@ Proof.
 Qed.
 
 Lemma Zmult_rem_distr_l: forall a b c,
-  Zrem (c*a) (c*b) = c * (Zrem a b).
+  Z.rem (c*a) (c*b) = c * (Z.rem a 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,
-  Zrem (a*c) (b*c) = (Zrem a b) * c.
+  Z.rem (a*c) (b*c) = (Z.rem a 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.
@@ -403,11 +394,11 @@ Qed.
 
 (** Operations modulo. *)
 
-Theorem Zrem_rem: forall a n, Zrem (Zrem a n) n = Zrem a n.
+Theorem Zrem_rem: forall a n, Z.rem (Z.rem a n) n = Z.rem a n.
 Proof. intros. zero_or_not n. apply Z.rem_rem; auto. Qed.
 
 Theorem Zmult_rem: forall a b n,
- Zrem (a * b) n = Zrem (Zrem a n * Zrem b n) n.
+ Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n.
 Proof. intros. zero_or_not n. apply Z.mul_rem; auto. Qed.
 
 (** addition and modulo
@@ -420,26 +411,26 @@ Proof. intros. zero_or_not n. apply Z.mul_rem; auto. Qed.
 
 Theorem Zplus_rem: forall a b n,
  0 <= a * b ->
- Zrem (a + b) n = Zrem (Zrem a n + Zrem b n) n.
+ Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) 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 ->
- Zrem (Zrem a n + b) n = Zrem (a + b) n.
+ Z.rem (Z.rem a n + b) n = Z.rem (a + b) 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 ->
- Zrem (b + Zrem a n) n = Zrem (b + a) n.
+ Z.rem (b + Z.rem a n) n = Z.rem (b + a) 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, Zrem (Zrem a n * b) n = Zrem (a * b) n.
+Lemma Zmult_rem_idemp_l: forall a b n, Z.rem (Z.rem a n * b) n = Z.rem (a * b) n.
 Proof. intros. zero_or_not n. apply Z.mul_rem_idemp_l; auto. Qed.
 
-Lemma Zmult_rem_idemp_r: forall a b n, Zrem (b * Zrem a n) n = Zrem (b * a) n.
+Lemma Zmult_rem_idemp_r: forall a b n, Z.rem (b * Z.rem a n) n = Z.rem (b * a) 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. *)
@@ -456,10 +447,10 @@ 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) *)
+(** Z.rem is related to divisibility (see more in Znumtheory) *)
 
 Lemma Zrem_divides : forall a b,
- Zrem a b = 0 <-> exists c, a = b*c.
+ Z.rem a b = 0 <-> exists c, a = b*c.
 Proof.
  intros. zero_or_not b. firstorder.
  rewrite Z.rem_divide; trivial.
@@ -469,7 +460,7 @@ Qed.
 (** Particular case : dividing by 2 is related with parity *)
 
 Lemma Zquot2_odd_remainder : forall a,
- Remainder a 2 (if Zodd_bool a then Zsgn a else 0).
+ Remainder a 2 (if Z.odd a then Z.sgn a else 0).
 Proof.
  intros [ |p|p]. simpl.
  left. simpl. auto with zarith.
@@ -477,15 +468,9 @@ Proof.
  right. destruct p; simpl; split; now auto with zarith.
 Qed.
 
-Lemma Zquot2_quot : forall a, Zquot2 a = a÷2.
-Proof.
- intros.
- apply Zquot_unique_full with (if Zodd_bool a then Zsgn a else 0).
- apply Zquot2_odd_remainder.
- apply Zquot2_odd_eqn.
-Qed.
+Notation Zquot2_quot := Zquot2_quot (only parsing).
 
-Lemma Zrem_odd : forall a, Zrem a 2 = if Zodd_bool a then Zsgn a else 0.
+Lemma Zrem_odd : forall a, Z.rem a 2 = if Z.odd a then Z.sgn a else 0.
 Proof.
  intros. symmetry.
  apply Zrem_unique_full with (Zquot2 a).
@@ -493,18 +478,18 @@ Proof.
  apply Zquot2_odd_eqn.
 Qed.
 
-Lemma Zrem_even : forall a, Zrem a 2 = if Zeven_bool a then 0 else Zsgn a.
+Lemma Zrem_even : forall a, Z.rem a 2 = if Z.even a then 0 else Z.sgn a.
 Proof.
  intros a. rewrite Zrem_odd, Zodd_even_bool. now destruct Zeven_bool.
 Qed.
 
-Lemma Zeven_rem : forall a, Zeven_bool a = Zeq_bool (Zrem a 2) 0.
+Lemma Zeven_rem : forall a, Z.even a = Zeq_bool (Z.rem a 2) 0.
 Proof.
  intros a. rewrite Zrem_even.
  destruct a as [ |p|p]; trivial; now destruct p.
 Qed.
 
-Lemma Zodd_rem : forall a, Zodd_bool a = negb (Zeq_bool (Zrem a 2) 0).
+Lemma Zodd_rem : forall a, Z.odd a = negb (Zeq_bool (Z.rem a 2) 0).
 Proof.
  intros a. rewrite Zrem_odd.
  destruct a as [ |p|p]; trivial; now destruct p.
@@ -515,7 +500,7 @@ Qed.
 (** They agree at least on positive numbers: *)
 
 Theorem Zquotrem_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b ->
-  a÷b = a/b /\ Zrem a b = a mod b.
+  a÷b = a/b /\ Z.rem a b = a mod b.
 Proof.
   intros.
   apply Zdiv_mod_unique with b.
@@ -535,7 +520,7 @@ Proof.
 Qed.
 
 Theorem Zrem_Zmod_pos : forall a b, 0 <= a -> 0 < b ->
-  Zrem a b = a mod b.
+  Z.rem a b = a mod b.
 Proof.
  intros a b Ha Hb; generalize (Zquotrem_Zdiv_eucl_pos a b Ha Hb);
  intuition.
@@ -544,7 +529,7 @@ Qed.
 (** Modulos are null at the same places *)
 
 Theorem Zrem_Zmod_zero : forall a b, b<>0 ->
- (Zrem a b = 0 <-> a mod b = 0).
+ (Z.rem a b = 0 <-> a mod b = 0).
 Proof.
  intros.
  rewrite Zrem_divides, Zmod_divides; intuition.
diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget
index 7592d2fae..10c2d71b2 100644
--- a/theories/ZArith/vo.itarget
+++ b/theories/ZArith/vo.itarget
@@ -22,7 +22,6 @@ Zmin.vo
 Zmisc.vo
 Znat.vo
 Znumtheory.vo
-Zdiv_def.vo
 Zquot.vo
 Zorder.vo
 Zpow_def.vo