Modularization of BinNat + fixes of stdlib

 A sub-module N in BinNat now contains functions add (ex-Nplus),
 mul (ex-Nmult), ... and properties.

 In particular, this sub-module N directly instantiates NAxiomsSig
  and includes all derived properties NProp.

 Files Ndiv_def and co are now obsolete and kept only for compat

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

3 files changed, 110 insertions, 111 deletions

diff --git a/theories/ZArith/Zdigits_def.v b/theories/ZArith/Zdigits_def.v
index 4e8e9fd93..a04719e52 100644
--- a/theories/ZArith/Zdigits_def.v
+++ b/theories/ZArith/Zdigits_def.v
@@ -8,7 +8,7 @@
 
 (** Bitwise operations for ZArith *)
 
-Require Import Bool BinPos BinNat BinInt Ndigits Znat Zeven Zpow_def
+Require Import Bool BinPos BinNat BinInt Znat Zeven Zpow_def
  Zorder Zcompare.
 
 Local Open Scope Z_scope.
@@ -28,8 +28,8 @@ Definition Ztestbit a n :=
    | 0 => Zodd_bool a
    | Zpos p => match a with
                  | 0 => false
-                 | Zpos a => Ptestbit a (Npos p)
-                 | Zneg a => negb (Ntestbit (Ppred_N a) (Npos p))
+                 | Zpos a => Pos.testbit a (Npos p)
+                 | Zneg a => negb (N.testbit (Pos.pred_N a) (Npos p))
                end
    | Zneg _ => false
  end.
@@ -60,72 +60,72 @@ Definition Zor a b :=
  match a, b with
    | 0, _ => b
    | _, 0 => a
-   | Zpos a, Zpos b => Zpos (Por a b)
-   | Zneg a, Zpos b => Zneg (Nsucc_pos (Ndiff (Ppred_N a) (Npos b)))
-   | Zpos a, Zneg b => Zneg (Nsucc_pos (Ndiff (Ppred_N b) (Npos a)))
-   | Zneg a, Zneg b => Zneg (Nsucc_pos (Nand (Ppred_N a) (Ppred_N b)))
+   | Zpos a, Zpos b => Zpos (Pos.lor a b)
+   | Zneg a, Zpos b => Zneg (N.succ_pos (N.ldiff (Pos.pred_N a) (Npos b)))
+   | Zpos a, Zneg b => Zneg (N.succ_pos (N.ldiff (Pos.pred_N b) (Npos a)))
+   | Zneg a, Zneg b => Zneg (N.succ_pos (N.land (Pos.pred_N a) (Pos.pred_N b)))
  end.
 
 Definition Zand a b :=
  match a, b with
    | 0, _ => 0
    | _, 0 => 0
-   | Zpos a, Zpos b => Z_of_N (Pand a b)
-   | Zneg a, Zpos b => Z_of_N (Ndiff (Npos b) (Ppred_N a))
-   | Zpos a, Zneg b => Z_of_N (Ndiff (Npos a) (Ppred_N b))
-   | Zneg a, Zneg b => Zneg (Nsucc_pos (Nor (Ppred_N a) (Ppred_N b)))
+   | Zpos a, Zpos b => Z_of_N (Pos.land a b)
+   | Zneg a, Zpos b => Z_of_N (N.ldiff (Npos b) (Pos.pred_N a))
+   | Zpos a, Zneg b => Z_of_N (N.ldiff (Npos a) (Pos.pred_N b))
+   | Zneg a, Zneg b => Zneg (N.succ_pos (N.lor (Pos.pred_N a) (Pos.pred_N b)))
  end.
 
 Definition Zdiff a b :=
  match a, b with
    | 0, _ => 0
    | _, 0 => a
-   | Zpos a, Zpos b => Z_of_N (Pdiff a b)
-   | Zneg a, Zpos b => Zneg (Nsucc_pos (Nor (Ppred_N a) (Npos b)))
-   | Zpos a, Zneg b => Z_of_N (Nand (Npos a) (Ppred_N b))
-   | Zneg a, Zneg b => Z_of_N (Ndiff (Ppred_N b) (Ppred_N a))
+   | Zpos a, Zpos b => Z_of_N (Pos.ldiff a b)
+   | Zneg a, Zpos b => Zneg (N.succ_pos (N.lor (Pos.pred_N a) (Npos b)))
+   | Zpos a, Zneg b => Z_of_N (N.land (Npos a) (Pos.pred_N b))
+   | Zneg a, Zneg b => Z_of_N (N.ldiff (Pos.pred_N b) (Pos.pred_N a))
  end.
 
 Definition Zxor a b :=
  match a, b with
    | 0, _ => b
    | _, 0 => a
