Clean-up of Znumtheory, deletion of Zgcd_def

 In particular, we merge the old Zdivide (used to be an ad-hoc
 inductive predicate) and the new Z.divide (based on exists).
 Notations allow to do that (almost) transparently, the only
 impact is that the name picked by the system will not be "q"
 anymore when destructing a Z.divide. Some fragile scripts
 may have to be fixed.

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

9 files changed, 161 insertions, 374 deletions

diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index 2d9eb395a..3bdbca44a 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -465,8 +465,8 @@ Section ZModulo.
  Proof.
  intros.
  generalize (Zgcd_is_gcd a b); inversion_clear 1.
- destruct H2; destruct H3; clear H4.
- assert (H3:=Zgcd_is_pos a b).
+ destruct H2 as (q,H2); destruct H3 as (q',H3); clear H4.
+ assert (H4:=Zgcd_is_pos a b).
  destruct (Z_eq_dec (Zgcd a b) 0).
  rewrite e; generalize (Zmax_spec a b); omega.
  assert (0 <= q).
@@ -477,7 +477,7 @@ Section ZModulo.
  generalize (Zmax_spec 0 b) (Zabs_spec b); omega.
 
  apply Zle_trans with a.
- rewrite H1 at 2.
+ rewrite H2 at 2.
  rewrite <- (Zmult_1_l (Zgcd a b)) at 1.
  apply Zmult_le_compat; auto with zarith.
  generalize (Zmax_spec a b); omega.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 44dd2c593..6facd3c3a 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -421,22 +421,22 @@ Qed.
 
 Lemma gcd_divide_l : forall n m, (gcd n m | n).
 Proof.
- intros n m. apply spec_divide. zify. apply Zgcd_divide_l.
+ intros n m. apply spec_divide. zify. apply Z.gcd_divide_l.
 Qed.
 
 Lemma gcd_divide_r : forall n m, (gcd n m | m).
 Proof.
- intros n m. apply spec_divide. zify. apply Zgcd_divide_r.
+ intros n m. apply spec_divide. zify. apply Z.gcd_divide_r.
 Qed.
 
 Lemma gcd_greatest : forall n m p, (p|n) -> (p|m) -> (p|gcd n m).
 Proof.
- intros n m p. rewrite !spec_divide. zify. apply Zgcd_greatest.
+ intros n m p. rewrite !spec_divide. zify. apply Z.gcd_greatest.
 Qed.
 
 Lemma gcd_nonneg : forall n m, 0 <= gcd n m.
 Proof.
- intros. zify. apply Zgcd_nonneg.
+ intros. zify. apply Z.gcd_nonneg.
 Qed.
 
 (** Bitwise operations *)
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 33181e32a..57277b489 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -347,22 +347,22 @@ Qed.
 
 Lemma gcd_divide_l : forall n m, (gcd n m | n).
 Proof.
- intros n m. apply spec_divide. zify. apply Zgcd_divide_l.
+ intros n m. apply spec_divide. zify. apply Z.gcd_divide_l.
 Qed.
 
 Lemma gcd_divide_r : forall n m, (gcd n m | m).
 Proof.
- intros n m. apply spec_divide. zify. apply Zgcd_divide_r.
+ intros n m. apply spec_divide. zify. apply Z.gcd_divide_r.
 Qed.
 
 Lemma gcd_greatest : forall n m p, (p|n) -> (p|m) -> (p|gcd n m).
 Proof.
- intros n m p. rewrite !spec_divide. zify. apply Zgcd_greatest.
+ intros n m p. rewrite !spec_divide. zify. apply Z.gcd_greatest.
 Qed.
 
 Lemma gcd_nonneg : forall n m, 0 <= gcd n m.
 Proof.
- intros. zify. apply Zgcd_nonneg.
+ intros. zify. apply Z.gcd_nonneg.
 Qed.
 
 (** Bitwise operations *)
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 4888ce4b1..e39eca0cb 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -9,7 +9,7 @@
 (** Normalisation functions for rational numbers. *)
 
 Require Export QArith_base.
-Require Import Zgcd_def Znumtheory.
+Require Import Znumtheory.
 
 (** First, a function that (tries to) build a positive back from a Z. *)
 
@@ -83,14 +83,13 @@ Proof.
   exists bb; auto with zarith.
   intros.
   inversion Hg1.
-  destruct (H6 (g*x)).
+  destruct (H6 (g*x)) as (x',Hx).
   rewrite Hg3.
   destruct H2 as (xa,Hxa); exists xa; rewrite Hxa; ring.
   rewrite Hg4.
   destruct H3 as (xb,Hxb); exists xb; rewrite Hxb; ring.
-  exists q.
-  apply Zmult_reg_l with g; auto.
-  pattern g at 1; rewrite H7; ring.
+  exists x'.
+  apply Zmult_reg_l with g; auto. rewrite Hx at 1; ring.
   (* /rel_prime *)
   unfold rel_prime in |- *.
   (* rel_prime *)
@@ -99,14 +98,13 @@ Proof.
   exists dd; auto with zarith.
   intros.
   inversion Hg'1.
-  destruct (H6 (g'*x)).
+  destruct (H6 (g'*x)) as (x',Hx).
   rewrite Hg'3.
   destruct H2 as (xc,Hxc); exists xc; rewrite Hxc; ring.
   rewrite Hg'4.
   destruct H3 as (xd,Hxd); exists xd; rewrite Hxd; ring.
-  exists q.
-  apply Zmult_reg_l with g'; auto.
-  pattern g' at 1; rewrite H7; ring.
+  exists x'.
+  apply Zmult_reg_l with g'; auto. rewrite Hx at 1; ring.
     (* /rel_prime *)
   assert (0<bb); [|auto with zarith].
   apply Zmult_gt_0_lt_0_reg_r with g.
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index e532e4ad9..a935c7dac 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 Zgcd_def Zdiv_def Zdigits_def.
+ Zpow_def Zsqrt_def Zlog_def Zdiv_def Zdigits_def.
 
 (** Extra modules using [Omega] or [Ring]. *)
 
diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v
index bcb9e42ae..ebf3d0246 100644
--- a/theories/ZArith/Zgcd_alt.v
+++ b/theories/ZArith/Zgcd_alt.v
@@ -22,7 +22,6 @@ Author: Pierre Letouzey
 Require Import ZArith_base.
 Require Import ZArithRing.
 Require Import Zdiv.
-Require Import Zgcd_def.
 Require Import Znumtheory.
 
 Open Scope Z_scope.
diff --git a/theories/ZArith/Zgcd_def.v b/theories/ZArith/Zgcd_def.v
deleted file mode 100644
index 674f705e5..000000000
--- a/theories/ZArith/Zgcd_def.v
+++ /dev/null
@@ -1,21 +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 BinInt.
-
-Open Local Scope Z_scope.
-
-Notation Zgcd := Z.gcd (only parsing).
-Notation Zggcd := Z.ggcd (only parsing).
-Notation Zggcd_gcd := Z.ggcd_gcd (only parsing).
-Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (only parsing).
-Notation Zgcd_divide_l := Z.gcd_divide_l (only parsing).
-Notation Zgcd_divide_r := Z.gcd_divide_r (only parsing).
-Notation Zgcd_greatest := Z.gcd_greatest (only parsing).
-Notation Zgcd_nonneg := Z.gcd_nonneg (only parsing).
-Notation Zggcd_opp := Z.ggcd_opp (only parsing).
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index bbc984af1..4371707dc 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -10,7 +10,6 @@ Require Import ZArith_base.
 Require Import ZArithRing.
 Require Import Zcomplements.
 Require Import Zdiv.
-Require Import Zgcd_def.
 Require Import Wf_nat.
 
 (** For compatibility reasons, this Open Scope isn't local as it should *)
@@ -23,313 +22,170 @@ Open Scope Z_scope.
      - Euclid algorithm [euclid]
      - a relatively prime predicate [rel_prime]
      - a prime predicate [prime]
-     - properties of the efficient [Zgcd] function defined in [Zgcd_def]
+     - properties of the efficient [Z.gcd] function
 *)
 
-(** * Divisibility *)
+Notation Zgcd := Z.gcd (only parsing).
+Notation Zggcd := Z.ggcd (only parsing).
+Notation Zggcd_gcd := Z.ggcd_gcd (only parsing).
+Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (only parsing).
+Notation Zgcd_divide_l := Z.gcd_divide_l (only parsing).
+Notation Zgcd_divide_r := Z.gcd_divide_r (only parsing).
+Notation Zgcd_greatest := Z.gcd_greatest (only parsing).
+Notation Zgcd_nonneg := Z.gcd_nonneg (only parsing).
+Notation Zggcd_opp := Z.ggcd_opp (only parsing).
 
-Inductive Zdivide (a b:Z) : Prop :=
-    Zdivide_intro : forall q:Z, b = q * a -> Zdivide a b.
+(** The former specialized inductive predicate [Zdivide] is now
+    a generic existential predicate. *)
 
-(** Syntax for divisibility *)
-
-Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope.
+Notation Zdivide := Z.divide (only parsing).
+Notation Zdivide_intro := ex_intro (only parsing).
 
 (** Results concerning divisibility*)
 
-Lemma Zdivide_equiv : forall a b, Z.divide a b <-> Zdivide a b.
-Proof.
- intros a b; split; intros (c,H); now exists c.
-Qed.
+Notation Zdivide_refl := Z.divide_refl (only parsing).
+Notation Zone_divide := Z.divide_1_l (only parsing).
+Notation Zdivide_0 := Z.divide_0_r (only parsing).
+Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (only parsing).
+Notation Zmult_divide_compat_r := Z.mul_divide_mono_r (only parsing).
+Notation Zdivide_plus_r := Z.divide_add_r (only parsing).
+Notation Zdivide_minus_l := Z.divide_sub_r (only parsing).
+Notation Zdivide_mult_l := Z.divide_mul_l (only parsing).
+Notation Zdivide_mult_r := Z.divide_mul_r (only parsing).
+Notation Zdivide_factor_r := Z.divide_factor_l (only parsing).
+Notation Zdivide_factor_l := Z.divide_factor_r (only parsing).
 
-Lemma Zdivide_refl : forall a:Z, (a | a).
-Proof.
-  intros; apply Zdivide_intro with 1; ring.
-Qed.
+Lemma Zdivide_opp_r a b : (a | b) -> (a | - b).
+Proof. apply Z.divide_opp_r. Qed.
 
-Lemma Zone_divide : forall a:Z, (1 | a).
-Proof.
-  intros; apply Zdivide_intro with a; ring.
-Qed.
+Lemma Zdivide_opp_r_rev a b : (a | - b) -> (a | b).
+Proof. apply Z.divide_opp_r. Qed.
 
-Lemma Zdivide_0 : forall a:Z, (a | 0).
-Proof.
-  intros; apply Zdivide_intro with 0; ring.
-Qed.
+Lemma Zdivide_opp_l a b : (a | b) -> (- a | b).
+Proof. apply Z.divide_opp_l. Qed.
 
-Hint Resolve Zdivide_refl Zone_divide Zdivide_0: zarith.
+Lemma Zdivide_opp_l_rev a b : (- a | b) -> (a | b).
+Proof. apply Z.divide_opp_l. Qed.
 
-Lemma Zmult_divide_compat_l : forall a b c:Z, (a | b) -> (c * a | c * b).
-Proof.
-  simple induction 1; intros; apply Zdivide_intro with q.
-  rewrite H0; ring.
-Qed.
+Theorem Zdivide_Zabs_l a b : (Z.abs a | b) -> (a | b).
+Proof. apply Z.divide_abs_l. Qed.
 
-Lemma Zmult_divide_compat_r : forall a b c:Z, (a | b) -> (a * c | b * c).
-Proof.
-  intros a b c; rewrite (Zmult_comm a c); rewrite (Zmult_comm b c).
-  apply Zmult_divide_compat_l; trivial.
-Qed.
+Theorem Zdivide_Zabs_inv_l a b : (a | b) -> (Z.abs a | b).
+Proof. apply Z.divide_abs_l. Qed.
 
+Hint Resolve Zdivide_refl Zone_divide Zdivide_0: zarith.
 Hint Resolve Zmult_divide_compat_l Zmult_divide_compat_r: zarith.
-
-Lemma Zdivide_plus_r : forall a b c:Z, (a | b) -> (a | c) -> (a | b + c).
-Proof.
-  simple induction 1; intros q Hq; simple induction 1; intros q' Hq'.
-  apply Zdivide_intro with (q + q').
-  rewrite Hq; rewrite Hq'; ring.
-Qed.
-
-Lemma Zdivide_opp_r : forall a b:Z, (a | b) -> (a | - b).
-Proof.
-  simple induction 1; intros; apply Zdivide_intro with (- q).
-  rewrite H0; ring.
-Qed.
-
-Lemma Zdivide_opp_r_rev : forall a b:Z, (a | - b) -> (a | b).
-Proof.
-  intros; replace b with (- - b). apply Zdivide_opp_r; trivial. ring.
-Qed.
-
-Lemma Zdivide_opp_l : forall a b:Z, (a | b) -> (- a | b).
-Proof.
-  simple induction 1; intros; apply Zdivide_intro with (- q).
-  rewrite H0; ring.
-Qed.
-
-Lemma Zdivide_opp_l_rev : forall a b:Z, (- a | b) -> (a | b).
-Proof.
-  intros; replace a with (- - a). apply Zdivide_opp_l; trivial. ring.
-Qed.
-
-Lemma Zdivide_minus_l : forall a b c:Z, (a | b) -> (a | c) -> (a | b - c).
-Proof.
-  simple induction 1; intros q Hq; simple induction 1; intros q' Hq'.
-  apply Zdivide_intro with (q - q').
-  rewrite Hq; rewrite Hq'; ring.
-Qed.
-
-Lemma Zdivide_mult_l : forall a b c:Z, (a | b) -> (a | b * c).
-Proof.
-  simple induction 1; intros q Hq; apply Zdivide_intro with (q * c).
-  rewrite Hq; ring.
-Qed.
-
-Lemma Zdivide_mult_r : forall a b c:Z, (a | c) -> (a | b * c).
-Proof.
-  simple induction 1; intros q Hq; apply Zdivide_intro with (q * b).
-  rewrite Hq; ring.
-Qed.
-
-Lemma Zdivide_factor_r : forall a b:Z, (a | a * b).
-Proof.
-  intros; apply Zdivide_intro with b; ring.
-Qed.
-
-Lemma Zdivide_factor_l : forall a b:Z, (a | b * a).
-Proof.
-  intros; apply Zdivide_intro with b; ring.
-Qed.
-
 Hint Resolve Zdivide_plus_r Zdivide_opp_r Zdivide_opp_r_rev Zdivide_opp_l
   Zdivide_opp_l_rev Zdivide_minus_l Zdivide_mult_l Zdivide_mult_r
   Zdivide_factor_r Zdivide_factor_l: zarith.
 
 (** Auxiliary result. *)
 
-Lemma Zmult_one : forall x y:Z, x >= 0 -> x * y = 1 -> x = 1.
+Lemma Zmult_one x y : x >= 0 -> x * y = 1 -> x = 1.
 Proof.
-  intros x y H H0; destruct (Zmult_1_inversion_l _ _ H0) as [Hpos| Hneg].
-  assumption.
-  rewrite Hneg in H; simpl in H.
-  contradiction (Zle_not_lt 0 (-1)).
-    apply Zge_le; assumption.
-    apply Zorder.Zlt_neg_0.
+ Z.swap_greater. apply Z.eq_mul_1_nonneg.
 Qed.
 
 (** Only [1] and [-1] divide [1]. *)
 
-Lemma Zdivide_1 : forall x:Z, (x | 1) -> x = 1 \/ x = -1.
-Proof.
-  simple induction 1; intros.
-  elim (Z_lt_ge_dec 0 x); [ left | right ].
-  apply Zmult_one with q; auto with zarith; rewrite H0; ring.
-  assert (- x = 1); auto with zarith.
-  apply Zmult_one with (- q); auto with zarith; rewrite H0; ring.
-Qed.
+Notation Zdivide_1 := Z.divide_1_r (only parsing).
 
 (** If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *)
 
-Lemma Zdivide_antisym : forall a b:Z, (a | b) -> (b | a) -> a = b \/ a = - b.
-Proof.
-  simple induction 1; intros.
-  inversion H1.
-  rewrite H0 in H2; clear H H1.
-  case (Z_zerop a); intro.
-  left; rewrite H0; rewrite e; ring.
-  assert (Hqq0 : q0 * q = 1).
-  apply Zmult_reg_l with a.
-  assumption.
-  ring_simplify.
-  pattern a at 2 in |- *; rewrite H2; ring.
-  assert (q | 1).
-  rewrite <- Hqq0; auto with zarith.
-  elim (Zdivide_1 q H); intros.
-  rewrite H1 in H0; left; omega.
-  rewrite H1 in H0; right; omega.
-Qed.
-
-Theorem Zdivide_trans: forall a b c, (a | b) -> (b | c) ->  (a | c).
-Proof.
-  intros a b c [d H1] [e H2]; exists (d * e); auto with zarith.
-  rewrite H2; rewrite H1; ring.
-Qed.
+Notation Zdivide_antisym := Z.divide_antisym (only parsing).
+Notation Zdivide_trans := Z.divide_trans (only parsing).
 
 (** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *)
 
-Lemma Zdivide_bounds : forall a b:Z, (a | b) -> b <> 0 -> Zabs a <= Zabs b.
+Lemma Zdivide_bounds a b : (a | b) -> b <> 0 -> Z.abs a <= Z.abs b.
 Proof.
-  simple induction 1; intros.
-  assert (Zabs b = Zabs q * Zabs a).
-  subst; apply Zabs_Zmult.
-  rewrite H2.
-  assert (H3 := Zabs_pos q).
-  assert (H4 := Zabs_pos a).
-  assert (Zabs q * Zabs a >= 1 * Zabs a); auto with zarith.
-  apply Zmult_ge_compat; auto with zarith.
-  elim (Z_lt_ge_dec (Zabs q) 1); [ intros | auto with zarith ].
-  assert (Zabs q = 0).
-  omega.
-  assert (q = 0).
-  rewrite <- (Zabs_Zsgn q).
-  rewrite H5; auto with zarith.
-  subst q; omega.
+ intros H Hb.
+ rewrite <- Z.divide_abs_l, <- Z.divide_abs_r in H.
+ apply Z.abs_pos in Hb.
+ now apply Z.divide_pos_le.
 Qed.
 
 (** [Zdivide] can be expressed using [Zmod]. *)
 
 Lemma Zmod_divide : forall a b, b<>0 -> a mod b = 0 -> (b | a).
 Proof.
- intros a b NZ EQ.
- apply Zdivide_intro with (a/b).
- rewrite (Z_div_mod_eq_full a b NZ) at 1.
- rewrite EQ; ring.
+ apply Z.mod_divide.
 Qed.
 
 Lemma Zdivide_mod : forall a b, (b | a) -> a mod b = 0.
 Proof.
-  intros a b (c,->); apply Z_mod_mult.
+ intros a b (c,->); apply Z_mod_mult.
 Qed.
 
 (** [Zdivide] is hence decidable *)
 
-Lemma Zdivide_dec : forall a b:Z, {(a | b)} + {~ (a | b)}.
-Proof.
-  intros a b; elim (Ztrichotomy_inf a 0).
-  (* a<0 *)
-  intros H; elim H; intros.
-  case (Z_eq_dec (b mod - a) 0).
-  left; apply Zdivide_opp_l_rev; apply Zmod_divide; auto with zarith.
-  intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith.
-  (* a=0 *)
-  case (Z_eq_dec b 0); intro.
-  left; subst; auto with zarith.
-  right; subst; intro H0; inversion H0; omega.
-  (* a>0 *)
-  intro H; case (Z_eq_dec (b mod a) 0).
-  left; apply Zmod_divide; auto with zarith.
-  intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith.
-Qed.
-
-Theorem Zdivide_Zdiv_eq: forall a b : Z,
- 0 < a -> (a | b) ->  b = a * (b / a).
+Lemma Zdivide_dec a b : {(a | b)} + {~ (a | b)}.
 Proof.
-  intros a b Hb Hc.
-  pattern b at 1; rewrite (Z_div_mod_eq b a); auto with zarith.
-  rewrite (Zdivide_mod b a); auto with zarith.
-Qed.
-
-Theorem Zdivide_Zdiv_eq_2: forall a b c : Z,
- 0 < a -> (a | b) -> (c * b)/a = c * (b / a).
-Proof.
-  intros a b c H1 H2.
-  inversion H2 as [z Hz].
-  rewrite Hz; rewrite Zmult_assoc.
-  repeat rewrite Z_div_mult; auto with zarith.
-Qed.
+ destruct (Z.eq_dec a 0) as [Ha|Ha].
+  destruct (Z.eq_dec b 0) as [Hb|Hb].
+   left; subst; apply Z.divide_0_r.
+   right. subst. contradict Hb. now apply Z.divide_0_l.
+  destruct (Z.eq_dec (b mod a) 0).
+   left. now apply Z.mod_divide.
+   right. now rewrite <- Z.mod_divide.
+Defined.
 
-Theorem Zdivide_Zabs_l: forall a b, (Zabs a | b) ->  (a | b).
+Theorem Zdivide_Zdiv_eq a b : 0 < a -> (a | b) ->  b = a * (b / a).
 Proof.
-  intros a b [x H]; subst b.
-  pattern (Zabs a); apply Zabs_intro.
-  exists (- x); ring.
-  exists x; ring.
+ intros Ha H.
+ rewrite (Z.div_mod b a) at 1; auto with zarith.
+ rewrite Zdivide_mod; auto with zarith.
 Qed.
 
-Theorem Zdivide_Zabs_inv_l: forall a b, (a | b) ->  (Zabs a | b).
+Theorem Zdivide_Zdiv_eq_2 a b c :
+ 0 < a -> (a | b) -> (c * b) / a = c * (b / a).
 Proof.
-  intros a b [x H]; subst b.
-  pattern (Zabs a); apply Zabs_intro.
-  exists (- x);  ring.
-  exists x; ring.
+ intros. apply Z.divide_div_mul_exact; auto with zarith.
 Qed.
 
 Theorem Zdivide_le: forall a b : Z,
  0 <= a -> 0 < b -> (a | b) ->  a <= b.
 Proof.
-  intros a b H1 H2 [q H3]; subst b.
-  case (Zle_lt_or_eq 0 a); auto with zarith; intros H3.
-  case (Zle_lt_or_eq 0 q); auto with zarith.
-  apply (Zmult_le_0_reg_r a); auto with zarith.
-  intros H4; apply Zle_trans with (1 * a); auto with zarith.
-  intros H4; subst q; omega.
+ intros. now apply Z.divide_pos_le.
 Qed.
 
-Theorem Zdivide_Zdiv_lt_pos: forall a b : Z,
+Theorem Zdivide_Zdiv_lt_pos a b :
  1 < a -> 0 < b -> (a | b) ->  0 < b / a < b .
 Proof.
-  intros a b H1 H2 H3; split.
-  apply Zmult_lt_reg_r with a; auto with zarith.
-  rewrite (Zmult_comm (Zdiv b a)); rewrite <- Zdivide_Zdiv_eq; auto with zarith.
-  apply Zmult_lt_reg_r with a; auto with zarith.
-  repeat rewrite (fun x => Zmult_comm x a); auto with zarith.
+  intros H1 H2 H3; split.
+  apply Z.mul_pos_cancel_l with a; auto with zarith.
   rewrite <- Zdivide_Zdiv_eq; auto with zarith.
-  pattern b at 1; replace b with (1 * b); auto with zarith.
-  apply Zmult_lt_compat_r; auto with zarith.
+  now apply Z.div_lt.
 Qed.
 
-Lemma Zmod_div_mod: forall n m a, 0 < n -> 0 < m ->
- (n | m) -> a mod n = (a mod m) mod n.
+Lemma Zmod_div_mod n m a:
+ 0 < n -> 0 < m -> (n | m) -> a mod n = (a mod m) mod n.
 Proof.
-  intros n m a H1 H2 H3.
-  pattern a at 1; rewrite (Z_div_mod_eq a m); auto with zarith.
-  case H3; intros q Hq; pattern m at 1; rewrite Hq.
-  rewrite (Zmult_comm q).
-  rewrite Zplus_mod; auto with zarith.
-  rewrite <- Zmult_assoc; rewrite Zmult_mod; auto with zarith.
-  rewrite Z_mod_same; try rewrite Zmult_0_l; auto with zarith.
-  rewrite (Zmod_small 0); auto with zarith.
-  rewrite Zplus_0_l; rewrite Zmod_mod; auto with zarith.
+  intros H1 H2 (p,Hp).
+  rewrite (Z.div_mod a m) at 1; auto with zarith.
+  rewrite Hp at 1.
+  rewrite Z.mul_shuffle0, Z.add_comm, Z.mod_add; auto with zarith.
 Qed.
 
-Lemma Zmod_divide_minus: forall a b c : Z, 0 < b ->
- a mod b = c -> (b | a - c).
+Lemma Zmod_divide_minus a b c:
+ 0 < b -> a mod b = c -> (b | a - c).
 Proof.
-  intros a b c H H1; apply Zmod_divide; auto with zarith.
+  intros H H1. apply Z.mod_divide; auto with zarith.
   rewrite Zminus_mod; auto with zarith.
-  rewrite H1; pattern c at 1; rewrite <- (Zmod_small c b); auto with zarith.
-  rewrite Zminus_diag; apply Zmod_small; auto with zarith.
-  subst; apply Z_mod_lt; auto with zarith.
+  rewrite H1. rewrite <- (Z.mod_small c b) at 1.
+  rewrite Z.sub_diag, Z.mod_0_l; auto with zarith.
+  subst. now apply Z.mod_pos_bound.
 Qed.
 
-Lemma Zdivide_mod_minus: forall a b c : Z, 0 <= c < b ->
- (b | a - c) -> a mod b = c.
+Lemma Zdivide_mod_minus a b c:
+ 0 <= c < b -> (b | a - c) -> a mod b = c.
 Proof.
-  intros a b c (H1, H2) H3; assert (0 < b); try apply Zle_lt_trans with c; auto.
+  intros (H1, H2) H3.
+  assert (0 < b) by Z.order.
   replace a with ((a - c) + c); auto with zarith.
-  rewrite Zplus_mod; auto with zarith.
-  rewrite (Zdivide_mod (a -c) b); try rewrite Zplus_0_l; auto with zarith.
-  rewrite Zmod_mod; try apply Zmod_small; auto with zarith.
+  rewrite Z.add_mod; auto with zarith.
+  rewrite (Zdivide_mod (a-c) b); try rewrite Z.add_0_l; auto with zarith.
+  rewrite Z.mod_mod; try apply Zmod_small; auto with zarith.
 Qed.
 
 (** * Greatest common divisor (gcd). *)
@@ -345,12 +201,12 @@ Inductive Zis_gcd (a b d:Z) : Prop :=
 
 (** Trivial properties of [gcd] *)
 
-Lemma Zis_gcd_sym : forall a b d:Z, Zis_gcd a b d -> Zis_gcd b a d.
+Lemma Zis_gcd_sym : forall a b d, Zis_gcd a b d -> Zis_gcd b a d.
 Proof.
-  simple induction 1; constructor; intuition.
+  induction 1; constructor; intuition.
 Qed.
 
-Lemma Zis_gcd_0 : forall a:Z, Zis_gcd a 0 a.
+Lemma Zis_gcd_0 : forall a, Zis_gcd a 0 a.
 Proof.
   constructor; auto with zarith.
 Qed.
@@ -365,19 +221,18 @@ Proof.
   constructor; auto with zarith.
 Qed.
 
-Lemma Zis_gcd_minus : forall a b d:Z, Zis_gcd a (- b) d -> Zis_gcd b a d.
+Lemma Zis_gcd_minus : forall a b d, Zis_gcd a (- b) d -> Zis_gcd b a d.
 Proof.
-  simple induction 1; constructor; intuition.
+  induction 1; constructor; intuition.
 Qed.
 
-Lemma Zis_gcd_opp : forall a b d:Z, Zis_gcd a b d -> Zis_gcd b a (- d).
+Lemma Zis_gcd_opp : forall a b d, Zis_gcd a b d -> Zis_gcd b a (- d).
 Proof.
-  simple induction 1; constructor; intuition.
+  induction 1; constructor; intuition.
 Qed.
 
-Lemma Zis_gcd_0_abs : forall a:Z, Zis_gcd 0 a (Zabs a).
+Lemma Zis_gcd_0_abs a : Zis_gcd 0 a (Z.abs a).
 Proof.
-  intros a.
   apply Zabs_ind.
   intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto.
   intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto.
@@ -526,14 +381,15 @@ Qed.
 Lemma Zis_gcd_mult :
   forall a b c d:Z, Zis_gcd a b d -> Zis_gcd (c * a) (c * b) (c * d).
 Proof.
-  intros a b c d; simple induction 1; constructor; intuition.
-  elim (Zis_gcd_bezout a b d H). intros.
-  elim H3; intros.
-  elim H4; intros.
-  apply Zdivide_intro with (u * q + v * q0).
-  rewrite <- H5.
+  intros a b c d; simple induction 1. constructor; auto with zarith.
+  intros x Ha Hb.
+  elim (Zis_gcd_bezout a b d H). intros u v Huv.
+  elim Ha; intros a' Ha'.
+  elim Hb; intros b' Hb'.
+  apply Zdivide_intro with (u * a' + v * b').
+  rewrite <- Huv.
   replace (c * (u * a + v * b)) with (u * (c * a) + v * (c * b)).
-  rewrite H6; rewrite H7; ring.
+  rewrite Ha'; rewrite Hb'; ring.
   ring.
 Qed.
 
@@ -632,14 +488,14 @@ Proof.
   exists a'; auto with zarith.
   exists b'; auto with zarith.
   intros x (xa,H5) (xb,H6).
-  destruct (H4 (x*g)).
+  destruct (H4 (x*g)) as (x',Hx').
   exists xa; rewrite Zmult_assoc; rewrite <- H5; auto.
   exists xb; rewrite Zmult_assoc; rewrite <- H6; auto.
-  replace g with (1*g) in H7; auto with zarith.
-  do 2 rewrite Zmult_assoc in H7.
-  generalize (Zmult_reg_r _ _ _ H2 H7); clear H7; intros.
-  rewrite Zmult_1_r in H7.
-  exists q; auto with zarith.
+  replace g with (1*g) in Hx'; auto with zarith.
+  do 2 rewrite Zmult_assoc in Hx'.
+  apply Zmult_reg_r in Hx'; trivial.
+  rewrite Zmult_1_r in Hx'.
+  exists x'; auto with zarith.
 Qed.
 
 Theorem rel_prime_sym: forall a b, rel_prime a b -> rel_prime b a.
@@ -882,83 +738,62 @@ Proof.
   contradict Hp; auto with zarith.
 Qed.
 
-(** we now prove that Zgcd (defined in Zgcd_def) is indeed a gcd in
-   the sense of Zis_gcd. *)
+(** we now prove that [Z.gcd] is indeed a gcd in
+   the sense of [Zis_gcd]. *)
 
-Notation Zgcd_is_pos := Zgcd_nonneg (only parsing).
+Notation Zgcd_is_pos := Z.gcd_nonneg (only parsing).
 
-Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Zgcd a b).
+Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Z.gcd a b).
 Proof.
- constructor; intros; apply Zdivide_equiv.
- apply Zgcd_divide_l.
- apply Zgcd_divide_r.
- apply Zgcd_greatest; now apply Zdivide_equiv.
+ constructor.
+ apply Z.gcd_divide_l.
+ apply Z.gcd_divide_r.
+ apply Z.gcd_greatest.
 Qed.
 
 Theorem Zgcd_spec : forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}.
 Proof.
-  intros x y; exists (Zgcd x y).
-  split; [apply Zgcd_is_gcd  | apply Zgcd_is_pos].
+  intros x y; exists (Z.gcd x y).
+  split; [apply Zgcd_is_gcd  | apply Z.gcd_nonneg].
 Qed.
 
 Theorem Zdivide_Zgcd: forall p q r : Z,
- (p | q) -> (p | r) -> (p | Zgcd q r).
+ (p | q) -> (p | r) -> (p | Z.gcd q r).
 Proof.
-  intros p q r H1 H2.
-  assert (H3: (Zis_gcd q r (Zgcd q r))).
-  apply Zgcd_is_gcd.
-  inversion_clear H3; auto.
+ intros. now apply Z.gcd_greatest.
 Qed.
 
 Theorem Zis_gcd_gcd: forall a b c : Z,
- 0 <= c ->  Zis_gcd a b c -> Zgcd a b = c.
+ 0 <= c ->  Zis_gcd a b c -> Z.gcd a b = c.
 Proof.
   intros a b c H1 H2.
   case (Zis_gcd_uniqueness_apart_sign a b c (Zgcd a b)); auto.
   apply Zgcd_is_gcd; auto.
-  case Zle_lt_or_eq with (1 := H1); clear H1; intros H1; subst; auto.
-  intros H3; subst.
-  generalize (Zgcd_is_pos a b); auto with zarith.
-  case (Zgcd a b); simpl; auto; intros; discriminate.
+  Z.le_elim H1.
+  generalize (Z.gcd_nonneg a b); auto with zarith.
+  subst. now case (Z.gcd a b).
 Qed.
 
-Theorem Zgcd_inv_0_l: forall x y, Zgcd x y = 0 -> x = 0.
-Proof.
-  intros x y H.
-  assert (F1: Zdivide 0 x).
-   rewrite <- H.
-   generalize (Zgcd_is_gcd x y); intros HH; inversion HH; auto.
-  inversion F1 as [z H1].
-  rewrite H1; ring.
-Qed.
-
-Theorem Zgcd_inv_0_r: forall x y, Zgcd x y = 0 -> y = 0.
-Proof.
-  intros x y H.
-  assert (F1: Zdivide 0 y).
-   rewrite <- H.
-   generalize (Zgcd_is_gcd x y); intros HH; inversion HH; auto.
-  inversion F1 as [z H1].
-  rewrite H1; ring.
-Qed.
+Notation Zgcd_inv_0_l := Z.gcd_eq_0_l (only parsing).
+Notation Zgcd_inv_0_r := Z.gcd_eq_0_r (only parsing).
 
 Theorem Zgcd_div_swap0 : forall a b : Z,
- 0 < Zgcd a b ->
+ 0 < Z.gcd a b ->
  0 < b ->
- (a / Zgcd a b) * b = a * (b/Zgcd a b).
+ (a / Z.gcd a b) * b = a * (b/Z.gcd a b).
 Proof.
   intros a b Hg Hb.
   assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3].
-  pattern b at 2; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto.
+  pattern b at 2; rewrite (Zdivide_Zdiv_eq (Z.gcd a b) b); auto.
   repeat rewrite Zmult_assoc; f_equal.
   rewrite Zmult_comm.
   rewrite <- Zdivide_Zdiv_eq; auto.
 Qed.
 
 Theorem Zgcd_div_swap : forall a b c : Z,
- 0 < Zgcd a b ->
+ 0 < Z.gcd a b ->
  0 < b ->
- (c * a) / Zgcd a b * b = c * a * (b/Zgcd a b).
+ (c * a) / Z.gcd a b * b = c * a * (b/Z.gcd a b).
 Proof.
   intros a b c Hg Hb.
   assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3].
@@ -970,44 +805,21 @@ Proof.
   rewrite <- Zdivide_Zdiv_eq; auto.
 Qed.
 
-Lemma Zgcd_comm : forall a b, Zgcd a b = Zgcd b a.
-Proof.
-  intros.
-  apply Zis_gcd_gcd.
-  apply Zgcd_is_pos.
-  apply Zis_gcd_sym.
-  apply Zgcd_is_gcd.
-Qed.
-
-Lemma Zgcd_ass : forall a b c, Zgcd (Zgcd a b) c = Zgcd a (Zgcd b c).
-Proof.
-  intros.
-  apply Zis_gcd_gcd.
-  apply Zgcd_is_pos.
-  destruct (Zgcd_is_gcd a b).
-  destruct (Zgcd_is_gcd b c).
-  destruct (Zgcd_is_gcd a (Zgcd b c)).
-  constructor; eauto using Zdivide_trans.
-Qed.
+Notation Zgcd_comm := Z.gcd_comm (only parsing).
 
-Lemma Zgcd_Zabs : forall a b, Zgcd (Zabs a) b = Zgcd a b.
+Lemma Zgcd_ass a b c : Zgcd (Zgcd a b) c = Zgcd a (Zgcd b c).
 Proof.
-  destruct a; simpl; auto.
+ symmetry. apply Z.gcd_assoc.
 Qed.
 
-Lemma Zgcd_0 : forall a, Zgcd a 0 = Zabs a.
-Proof.
-  destruct a; simpl; auto.
-Qed.
+Notation Zgcd_Zabs := Z.gcd_abs_l (only parsing).
+Notation Zgcd_0 := Z.gcd_0_r (only parsing).
+Notation Zgcd_1 := Z.gcd_1_r (only parsing).
 
-Lemma Zgcd_1 : forall a, Zgcd a 1 = 1.
-Proof.
-  intros; apply Zis_gcd_gcd; auto with zarith; apply Zis_gcd_1.
-Qed.
 Hint Resolve Zgcd_0 Zgcd_1 : zarith.
 
 Theorem Zgcd_1_rel_prime : forall a b,
- Zgcd a b = 1 <-> rel_prime a b.
+ Z.gcd a b = 1 <-> rel_prime a b.
 Proof.
   unfold rel_prime; split; intro H.
   rewrite <- H; apply Zgcd_is_gcd.
diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget
index cf0cdd7c7..7592d2fae 100644
--- a/theories/ZArith/vo.itarget
+++ b/theories/ZArith/vo.itarget
@@ -32,6 +32,5 @@ Zsqrt_compat.vo
 Zwf.vo
 Zsqrt_def.vo
 Zlog_def.vo
-Zgcd_def.vo
 Zeuclid.vo
 Zdigits_def.vo
\ No newline at end of file