-   | Zpos a, Zpos b => Z_of_N (Pxor a b)
-   | Zneg a, Zpos b => Zneg (Nsucc_pos (Nxor (Ppred_N a) (Npos b)))
-   | Zpos a, Zneg b => Zneg (Nsucc_pos (Nxor (Npos a) (Ppred_N b)))
-   | Zneg a, Zneg b => Z_of_N (Nxor (Ppred_N a) (Ppred_N b))
+   | Zpos a, Zpos b => Z_of_N (Pos.lxor a b)
+   | Zneg a, Zpos b => Zneg (N.succ_pos (N.lxor (Pos.pred_N a) (Npos b)))
+   | Zpos a, Zneg b => Zneg (N.succ_pos (N.lxor (Npos a) (Pos.pred_N b)))
+   | Zneg a, Zneg b => Z_of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b))
  end.
 
 
 (** Conversions between [Ztestbit] and [Ntestbit] *)
 
 Lemma Ztestbit_of_N : forall a n,
- Ztestbit (Z_of_N a) (Z_of_N n) = Ntestbit a n.
+ Ztestbit (Z_of_N a) (Z_of_N n) = N.testbit a n.
 Proof.
  intros [ |a] [ |n]; simpl; trivial. now destruct a.
 Qed.
 
 Lemma Ztestbit_of_N' : forall a n, 0<=n ->
- Ztestbit (Z_of_N a) n = Ntestbit a (Zabs_N n).
+ Ztestbit (Z_of_N a) n = N.testbit a (Zabs_N n).
 Proof.
  intros. now rewrite <- Ztestbit_of_N, Z_of_N_abs, Zabs_eq.
 Qed.
 
 Lemma Ztestbit_Zpos : forall a n, 0<=n ->
- Ztestbit (Zpos a) n = Ntestbit (Npos a) (Zabs_N n).
+ Ztestbit (Zpos a) n = N.testbit (Npos a) (Zabs_N n).
 Proof.
  intros. now rewrite <- Ztestbit_of_N'.
 Qed.
 
 Lemma Ztestbit_Zneg : forall a n, 0<=n ->
- Ztestbit (Zneg a) n = negb (Ntestbit (Ppred_N a) (Zabs_N n)).
+ Ztestbit (Zneg a) n = negb (N.testbit (Pos.pred_N a) (Zabs_N n)).
 Proof.
  intros a n Hn.
  rewrite <- Ztestbit_of_N' by trivial.
  destruct n as [ |n|n];
   [ | simpl; now destruct (Ppred_N a) | now destruct Hn].
  unfold Ztestbit.
- replace (Z_of_N (Ppred_N a)) with (Zpred (Zpos a))
+ replace (Z_of_N (Pos.pred_N a)) with (Zpred (Zpos a))
   by (destruct a; trivial).
  now rewrite Zodd_bool_pred, <- Zodd_even_bool.
 Qed.
@@ -164,7 +164,7 @@ Proof.
  destruct a as [|[a|a|]|[a|a|]]; simpl; trivial. now destruct a.
  unfold Ztestbit. rewrite <- Zpos_succ_morphism.
  destruct a as [|a|[a|a|]]; simpl; trivial;
-  rewrite ?Ppred_succ; now destruct n.
+  rewrite ?Pos.pred_N_succ; now destruct n.
 Qed.
 
 Lemma Ztestbit_even_succ a n : 0<=n ->
@@ -174,57 +174,64 @@ Proof.
  destruct a as [|[a|a|]|[a|a|]]; simpl; trivial. now destruct a.
  unfold Ztestbit. rewrite <- Zpos_succ_morphism.
  destruct a as [|a|[a|a|]]; simpl; trivial;
-  rewrite ?Ppred_succ; now destruct n.
+  rewrite ?Pos.pred_N_succ; now destruct n.
 Qed.
 
 Lemma Ppred_div2_up : forall p,
- Ppred_N (Pdiv2_up p) = Ndiv2 (Ppred_N p).
+ Pos.pred_N (Pos.div2_up p) = N.div2 (Pos.pred_N p).
 Proof.
  intros [p|p| ]; trivial.
- simpl. rewrite Ppred_N_spec. apply (Npred_succ (Npos p)).
+ simpl. apply Pos.pred_N_succ.
  destruct p; simpl; trivial.
 Qed.
 
-Lemma Z_of_N_div2 : forall n, Z_of_N (Ndiv2 n) = Zdiv2 (Z_of_N n).
+Lemma Z_of_N_div2 : forall n, Z_of_N (N.div2 n) = Zdiv2 (Z_of_N n).
 Proof.
  intros [|p]; trivial. now destruct p.
 Qed.
 
-Lemma Z_of_N_quot2 : forall n, Z_of_N (Ndiv2 n) = Zquot2 (Z_of_N n).
+Lemma Z_of_N_quot2 : forall n, Z_of_N (N.div2 n) = Zquot2 (Z_of_N n).
 Proof.
  intros [|p]; trivial. now destruct p.
 Qed.
 
 (** Auxiliary results about right shift on positive numbers *)
 
-Lemma Ppred_Pshiftl_low : forall p n m, (m<n)%nat ->
- Nbit (Ppred_N (iter_nat n _ xO p)) m = true.
+Lemma Ppred_Pshiftl_low : forall p n m, (m<n)%N ->
+ N.testbit (Pos.pred_N (Pos.shiftl p n)) m = true.
 Proof.
- induction n.
- inversion 1.
- intros m H. simpl.
- destruct m.
- now destruct (iter_nat n _ xO p).
- apply lt_S_n in H.
- specialize (IHn m H).
- now destruct (iter_nat n _ xO p).
+ induction n using N.peano_ind.
+ now destruct m.
+ intros m H. unfold Pos.shiftl.
+ destruct n as [|n]; simpl in *.
+ destruct m. now destruct p. elim (Pos.nlt_1_r _ H).
+ rewrite Pos.iter_succ. simpl.
+ set (u:=Pos.iter n xO p) in *; clearbody u.
+ destruct m as [|m]. now destruct u.
+ rewrite <- (IHn (Pos.pred_N m)).
+ rewrite <- (N.testbit_odd_succ _ (Pos.pred_N m)).
+ rewrite N.succ_pos_pred. now destruct u.
+ apply N.le_0_l.
+ apply N.succ_lt_mono. now rewrite N.succ_pos_pred.
 Qed.
 
-Lemma Ppred_Pshiftl_high : forall p n m, (n<=m)%nat ->
- Nbit (Ppred_N (iter_nat n _ xO p)) m =
- Nbit (Nshiftl_nat (Ppred_N p) n) m.
+Lemma Ppred_Pshiftl_high : forall p n m, (n<=m)%N ->
+ N.testbit (Pos.pred_N (Pos.shiftl p n)) m =
+ N.testbit (N.shiftl (Pos.pred_N p) n) m.
 Proof.
- induction n.
- now unfold Nshiftl_nat.
- intros m H.
- destruct m.
- inversion H.
- apply le_S_n in H.
- rewrite Nshiftl_nat_S.
- specialize (IHn m H).
- simpl in *.
- unfold Nbit.
- now destruct (Nshiftl_nat (Ppred_N p) n), (iter_nat n positive xO p).
+ induction n using N.peano_ind; intros m H.
+ unfold N.shiftl. simpl. now destruct (Pos.pred_N p).
+ rewrite N.shiftl_succ_r.
+ destruct n as [|n].
+ destruct m as [|m]. now destruct H. now destruct p.
+ destruct m as [|m]. now destruct H.
+ rewrite <- (N.succ_pos_pred m).
+ rewrite N.double_spec, N.testbit_even_succ by apply N.le_0_l.
+ rewrite <- IHn.
+ rewrite N.testbit_succ_r_div2 by apply N.le_0_l.
+ f_equal. simpl. rewrite Pos.iter_succ.
+ now destruct (Pos.iter n xO p).
+ apply N.succ_le_mono. now rewrite N.succ_pos_pred.
 Qed.
 
 (** Correctness proofs about [Zshiftr] and [Zshiftl] *)
@@ -245,14 +252,14 @@ Proof.
  rewrite <- (iter_pos_swap_gen _ _ _ Ndiv2) by exact Z_of_N_div2.
  rewrite Ztestbit_Zpos, Ztestbit_of_N'; trivial.
  rewrite Zabs_N_plus; try easy. simpl Zabs_N.
- exact (Nshiftr_spec (Npos a) (Npos n) (Zabs_N m)).
+ exact (N.shiftr_spec' (Npos a) (Npos n) (Zabs_N m)).
  now apply Zplus_le_0_compat.
  (* a < 0 *)
  rewrite <- (iter_pos_swap_gen _ _ _ Pdiv2_up) by trivial.
  rewrite 2 Ztestbit_Zneg; trivial. f_equal.
  rewrite Zabs_N_plus; try easy. simpl Zabs_N.
  rewrite (iter_pos_swap_gen _ _ _ _ Ndiv2) by exact Ppred_div2_up.
- exact (Nshiftr_spec (Ppred_N a) (Npos n) (Zabs_N m)).
+ exact (N.shiftr_spec' (Ppred_N a) (Npos n) (Zabs_N m)).
  now apply Zplus_le_0_compat.
 Qed.
 
@@ -271,14 +278,11 @@ Proof.
  (* a > 0 *)
  rewrite <- (iter_pos_swap_gen _ _ _ xO) by trivial.
  rewrite Ztestbit_Zpos by easy.
- exact (Nshiftl_spec_low (Npos a) (Npos n) (Npos m) H).
+ exact (N.shiftl_spec_low (Npos a) (Npos n) (Npos m) H).
  (* a < 0 *)
  rewrite <- (iter_pos_swap_gen _ _ _ xO) by trivial.
  rewrite Ztestbit_Zneg by easy.
- simpl Zabs_N.
- rewrite <- Nbit_Ntestbit, iter_nat_of_P. simpl nat_of_N.
- rewrite Ppred_Pshiftl_low; trivial.
- now apply Plt_lt.
+ now rewrite (Ppred_Pshiftl_low a (Npos n)).
 Qed.
 
 Lemma Zshiftl_spec_high : forall a n m, 0<=m -> n<=m ->
@@ -300,16 +304,13 @@ Proof.
  (* ... a > 0 *)
  rewrite <- (iter_pos_swap_gen _ _ _ xO) by trivial.
  rewrite 2 Ztestbit_Zpos, EQ by easy.
- exact (Nshiftl_spec_high (Npos p) (Npos n) (Npos m) H).
+ exact (N.shiftl_spec_high' (Npos p) (Npos n) (Npos m) H).
  (* ... a < 0 *)
  rewrite <- (iter_pos_swap_gen _ _ _ xO) by trivial.
  rewrite 2 Ztestbit_Zneg, EQ by easy. f_equal.
  simpl Zabs_N.
- rewrite <- Nshiftl_spec_high by easy.
- rewrite <- 2 Nbit_Ntestbit, iter_nat_of_P, <- Nshiftl_nat_equiv.
- simpl nat_of_N.
- apply Ppred_Pshiftl_high.
- now apply Ple_le.
+ rewrite <- N.shiftl_spec_high by easy.
+ now apply (Ppred_Pshiftl_high p (Npos n)).
  (* n < 0 *)
  unfold Zminus. simpl.
  now apply (Zshiftr_spec_aux a (Zpos n) m).
@@ -342,10 +343,10 @@ Proof.
   rewrite ?Ztestbit_0_l, ?orb_false_r; trivial; unfold Zor;
   rewrite ?Ztestbit_Zpos, ?Ztestbit_Zneg, ?Ppred_Nsucc
    by trivial.
- now rewrite <- Nor_spec.
- now rewrite Ndiff_spec, negb_andb, negb_involutive, orb_comm.
- now rewrite Ndiff_spec, negb_andb, negb_involutive.
- now rewrite Nand_spec, negb_andb.
+ now rewrite <- N.lor_spec.
+ now rewrite N.ldiff_spec, negb_andb, negb_involutive, orb_comm.
+ now rewrite N.ldiff_spec, negb_andb, negb_involutive.
+ now rewrite N.land_spec, negb_andb.
 Qed.
 
 Lemma Zand_spec : forall a b n,
@@ -357,10 +358,10 @@ Proof.
   rewrite ?Ztestbit_0_l, ?andb_false_r; trivial; unfold Zand;
   rewrite ?Ztestbit_Zpos, ?Ztestbit_Zneg, ?Ztestbit_of_N', ?Ppred_Nsucc
    by trivial.
- now rewrite <- Nand_spec.
- now rewrite Ndiff_spec.
- now rewrite Ndiff_spec, andb_comm.
- now rewrite Nor_spec, negb_orb.
+ now rewrite <- N.land_spec.
+ now rewrite N.ldiff_spec.
+ now rewrite N.ldiff_spec, andb_comm.
+ now rewrite N.lor_spec, negb_orb.
 Qed.
 
 Lemma Zdiff_spec : forall a b n,
@@ -372,10 +373,10 @@ Proof.
   rewrite ?Ztestbit_0_l, ?andb_true_r; trivial; unfold Zdiff;
   rewrite ?Ztestbit_Zpos, ?Ztestbit_Zneg, ?Ztestbit_of_N', ?Ppred_Nsucc
    by trivial.
- now rewrite <- Ndiff_spec.
- now rewrite Nand_spec, negb_involutive.
- now rewrite Nor_spec, negb_orb.
- now rewrite Ndiff_spec, negb_involutive, andb_comm.
+ now rewrite <- N.ldiff_spec.
+ now rewrite N.land_spec, negb_involutive.
+ now rewrite N.lor_spec, negb_orb.
+ now rewrite N.ldiff_spec, negb_involutive, andb_comm.
 Qed.
 
 Lemma Zxor_spec : forall a b n,
@@ -387,16 +388,17 @@ Proof.
   rewrite ?Ztestbit_0_l, ?xorb_false_l, ?xorb_false_r; trivial; unfold Zxor;
   rewrite ?Ztestbit_Zpos, ?Ztestbit_Zneg, ?Ztestbit_of_N', ?Ppred_Nsucc
    by trivial.
- now rewrite <- Nxor_spec.
- now rewrite Nxor_spec, negb_xorb_r.
- now rewrite Nxor_spec, negb_xorb_l.
- now rewrite Nxor_spec, xorb_negb_negb.
+ now rewrite <- N.lxor_spec.
+ now rewrite N.lxor_spec, negb_xorb_r.
+ now rewrite N.lxor_spec, negb_xorb_l.
+ now rewrite N.lxor_spec, xorb_negb_negb.
 Qed.
 
 (** An additionnal proof concerning [Pshiftl_nat], used in BigN *)
 
+
 Lemma Pshiftl_nat_Zpower : forall n p,
-  Zpos (Pshiftl_nat p n) = Zpos p * 2 ^ Z_of_nat n.
+  Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z_of_nat n.
 Proof.
  intros.
  rewrite Zmult_comm.
diff --git a/theories/ZArith/Zdiv_def.v b/theories/ZArith/Zdiv_def.v
index 87e04b0be..e38bec175 100644
--- a/theories/ZArith/Zdiv_def.v
+++ b/theories/ZArith/Zdiv_def.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import BinPos BinNat BinInt Zbool Zcompare Zorder Zabs Znat Ndiv_def.
+Require Import BinPos BinNat BinInt Zbool Zcompare Zorder Zabs Znat.
 Local Open Scope Z_scope.
 
 (** * Definitions of divisions for binary integers *)
@@ -113,13 +113,13 @@ Definition Zquotrem (a b:Z) : Z * Z :=
    | 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)
+     let (q, r) := N.pos_div_eucl a (Npos 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)
+     let (q, r) := N.pos_div_eucl a (Npos 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)
+     let (q, r) := N.pos_div_eucl a (Npos 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)
+     let (q, r) := N.pos_div_eucl a (Npos b) in (Z_of_N q, - Z_of_N r)
   end.
 
 Definition Zquot a b := fst (Zquotrem a b).
@@ -261,7 +261,7 @@ 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;
+ generalize (N.pos_div_eucl_spec p (Npos p0)); case N.pos_div_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.
@@ -281,19 +281,20 @@ Proof.
  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.
+ assert (H := N.pos_div_eucl_remainder a (Npos b)).
+ destruct N.pos_div_eucl as (q,r); simpl.
+ split. apply Z_of_N_le_0.
+ destruct r; [ reflexivity | now apply H ].
 Qed.
 
 Lemma Zrem_opp_l : forall a b, Zrem (-a) b = - (Zrem a b).
 Proof.
  intros [|a|a] [|b|b]; trivial; unfold Zrem;
-  simpl; destruct Pdiv_eucl; simpl; try rewrite Zopp_involutive; trivial.
+  simpl; destruct N.pos_div_eucl; simpl; try rewrite Zopp_involutive; trivial.
 Qed.
 
 Lemma Zrem_opp_r : forall a b, Zrem a (-b) = Zrem a b.
 Proof.
  intros [|a|a] [|b|b]; trivial; unfold Zrem; simpl;
-  destruct Pdiv_eucl; simpl; try rewrite Zopp_involutive; trivial.
+  destruct N.pos_div_eucl; simpl; try rewrite Zopp_involutive; trivial.
 Qed.
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index 7f0885128..ae8c20875 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing Morphisms Zdiv.
-Require Export Ndiv_def Zdiv_def.
+Require Export Zdiv_def.
 Require ZBinary ZDivTrunc.
 
 Local Open Scope Z_scope.
@@ -31,7 +31,7 @@ Lemma Ndiv_Zquot : forall a b:N,
 Proof.
   intros.
   destruct a; destruct b; simpl; auto.
-  unfold Ndiv, Zquot; simpl; destruct Pdiv_eucl; auto.
+  unfold N.div, Zquot; simpl. destruct N.pos_div_eucl; auto.
 Qed.
 
 Lemma Nmod_Zrem : forall a b:N,
@@ -39,7 +39,7 @@ Lemma Nmod_Zrem : forall a b:N,
 Proof.
   intros.
   destruct a; destruct b; simpl; auto.
-  unfold Nmod, Zrem; simpl; destruct Pdiv_eucl; auto.
+  unfold N.modulo, Zrem; simpl; destruct N.pos_div_eucl; auto.
 Qed.
 
 (** * Characterization of this euclidean division. *)
@@ -56,11 +56,7 @@ Notation Z_quot_rem_eq := Z_quot_rem_eq (only parsing).
 Theorem Zrem_lt : forall a b:Z, b<>0 ->
   Zabs (Zrem a 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).
+  apply Z.rem_bound_abs.
 Qed.
 
 (** The sign of the remainder is the one of [a]. Due to the possible
@@ -71,7 +67,7 @@ Theorem Zrem_sgn : forall a b:Z,
   0 <= Zsgn (Zrem a b) * Zsgn a.
 Proof.
   destruct b as [ |b|b]; destruct a as [ |a|a]; simpl; auto with zarith;
-  unfold Zrem, Zquotrem; destruct Pdiv_eucl;
+  unfold Zrem, Zquotrem; destruct N.pos_div_eucl;
   simpl; destruct n0; simpl; auto with zarith.
 Qed.
 
@@ -142,37 +138,37 @@ Qed.
 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.
+  unfold Zquot, Zquotrem; destruct N.pos_div_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.
+  unfold Zquot, Zquotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
 Qed.
 
 Theorem Zrem_opp_l : forall a b:Z, Zrem (-a) b = -(Zrem a b).
 Proof.
  destruct a; destruct b; simpl; auto;
-  unfold Zrem, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith.
+  unfold Zrem, Zquotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
 Qed.
 
 Theorem Zrem_opp_r : forall a b:Z, Zrem a (-b) = Zrem a b.
 Proof.
  destruct a; destruct b; simpl; auto;
-  unfold Zrem, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith.
+  unfold Zrem, Zquotrem; destruct N.pos_div_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.
+  unfold Zquot, Zquotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
 Qed.
 
 Theorem Zrem_opp_opp : forall a b:Z, Zrem (-a) (-b) = -(Zrem a b).
 Proof.
  destruct a; destruct b; simpl; auto;
-  unfold Zrem, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith.
+  unfold Zrem, Zquotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
 Qed.
 
 (** * Unicity results *)
@@ -356,7 +352,7 @@ 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.
+  unfold Zquot; simpl; destruct N.pos_div_eucl; simpl; destruct n; simpl; auto with zarith.
 Qed.
 
 (** * Relations between usual operations and Zmod and Zdiv *)