From fc2613e871dffffa788d90044a81598f671d0a3b Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 5 Jul 2012 16:56:16 +0000
Subject: ZArith + other : favor the use of modern names instead of compat
 notations

 - For instance, refl_equal --> eq_refl
 - Npos, Zpos, Zneg now admit more uniform qualified aliases
   N.pos, Z.pos, Z.neg.
 - A new module BinInt.Pos2Z with results about injections from
   positive to Z
 - A result about Z.pow pushed in the generic layer
 - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
 - Using tactic Z.le_elim instead of Zle_lt_or_eq
 - Some cleanup in ring, field, micromega
   (use of "Equivalence", "Proper" ...)
 - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
 - In ZMake and ZMake, functor parameters are now named NN and ZZ
   instead of N and Z for avoiding confusions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Rational/BigQ/BigQ.v  |   8 +-
 theories/Numbers/Rational/BigQ/QMake.v | 483 ++++++++++++++++-----------------
 2 files changed, 245 insertions(+), 246 deletions(-)

(limited to 'theories/Numbers/Rational/BigQ')

diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index 424db5b75..bc50c4148 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -26,10 +26,10 @@ Module BigN_BigZ <: NType_ZType BigN.BigN BigZ.
  reflexivity.
  Qed.
  Definition Zabs_N := BigZ.to_N.
- Lemma spec_Zabs_N : forall z, BigN.to_Z (Zabs_N z) = Zabs (BigZ.to_Z z).
+ Lemma spec_Zabs_N : forall z, BigN.to_Z (Zabs_N z) = Z.abs (BigZ.to_Z z).
  Proof.
  unfold Zabs_N; intros.
- rewrite BigZ.spec_to_Z, Zmult_comm; apply Zsgn_Zabs.
+ rewrite BigZ.spec_to_Z, Z.mul_comm; apply Z.sgn_abs.
  Qed.
 End BigN_BigZ.
 
@@ -89,10 +89,10 @@ exact BigQ.div_mul_inv. exact BigQ.mul_inv_diag_l.
 Qed.
 
 Lemma BigQpowerth :
- power_theory 1 BigQ.mul BigQ.eq Z_of_N BigQ.power.
+ power_theory 1 BigQ.mul BigQ.eq Z.of_N BigQ.power.
 Proof.
 constructor. intros. BigQ.qify.
-replace ([r] ^ Z_of_N n)%Q with (pow_N 1 Qmult [r] n)%Q by (now destruct n).
+replace ([r] ^ Z.of_N n)%Q with (pow_N 1 Qmult [r] n)%Q by (now destruct n).
 destruct n. reflexivity.
 induction p; simpl; auto; rewrite ?BigQ.spec_mul, ?IHp; reflexivity.
 Qed.
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 995fbb9ee..78ad7c470 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -19,14 +19,14 @@ Require Import NSig ZSig QSig.
     denominators. But first we will need some glue between [NType] and
     [ZType]. *)
 
-Module Type NType_ZType (N:NType)(Z:ZType).
- Parameter Z_of_N : N.t -> Z.t.
- Parameter spec_Z_of_N : forall n, Z.to_Z (Z_of_N n) = N.to_Z n.
- Parameter Zabs_N : Z.t -> N.t.
- Parameter spec_Zabs_N : forall z, N.to_Z (Zabs_N z) = Zabs (Z.to_Z z).
+Module Type NType_ZType (NN:NType)(ZZ:ZType).
+ Parameter Z_of_N : NN.t -> ZZ.t.
+ Parameter spec_Z_of_N : forall n, ZZ.to_Z (Z_of_N n) = NN.to_Z n.
+ Parameter Zabs_N : ZZ.t -> NN.t.
+ Parameter spec_Zabs_N : forall z, NN.to_Z (Zabs_N z) = Z.abs (ZZ.to_Z z).
 End NType_ZType.
 
-Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
+Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
 
  (** The notation of a rational number is either an integer x,
      interpreted as itself or a pair (x,y) of an integer x and a natural
@@ -34,8 +34,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
      interpreted as 0. *)
 
  Inductive t_ :=
-  | Qz : Z.t -> t_
-  | Qq : Z.t -> N.t -> t_.
+  | Qz : ZZ.t -> t_
+  | Qq : ZZ.t -> NN.t -> t_.
 
  Definition t := t_.
 
@@ -45,41 +45,41 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Local Open Scope Q_scope.
 
- Definition of_Z x: t := Qz (Z.of_Z x).
+ Definition of_Z x: t := Qz (ZZ.of_Z x).
 
  Definition of_Q (q:Q) : t :=
   let (x,y) := q in
   match y with
-    | 1%positive => Qz (Z.of_Z x)
-    | _ => Qq (Z.of_Z x) (N.of_N (Npos y))
+    | 1%positive => Qz (ZZ.of_Z x)
+    | _ => Qq (ZZ.of_Z x) (NN.of_N (Npos y))
   end.
 
  Definition to_Q (q: t) :=
  match q with
-   | Qz x => Z.to_Z x # 1
-   | Qq x y => if N.eqb y N.zero then 0
-               else Z.to_Z x # Z2P (N.to_Z y)
+   | Qz x => ZZ.to_Z x # 1
+   | Qq x y => if NN.eqb y NN.zero then 0
+               else ZZ.to_Z x # Z.to_pos (NN.to_Z y)
  end.
 
  Notation "[ x ]" := (to_Q x).
 
  Lemma N_to_Z_pos :
-  forall x, (N.to_Z x <> N.to_Z N.zero)%Z -> (0 < N.to_Z x)%Z.
+  forall x, (NN.to_Z x <> NN.to_Z NN.zero)%Z -> (0 < NN.to_Z x)%Z.
  Proof.
- intros x; rewrite N.spec_0; generalize (N.spec_pos x). romega.
+ intros x; rewrite NN.spec_0; generalize (NN.spec_pos x). romega.
  Qed.
 
  Ltac destr_zcompare := case Z.compare_spec; intros ?H.
 
  Ltac destr_eqb :=
   match goal with
-   | |- context [Z.eqb ?x ?y] =>
-     rewrite (Z.spec_eqb x y);
-     case (Z.eqb_spec (Z.to_Z x) (Z.to_Z y));
+   | |- context [ZZ.eqb ?x ?y] =>
+     rewrite (ZZ.spec_eqb x y);
+     case (Z.eqb_spec (ZZ.to_Z x) (ZZ.to_Z y));
      destr_eqb
-   | |- context [N.eqb ?x ?y] =>
-     rewrite (N.spec_eqb x y);
-     case (Z.eqb_spec (N.to_Z x) (N.to_Z y));
+   | |- context [NN.eqb ?x ?y] =>
+     rewrite (NN.spec_eqb x y);
+     case (Z.eqb_spec (NN.to_Z x) (NN.to_Z y));
      [ | let H:=fresh "H" in
          try (intro H;generalize (N_to_Z_pos _ H); clear H)];
      destr_eqb
@@ -87,11 +87,11 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
   end.
 
  Hint Rewrite
-  Zplus_0_r Zplus_0_l Zmult_0_r Zmult_0_l Zmult_1_r Zmult_1_l
-  Z.spec_0 N.spec_0 Z.spec_1 N.spec_1 Z.spec_m1 Z.spec_opp
-  Z.spec_compare N.spec_compare
-  Z.spec_add N.spec_add Z.spec_mul N.spec_mul Z.spec_div N.spec_div
-  Z.spec_gcd N.spec_gcd Zgcd_Zabs Zgcd_1
+  Z.add_0_r Z.add_0_l Z.mul_0_r Z.mul_0_l Z.mul_1_r Z.mul_1_l
+  ZZ.spec_0 NN.spec_0 ZZ.spec_1 NN.spec_1 ZZ.spec_m1 ZZ.spec_opp
+  ZZ.spec_compare NN.spec_compare
+  ZZ.spec_add NN.spec_add ZZ.spec_mul NN.spec_mul ZZ.spec_div NN.spec_div
+  ZZ.spec_gcd NN.spec_gcd Z.gcd_abs_l Z.gcd_1_r
   spec_Z_of_N spec_Zabs_N
  : nz.
 
@@ -99,13 +99,13 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Ltac qsimpl := try red; unfold to_Q; simpl; intros;
   destr_eqb; simpl; nzsimpl; intros;
-  rewrite ?Z2P_correct by auto;
+  rewrite ?Z2Pos.id by auto;
   auto.
 
  Theorem strong_spec_of_Q: forall q: Q, [of_Q q] = q.
  Proof.
- intros(x,y); destruct y; simpl; rewrite ?Z.spec_of_Z; auto;
-  destr_eqb; now rewrite ?N.spec_0, ?N.spec_of_N.
+ intros(x,y); destruct y; simpl; rewrite ?ZZ.spec_of_Z; auto;
+  destr_eqb; now rewrite ?NN.spec_0, ?NN.spec_of_N.
  Qed.
 
  Theorem spec_of_Q: forall q: Q, [of_Q q] == q.
@@ -115,9 +115,9 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Definition eq x y := [x] == [y].
 
- Definition zero: t := Qz Z.zero.
- Definition one: t := Qz Z.one.
- Definition minus_one: t := Qz Z.minus_one.
+ Definition zero: t := Qz ZZ.zero.
+ Definition one: t := Qz ZZ.one.
+ Definition minus_one: t := Qz ZZ.minus_one.
 
  Lemma spec_0: [zero] == 0.
  Proof.
@@ -136,20 +136,20 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Definition compare (x y: t) :=
   match x, y with
-  | Qz zx, Qz zy => Z.compare zx zy
+  | Qz zx, Qz zy => ZZ.compare zx zy
   | Qz zx, Qq ny dy =>
-    if N.eqb dy N.zero then Z.compare zx Z.zero
-    else Z.compare (Z.mul zx (Z_of_N dy)) ny
+    if NN.eqb dy NN.zero then ZZ.compare zx ZZ.zero
+    else ZZ.compare (ZZ.mul zx (Z_of_N dy)) ny
   | Qq nx dx, Qz zy =>
-    if N.eqb dx N.zero then Z.compare Z.zero zy
-    else Z.compare nx (Z.mul zy (Z_of_N dx))
+    if NN.eqb dx NN.zero then ZZ.compare ZZ.zero zy
+    else ZZ.compare nx (ZZ.mul zy (Z_of_N dx))
   | Qq nx dx, Qq ny dy =>
-    match N.eqb dx N.zero, N.eqb dy N.zero with
+    match NN.eqb dx NN.zero, NN.eqb dy NN.zero with
     | true, true => Eq
-    | true, false => Z.compare Z.zero ny
-    | false, true => Z.compare nx Z.zero
-    | false, false => Z.compare (Z.mul nx (Z_of_N dy))
-                                (Z.mul ny (Z_of_N dx))
+    | true, false => ZZ.compare ZZ.zero ny
+    | false, true => ZZ.compare nx ZZ.zero
+    | false, false => ZZ.compare (ZZ.mul nx (Z_of_N dy))
+                                (ZZ.mul ny (Z_of_N dx))
     end
   end.
 
@@ -188,7 +188,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  (** [check_int] : is a reduced fraction [n/d] in fact a integer ? *)
 
  Definition check_int n d :=
-  match N.compare N.one d with
+  match NN.compare NN.one d with
   | Lt => Qq n d
   | Eq => Qz n
   | Gt => zero  (* n/0 encodes 0 *)
@@ -207,9 +207,9 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  (** Normalisation function *)
 
  Definition norm n d : t :=
-  let gcd := N.gcd (Zabs_N n) d in
-  match N.compare N.one gcd with
-  | Lt => check_int (Z.div n (Z_of_N gcd)) (N.div d gcd)
+  let gcd := NN.gcd (Zabs_N n) d in
+  match NN.compare NN.one gcd with
+  | Lt => check_int (ZZ.div n (Z_of_N gcd)) (NN.div d gcd)
   | Eq => check_int n d
   | Gt => zero (* gcd = 0 => both numbers are 0 *)
   end.
@@ -217,8 +217,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_norm: forall n q, [norm n q] == [Qq n q].
  Proof.
  intros p q; unfold norm.
- assert (Hp := N.spec_pos (Zabs_N p)).
- assert (Hq := N.spec_pos q).
+ assert (Hp := NN.spec_pos (Zabs_N p)).
+ assert (Hq := NN.spec_pos q).
  nzsimpl.
  destr_zcompare.
  (* Eq *)
@@ -226,15 +226,15 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  (* Lt *)
  rewrite strong_spec_check_int.
  qsimpl.
- generalize (Zgcd_div_pos (Z.to_Z p) (N.to_Z q)). romega.
- replace (N.to_Z q) with 0%Z in * by assumption.
+ generalize (Zgcd_div_pos (ZZ.to_Z p) (NN.to_Z q)). romega.
+ replace (NN.to_Z q) with 0%Z in * by assumption.
  rewrite Zdiv_0_l in *; auto with zarith.
  apply Zgcd_div_swap0; romega.
  (* Gt *)
  qsimpl.
- assert (H' : Zgcd (Z.to_Z p) (N.to_Z q) = 0%Z).
-  generalize (Zgcd_is_pos (Z.to_Z p) (N.to_Z q)); romega.
- symmetry; apply (Zgcd_inv_0_l _ _ H'); auto.
+ assert (H' : Z.gcd (ZZ.to_Z p) (NN.to_Z q) = 0%Z).
+  generalize (Z.gcd_nonneg (ZZ.to_Z p) (NN.to_Z q)); romega.
+ symmetry; apply (Z.gcd_eq_0_l _ _ H'); auto.
  Qed.
 
  Theorem strong_spec_norm : forall p q, [norm p q] = Qred [Qq p q].
@@ -244,8 +244,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
   (apply Qred_complete; apply spec_norm).
  symmetry; apply Qred_identity.
  unfold norm.
- assert (Hp := N.spec_pos (Zabs_N p)).
- assert (Hq := N.spec_pos q).
+ assert (Hp := NN.spec_pos (Zabs_N p)).
+ assert (Hq := NN.spec_pos q).
  nzsimpl.
  destr_zcompare; rewrite ?strong_spec_check_int.
  (* Eq *)
@@ -253,10 +253,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  (* Lt *)
  qsimpl.
  rewrite Zgcd_1_rel_prime.
- destruct (Z_lt_le_dec 0 (N.to_Z q)).
+ destruct (Z_lt_le_dec 0 (NN.to_Z q)).
  apply Zis_gcd_rel_prime; auto with zarith.
  apply Zgcd_is_gcd.
- replace (N.to_Z q) with 0%Z in * by romega.
+ replace (NN.to_Z q) with 0%Z in * by romega.
  rewrite Zdiv_0_l in *; romega.
  (* Gt *)
  simpl; auto with zarith.
@@ -292,20 +292,20 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
   match x with
   | Qz zx =>
     match y with
-    | Qz zy => Qz (Z.add zx zy)
+    | Qz zy => Qz (ZZ.add zx zy)
     | Qq ny dy =>
-      if N.eqb dy N.zero then x
-      else Qq (Z.add (Z.mul zx (Z_of_N dy)) ny) dy
+      if NN.eqb dy NN.zero then x
+      else Qq (ZZ.add (ZZ.mul zx (Z_of_N dy)) ny) dy
     end
   | Qq nx dx =>
-    if N.eqb dx N.zero then y
+    if NN.eqb dx NN.zero then y
     else match y with
-    | Qz zy => Qq (Z.add nx (Z.mul zy (Z_of_N dx))) dx
+    | Qz zy => Qq (ZZ.add nx (ZZ.mul zy (Z_of_N dx))) dx
     | Qq ny dy =>
-      if N.eqb dy N.zero then x
+      if NN.eqb dy NN.zero then x
       else
-       let n := Z.add (Z.mul nx (Z_of_N dy)) (Z.mul ny (Z_of_N dx)) in
-       let d := N.mul dx dy in
+       let n := ZZ.add (ZZ.mul nx (Z_of_N dy)) (ZZ.mul ny (Z_of_N dx)) in
+       let d := NN.mul dx dy in
        Qq n d
     end
   end.
@@ -314,30 +314,30 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Proof.
  intros [x | nx dx] [y | ny dy]; unfold Qplus; qsimpl;
   auto with zarith.
- rewrite Pmult_1_r, Z2P_correct; auto.
- rewrite Pmult_1_r, Z2P_correct; auto.
- destruct (Zmult_integral (N.to_Z dx) (N.to_Z dy)); intuition.
- rewrite Zpos_mult_morphism, 2 Z2P_correct; auto.
+ rewrite Pos.mul_1_r, Z2Pos.id; auto.
+ rewrite Pos.mul_1_r, Z2Pos.id; auto.
+ rewrite Z.mul_eq_0 in *; intuition.
+ rewrite Pos2Z.inj_mul, 2 Z2Pos.id; auto.
  Qed.
 
  Definition add_norm (x y: t): t :=
   match x with
   | Qz zx =>
     match y with
-    | Qz zy => Qz (Z.add zx zy)
+    | Qz zy => Qz (ZZ.add zx zy)
     | Qq ny dy =>
-      if N.eqb dy N.zero then x
-      else norm (Z.add (Z.mul zx (Z_of_N dy)) ny) dy
+      if NN.eqb dy NN.zero then x
+      else norm (ZZ.add (ZZ.mul zx (Z_of_N dy)) ny) dy
     end
   | Qq nx dx =>
-    if N.eqb dx N.zero then y
+    if NN.eqb dx NN.zero then y
     else match y with
-    | Qz zy => norm (Z.add nx (Z.mul zy (Z_of_N dx))) dx
+    | Qz zy => norm (ZZ.add nx (ZZ.mul zy (Z_of_N dx))) dx
     | Qq ny dy =>
-      if N.eqb dy N.zero then x
+      if NN.eqb dy NN.zero then x
       else
-       let n := Z.add (Z.mul nx (Z_of_N dy)) (Z.mul ny (Z_of_N dx)) in
-       let d := N.mul dx dy in
+       let n := ZZ.add (ZZ.mul nx (Z_of_N dy)) (ZZ.mul ny (Z_of_N dx)) in
+       let d := NN.mul dx dy in
        norm n d
     end
   end.
@@ -363,18 +363,18 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Definition opp (x: t): t :=
   match x with
-  | Qz zx => Qz (Z.opp zx)
-  | Qq nx dx => Qq (Z.opp nx) dx
+  | Qz zx => Qz (ZZ.opp zx)
+  | Qq nx dx => Qq (ZZ.opp nx) dx
   end.
 
  Theorem strong_spec_opp: forall q, [opp q] = -[q].
  Proof.
  intros [z | x y]; simpl.
- rewrite Z.spec_opp; auto.
- match goal with  |- context[N.eqb ?X ?Y] =>
-  generalize (N.spec_eqb X Y); case N.eqb
- end; auto; rewrite N.spec_0.
- rewrite Z.spec_opp; auto.
+ rewrite ZZ.spec_opp; auto.
+ match goal with  |- context[NN.eqb ?X ?Y] =>
+  generalize (NN.spec_eqb X Y); case NN.eqb
+ end; auto; rewrite NN.spec_0.
+ rewrite ZZ.spec_opp; auto.
  Qed.
 
  Theorem spec_opp : forall q, [opp q] == -[q].
@@ -416,28 +416,28 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Definition mul (x y: t): t :=
   match x, y with
-  | Qz zx, Qz zy => Qz (Z.mul zx zy)
-  | Qz zx, Qq ny dy => Qq (Z.mul zx ny) dy
-  | Qq nx dx, Qz zy => Qq (Z.mul nx zy) dx
-  | Qq nx dx, Qq ny dy => Qq (Z.mul nx ny) (N.mul dx dy)
+  | Qz zx, Qz zy => Qz (ZZ.mul zx zy)
+  | Qz zx, Qq ny dy => Qq (ZZ.mul zx ny) dy
+  | Qq nx dx, Qz zy => Qq (ZZ.mul nx zy) dx
+  | Qq nx dx, Qq ny dy => Qq (ZZ.mul nx ny) (NN.mul dx dy)
   end.
 
  Ltac nsubst :=
-  match goal with E : N.to_Z _ = _ |- _ => rewrite E in * end.
+  match goal with E : NN.to_Z _ = _ |- _ => rewrite E in * end.
 
  Theorem spec_mul : forall x y, [mul x y] == [x] * [y].
  Proof.
  intros [x | nx dx] [y | ny dy]; unfold Qmult; simpl; qsimpl.
- rewrite Pmult_1_r, Z2P_correct; auto.
- destruct (Zmult_integral (N.to_Z dx) (N.to_Z dy)); intuition.
+ rewrite Pos.mul_1_r, Z2Pos.id; auto.
+ rewrite Z.mul_eq_0 in *; intuition.
  nsubst; auto with zarith.
  nsubst; auto with zarith.
  nsubst; nzsimpl; auto with zarith.
- rewrite Zpos_mult_morphism, 2 Z2P_correct; auto.
+ rewrite Pos2Z.inj_mul, 2 Z2Pos.id; auto.
  Qed.
 
  Definition norm_denum n d :=
-  if N.eqb d N.one then Qz n else Qq n d.
+  if NN.eqb d NN.one then Qz n else Qq n d.
 
  Lemma spec_norm_denum : forall n d,
   [norm_denum n d] == [Qq n d].
@@ -448,40 +448,40 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Qed.
 
  Definition irred n d :=
-   let gcd := N.gcd (Zabs_N n) d in
-   match N.compare gcd N.one with
-     | Gt => (Z.div n (Z_of_N gcd), N.div d gcd)
+   let gcd := NN.gcd (Zabs_N n) d in
+   match NN.compare gcd NN.one with
+     | Gt => (ZZ.div n (Z_of_N gcd), NN.div d gcd)
      | _ => (n, d)
    end.
 
  Lemma spec_irred : forall n d, exists g,
   let (n',d') := irred n d in
-  (Z.to_Z n' * g = Z.to_Z n)%Z /\ (N.to_Z d' * g = N.to_Z d)%Z.
+  (ZZ.to_Z n' * g = ZZ.to_Z n)%Z /\ (NN.to_Z d' * g = NN.to_Z d)%Z.
  Proof.
  intros.
  unfold irred; nzsimpl; simpl.
  destr_zcompare.
  exists 1%Z; nzsimpl; auto.
  exists 0%Z; nzsimpl.
- assert (Zgcd (Z.to_Z n) (N.to_Z d) = 0%Z).
-  generalize (Zgcd_is_pos (Z.to_Z n) (N.to_Z d)); romega.
+ assert (Z.gcd (ZZ.to_Z n) (NN.to_Z d) = 0%Z).
+  generalize (Z.gcd_nonneg (ZZ.to_Z n) (NN.to_Z d)); romega.
  clear H.
  split.
- symmetry; apply (Zgcd_inv_0_l _ _ H0).
- symmetry; apply (Zgcd_inv_0_r _ _ H0).
- exists (Zgcd (Z.to_Z n) (N.to_Z d)).
+ symmetry; apply (Z.gcd_eq_0_l _ _ H0).
+ symmetry; apply (Z.gcd_eq_0_r _ _ H0).
+ exists (Z.gcd (ZZ.to_Z n) (NN.to_Z d)).
  simpl.
  split.
  nzsimpl.
- destruct (Zgcd_is_gcd (Z.to_Z n) (N.to_Z d)).
- rewrite Zmult_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith.
+ destruct (Zgcd_is_gcd (ZZ.to_Z n) (NN.to_Z d)).
+ rewrite Z.mul_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith.
  nzsimpl.
- destruct (Zgcd_is_gcd (Z.to_Z n) (N.to_Z d)).
- rewrite Zmult_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith.
+ destruct (Zgcd_is_gcd (ZZ.to_Z n) (NN.to_Z d)).
+ rewrite Z.mul_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith.
  Qed.
 
  Lemma spec_irred_zero : forall n d,
-   (N.to_Z d = 0)%Z <-> (N.to_Z (snd (irred n d)) = 0)%Z.
+   (NN.to_Z d = 0)%Z <-> (NN.to_Z (snd (irred n d)) = 0)%Z.
  Proof.
  intros.
  unfold irred.
@@ -494,8 +494,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  nzsimpl; destr_zcompare; simpl; auto.
  nzsimpl.
  intros.
- generalize (N.spec_pos d); intros.
- destruct (N.to_Z d); auto.
+ generalize (NN.spec_pos d); intros.
+ destruct (NN.to_Z d); auto.
  assert (0 < 0)%Z.
   rewrite <- H0 at 2.
   apply Zgcd_div_pos; auto with zarith.
@@ -505,49 +505,49 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Qed.
 
  Lemma strong_spec_irred : forall n d,
-  (N.to_Z d <> 0%Z) ->
-  let (n',d') := irred n d in Zgcd (Z.to_Z n') (N.to_Z d') = 1%Z.
+  (NN.to_Z d <> 0%Z) ->
+  let (n',d') := irred n d in Z.gcd (ZZ.to_Z n') (NN.to_Z d') = 1%Z.
  Proof.
  unfold irred; intros.
  nzsimpl.
  destr_zcompare; simpl; auto.
  elim H.
- apply (Zgcd_inv_0_r (Z.to_Z n)).
- generalize (Zgcd_is_pos (Z.to_Z n) (N.to_Z d)); romega.
+ apply (Z.gcd_eq_0_r (ZZ.to_Z n)).
+ generalize (Z.gcd_nonneg (ZZ.to_Z n) (NN.to_Z d)); romega.
 
  nzsimpl.
  rewrite Zgcd_1_rel_prime.
  apply Zis_gcd_rel_prime.
- generalize (N.spec_pos d); romega.
- generalize (Zgcd_is_pos (Z.to_Z n) (N.to_Z d)); romega.
+ generalize (NN.spec_pos d); romega.
+ generalize (Z.gcd_nonneg (ZZ.to_Z n) (NN.to_Z d)); romega.
  apply Zgcd_is_gcd; auto.
  Qed.
 
  Definition mul_norm_Qz_Qq z n d :=
-   if Z.eqb z Z.zero then zero
+   if ZZ.eqb z ZZ.zero then zero
    else
-    let gcd := N.gcd (Zabs_N z) d in
-    match N.compare gcd N.one with
+    let gcd := NN.gcd (Zabs_N z) d in
+    match NN.compare gcd NN.one with
       | Gt =>
-        let z := Z.div z (Z_of_N gcd) in
-        let d := N.div d gcd in
-        norm_denum (Z.mul z n) d
-      | _  => Qq (Z.mul z n) d
+        let z := ZZ.div z (Z_of_N gcd) in
+        let d := NN.div d gcd in
+        norm_denum (ZZ.mul z n) d
+      | _  => Qq (ZZ.mul z n) d
     end.
 
  Definition mul_norm (x y: t): t :=
  match x, y with
- | Qz zx, Qz zy => Qz (Z.mul zx zy)
+ | Qz zx, Qz zy => Qz (ZZ.mul zx zy)
  | Qz zx, Qq ny dy => mul_norm_Qz_Qq zx ny dy
  | Qq nx dx, Qz zy => mul_norm_Qz_Qq zy nx dx
  | Qq nx dx, Qq ny dy =>
     let (nx, dy) := irred nx dy in
     let (ny, dx) := irred ny dx in
-    norm_denum (Z.mul ny nx) (N.mul dx dy)
+    norm_denum (ZZ.mul ny nx) (NN.mul dx dy)
  end.
 
  Lemma spec_mul_norm_Qz_Qq : forall z n d,
-   [mul_norm_Qz_Qq z n d] == [Qq (Z.mul z n) d].
+   [mul_norm_Qz_Qq z n d] == [Qq (ZZ.mul z n) d].
  Proof.
  intros z n d; unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt.
  destr_eqb; nzsimpl; intros Hz.
@@ -558,7 +558,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  qsimpl.
  rewrite Zdiv_gcd_zero in GT; auto with zarith.
  nsubst. rewrite Zdiv_0_l in *; discriminate.
- rewrite <- Zmult_assoc, (Zmult_comm (Z.to_Z n)), Zmult_assoc.
+ rewrite <- Z.mul_assoc, (Z.mul_comm (ZZ.to_Z n)), Z.mul_assoc.
  rewrite Zgcd_div_swap0; try romega.
  ring.
  Qed.
@@ -582,34 +582,34 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  destr_eqb; simpl; nzsimpl; auto.
  nzsimpl; rewrite Hd, Zdiv_0_l; auto with zarith.
 
- rewrite Z2P_correct in H; auto.
+ rewrite Z2Pos.id in H; auto.
  unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt.
  destr_eqb; intros Hz; simpl; nzsimpl; simpl; auto.
  destruct Z_le_gt_dec as [H'|H'].
  simpl; nzsimpl.
  destr_eqb; simpl; nzsimpl; auto.
  intros.
- rewrite Z2P_correct; auto.
+ rewrite Z2Pos.id; auto.
  apply Zgcd_mult_rel_prime; auto.
-  generalize (Zgcd_inv_0_l (Z.to_Z z) (N.to_Z d))
-    (Zgcd_is_pos (Z.to_Z z) (N.to_Z d)); romega.
+  generalize (Z.gcd_eq_0_l (ZZ.to_Z z) (NN.to_Z d))
+    (Z.gcd_nonneg (ZZ.to_Z z) (NN.to_Z d)); romega.
  destr_eqb; simpl; nzsimpl; auto.
  unfold norm_denum.
  destr_eqb; nzsimpl; simpl; destr_eqb; simpl; auto.
  intros; nzsimpl.
- rewrite Z2P_correct; auto.
+ rewrite Z2Pos.id; auto.
  apply Zgcd_mult_rel_prime.
  rewrite Zgcd_1_rel_prime.
  apply Zis_gcd_rel_prime.
- generalize (N.spec_pos d); romega.
- generalize (Zgcd_is_pos (Z.to_Z z) (N.to_Z d)); romega.
+ generalize (NN.spec_pos d); romega.
+ generalize (Z.gcd_nonneg (ZZ.to_Z z) (NN.to_Z d)); romega.
  apply Zgcd_is_gcd.
- destruct (Zgcd_is_gcd (Z.to_Z z) (N.to_Z d)) as [ (z0,Hz0) (d0,Hd0) Hzd].
- replace (N.to_Z d / Zgcd (Z.to_Z z) (N.to_Z d))%Z with d0.
+ destruct (Zgcd_is_gcd (ZZ.to_Z z) (NN.to_Z d)) as [ (z0,Hz0) (d0,Hd0) Hzd].
+ replace (NN.to_Z d / Z.gcd (ZZ.to_Z z) (NN.to_Z d))%Z with d0.
  rewrite Zgcd_1_rel_prime in *.
  apply bezout_rel_prime.
  destruct (rel_prime_bezout _ _ H) as [u v Huv].
- apply Bezout_intro with u (v*(Zgcd (Z.to_Z z) (N.to_Z d)))%Z.
+ apply Bezout_intro with u (v*(Z.gcd (ZZ.to_Z z) (NN.to_Z d)))%Z.
  rewrite <- Huv; rewrite Hd0 at 2; ring.
  rewrite Hd0 at 1.
  symmetry; apply Z_div_mult_full; auto with zarith.
@@ -634,14 +634,14 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  qsimpl.
 
  match goal with E : (_ * _ = 0)%Z |- _ =>
-  destruct (Zmult_integral _ _ E) as [Eq|Eq] end.
+  rewrite Z.mul_eq_0 in E; destruct E as [Eq|Eq] end.
  rewrite Eq in *; simpl in *.
  rewrite <- Hg2' in *; auto with zarith.
  rewrite Eq in *; simpl in *.
  rewrite <- Hg2 in *; auto with zarith.
 
  match goal with E : (_ * _ = 0)%Z |- _ =>
-  destruct (Zmult_integral _ _ E) as [Eq|Eq] end.
+  rewrite Z.mul_eq_0 in E; destruct E as [Eq|Eq] end.
  rewrite Hz' in Eq; rewrite Eq in *; auto with zarith.
  rewrite Hz in Eq; rewrite Eq in *; auto with zarith.
 
@@ -671,31 +671,31 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  unfold norm_denum; qsimpl.
 
- assert (NEQ : N.to_Z dy <> 0%Z) by
+ assert (NEQ : NN.to_Z dy <> 0%Z) by
   (rewrite Hz; intros EQ; rewrite EQ in *; romega).
  specialize (Hgc NEQ).
 
- assert (NEQ' : N.to_Z dx <> 0%Z) by
+ assert (NEQ' : NN.to_Z dx <> 0%Z) by
   (rewrite Hz'; intro EQ; rewrite EQ in *; romega).
  specialize (Hgc' NEQ').
 
  revert H H0.
  rewrite 2 strong_spec_red, 2 Qred_iff; simpl.
  destr_eqb; simpl; nzsimpl; try romega; intros.
- rewrite Z2P_correct in *; auto.
+ rewrite Z2Pos.id in *; auto.
 
- apply Zgcd_mult_rel_prime; rewrite Zgcd_comm;
-  apply Zgcd_mult_rel_prime; rewrite Zgcd_comm; auto.
+ apply Zgcd_mult_rel_prime; rewrite Z.gcd_comm;
+  apply Zgcd_mult_rel_prime; rewrite Z.gcd_comm; auto.
 
  rewrite Zgcd_1_rel_prime in *.
  apply bezout_rel_prime.
- destruct (rel_prime_bezout (Z.to_Z ny) (N.to_Z dy)) as [u v Huv]; trivial.
+ destruct (rel_prime_bezout (ZZ.to_Z ny) (NN.to_Z dy)) as [u v Huv]; trivial.
  apply Bezout_intro with (u*g')%Z (v*g)%Z.
  rewrite <- Huv, <- Hg1', <- Hg2. ring.
 
  rewrite Zgcd_1_rel_prime in *.
  apply bezout_rel_prime.
- destruct (rel_prime_bezout (Z.to_Z nx) (N.to_Z dx)) as [u v Huv]; trivial.
+ destruct (rel_prime_bezout (ZZ.to_Z nx) (NN.to_Z dx)) as [u v Huv]; trivial.
  apply Bezout_intro with (u*g)%Z (v*g')%Z.
  rewrite <- Huv, <- Hg2', <- Hg1. ring.
  Qed.
@@ -703,16 +703,16 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Definition inv (x: t): t :=
  match x with
  | Qz z =>
-   match Z.compare Z.zero z with
+   match ZZ.compare ZZ.zero z with
      | Eq => zero
-     | Lt => Qq Z.one (Zabs_N z)
-     | Gt => Qq Z.minus_one (Zabs_N z)
+     | Lt => Qq ZZ.one (Zabs_N z)
+     | Gt => Qq ZZ.minus_one (Zabs_N z)
    end
  | Qq n d =>
-   match Z.compare Z.zero n with
+   match ZZ.compare ZZ.zero n with
      | Eq => zero
      | Lt => Qq (Z_of_N d) (Zabs_N n)
-     | Gt => Qq (Z.opp (Z_of_N d)) (Zabs_N n)
+     | Gt => Qq (ZZ.opp (Z_of_N d)) (Zabs_N n)
    end
  end.
 
@@ -721,29 +721,29 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  destruct x as [ z | n d ].
  (* Qz z *)
  simpl.
- rewrite Z.spec_compare; destr_zcompare.
+ rewrite ZZ.spec_compare; destr_zcompare.
  (* 0 = z *)
  rewrite <- H.
  simpl; nzsimpl; compute; auto.
  (* 0 < z *)
  simpl.
- destr_eqb; nzsimpl; [ intros; rewrite Zabs_eq in *; romega | intros _ ].
- set (z':=Z.to_Z z) in *; clearbody z'.
+ destr_eqb; nzsimpl; [ intros; rewrite Z.abs_eq in *; romega | intros _ ].
+ set (z':=ZZ.to_Z z) in *; clearbody z'.
  red; simpl.
- rewrite Zabs_eq by romega.
- rewrite Z2P_correct by auto.
+ rewrite Z.abs_eq by romega.
+ rewrite Z2Pos.id by auto.
  unfold Qinv; simpl; destruct z'; simpl; auto; discriminate.
  (* 0 > z *)
  simpl.
- destr_eqb; nzsimpl; [ intros; rewrite Zabs_non_eq in *; romega | intros _ ].
- set (z':=Z.to_Z z) in *; clearbody z'.
+ destr_eqb; nzsimpl; [ intros; rewrite Z.abs_neq in *; romega | intros _ ].
+ set (z':=ZZ.to_Z z) in *; clearbody z'.
  red; simpl.
- rewrite Zabs_non_eq by romega.
- rewrite Z2P_correct by romega.
+ rewrite Z.abs_neq by romega.
+ rewrite Z2Pos.id by romega.
  unfold Qinv; simpl; destruct z'; simpl; auto; discriminate.
  (* Qq n d *)
  simpl.
- rewrite Z.spec_compare; destr_zcompare.
+ rewrite ZZ.spec_compare; destr_zcompare.
  (* 0 = n *)
  rewrite <- H.
  simpl; nzsimpl.
@@ -751,51 +751,51 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  (* 0 < n *)
  simpl.
  destr_eqb; nzsimpl; intros.
- intros; rewrite Zabs_eq in *; romega.
- intros; rewrite Zabs_eq in *; romega.
+ intros; rewrite Z.abs_eq in *; romega.
+ intros; rewrite Z.abs_eq in *; romega.
  nsubst; compute; auto.
- set (n':=Z.to_Z n) in *; clearbody n'.
- rewrite Zabs_eq by romega.
+ set (n':=ZZ.to_Z n) in *; clearbody n'.
+ rewrite Z.abs_eq by romega.
  red; simpl.
- rewrite Z2P_correct by auto.
+ rewrite Z2Pos.id by auto.
  unfold Qinv; simpl; destruct n'; simpl; auto; try discriminate.
- rewrite Zpos_mult_morphism, Z2P_correct; auto.
+ rewrite Pos2Z.inj_mul, Z2Pos.id; auto.
  (* 0 > n *)
  simpl.
  destr_eqb; nzsimpl; intros.
- intros; rewrite Zabs_non_eq in *; romega.
- intros; rewrite Zabs_non_eq in *; romega.
+ intros; rewrite Z.abs_neq in *; romega.
+ intros; rewrite Z.abs_neq in *; romega.
  nsubst; compute; auto.
- set (n':=Z.to_Z n) in *; clearbody n'.
+ set (n':=ZZ.to_Z n) in *; clearbody n'.
  red; simpl; nzsimpl.
- rewrite Zabs_non_eq by romega.
- rewrite Z2P_correct by romega.
+ rewrite Z.abs_neq by romega.
+ rewrite Z2Pos.id by romega.
  unfold Qinv; simpl; destruct n'; simpl; auto; try discriminate.
- assert (T : forall x, Zneg x = Zopp (Zpos x)) by auto.
- rewrite T, Zpos_mult_morphism, Z2P_correct; auto; ring.
+ assert (T : forall x, Zneg x = Z.opp (Zpos x)) by auto.
+ rewrite T, Pos2Z.inj_mul, Z2Pos.id; auto; ring.
  Qed.
 
  Definition inv_norm (x: t): t :=
    match x with
      | Qz z =>
-       match Z.compare Z.zero z with
+       match ZZ.compare ZZ.zero z with
          | Eq => zero
-         | Lt => Qq Z.one (Zabs_N z)
-         | Gt => Qq Z.minus_one (Zabs_N z)
+         | Lt => Qq ZZ.one (Zabs_N z)
+         | Gt => Qq ZZ.minus_one (Zabs_N z)
        end
      | Qq n d =>
-       if N.eqb d N.zero then zero else
-       match Z.compare Z.zero n with
+       if NN.eqb d NN.zero then zero else
+       match ZZ.compare ZZ.zero n with
          | Eq => zero
          | Lt =>
-           match Z.compare n Z.one with
+           match ZZ.compare n ZZ.one with
              | Gt => Qq (Z_of_N d) (Zabs_N n)
              | _ => Qz (Z_of_N d)
            end
          | Gt =>
-           match Z.compare n Z.minus_one with
-             | Lt => Qq (Z.opp (Z_of_N d)) (Zabs_N n)
-             | _ => Qz (Z.opp (Z_of_N d))
+           match ZZ.compare n ZZ.minus_one with
+             | Lt => Qq (ZZ.opp (Z_of_N d)) (Zabs_N n)
+             | _ => Qz (ZZ.opp (Z_of_N d))
            end
        end
    end.
@@ -807,7 +807,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  destruct x as [ z | n d ].
  (* Qz z *)
  simpl.
- rewrite Z.spec_compare; destr_zcompare; auto with qarith.
+ rewrite ZZ.spec_compare; destr_zcompare; auto with qarith.
  (* Qq n d *)
  simpl; nzsimpl; destr_eqb.
  destr_zcompare; simpl; auto with qarith.
@@ -818,12 +818,12 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  (* 0 < n *)
  destr_zcompare; auto with qarith.
  destr_zcompare; nzsimpl; simpl; auto with qarith; intros.
- destr_eqb; nzsimpl; [ intros; rewrite Zabs_eq in *; romega | intros _ ].
+ destr_eqb; nzsimpl; [ intros; rewrite Z.abs_eq in *; romega | intros _ ].
  rewrite H0; auto with qarith.
  romega.
  (* 0 > n *)
  destr_zcompare; nzsimpl; simpl; auto with qarith.
- destr_eqb; nzsimpl; [ intros; rewrite Zabs_non_eq in *; romega | intros _ ].
+ destr_eqb; nzsimpl; [ intros; rewrite Z.abs_neq in *; romega | intros _ ].
  rewrite H0; auto with qarith.
  romega.
  Qed.
@@ -847,36 +847,36 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  (* 0 < n *)
  destr_zcompare; simpl; nzsimpl; auto.
  destr_eqb; nzsimpl; simpl; auto.
- rewrite Zabs_eq; romega.
+ rewrite Z.abs_eq; romega.
  intros _.
  rewrite strong_spec_norm; simpl; nzsimpl.
  destr_eqb; nzsimpl.
- rewrite Zabs_eq; romega.
+ rewrite Z.abs_eq; romega.
  intros _.
  rewrite Qred_iff.
  simpl.
- rewrite Zabs_eq; auto with zarith.
- rewrite Z2P_correct in *; auto.
- rewrite Zgcd_comm; auto.
+ rewrite Z.abs_eq; auto with zarith.
+ rewrite Z2Pos.id in *; auto.
+ rewrite Z.gcd_comm; auto.
  (* 0 > n *)
  destr_eqb; nzsimpl; simpl; auto; intros.
  destr_zcompare; simpl; nzsimpl; auto.
  destr_eqb; nzsimpl.
- rewrite Zabs_non_eq; romega.
+ rewrite Z.abs_neq; romega.
  intros _.
  rewrite strong_spec_norm; simpl; nzsimpl.
  destr_eqb; nzsimpl.
- rewrite Zabs_non_eq; romega.
+ rewrite Z.abs_neq; romega.
  intros _.
  rewrite Qred_iff.
  simpl.
- rewrite Z2P_correct in *; auto.
+ rewrite Z2Pos.id in *; auto.
  intros.
- rewrite Zgcd_comm, Zgcd_Zabs, Zgcd_comm.
+ rewrite Z.gcd_comm, Z.gcd_abs_l, Z.gcd_comm.
  apply Zis_gcd_gcd; auto with zarith.
  apply Zis_gcd_minus.
- rewrite Zopp_involutive, <- H1; apply Zgcd_is_gcd.
- rewrite Zabs_non_eq; romega.
+ rewrite Z.opp_involutive, <- H1; apply Zgcd_is_gcd.
+ rewrite Z.abs_neq; romega.
  Qed.
 
  Definition div x y := mul x (inv y).
@@ -909,31 +909,30 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Definition square (x: t): t :=
   match x with
-  | Qz zx => Qz (Z.square zx)
-  | Qq nx dx => Qq (Z.square nx) (N.square dx)
+  | Qz zx => Qz (ZZ.square zx)
+  | Qq nx dx => Qq (ZZ.square nx) (NN.square dx)
   end.
 
  Theorem spec_square : forall x, [square x] == [x] ^ 2.
  Proof.
  destruct x as [ z | n d ].
- simpl; rewrite Z.spec_square; red; auto.
+ simpl; rewrite ZZ.spec_square; red; auto.
  simpl.
  destr_eqb; nzsimpl; intros.
  apply Qeq_refl.
- rewrite N.spec_square in *; nzsimpl.
- match goal with E : (_ * _ = 0)%Z |- _ =>
-  elim (Zmult_integral _ _ E); romega end.
- rewrite N.spec_square in *; nzsimpl; nsubst; romega.
- rewrite Z.spec_square, N.spec_square.
+ rewrite NN.spec_square in *; nzsimpl.
+ rewrite Z.mul_eq_0 in *; romega.
+ rewrite NN.spec_square in *; nzsimpl; nsubst; romega.
+ rewrite ZZ.spec_square, NN.spec_square.
  red; simpl.
- rewrite Zpos_mult_morphism; rewrite !Z2P_correct; auto.
- apply Zmult_lt_0_compat; auto.
+ rewrite Pos2Z.inj_mul; rewrite !Z2Pos.id; auto.
+ apply Z.mul_pos_pos; auto.
  Qed.
 
  Definition power_pos (x : t) p : t :=
   match x with
-  | Qz zx => Qz (Z.pow_pos zx p)
-  | Qq nx dx => Qq (Z.pow_pos nx p) (N.pow_pos dx p)
+  | Qz zx => Qz (ZZ.pow_pos zx p)
+  | Qq nx dx => Qq (ZZ.pow_pos nx p) (NN.pow_pos dx p)
   end.
 
  Theorem spec_power_pos : forall x p, [power_pos x p] == [x] ^ Zpos p.
@@ -941,26 +940,26 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  intros [ z | n d ] p; unfold power_pos.
  (* Qz *)
  simpl.
- rewrite Z.spec_pow_pos.
- rewrite Qpower_decomp.
+ rewrite ZZ.spec_pow_pos, Qpower_decomp.
  red; simpl; f_equal.
- rewrite Zpower_pos_1_l; auto.
+ now rewrite Pos2Z.inj_pow, Z.pow_1_l.
  (* Qq *)
  simpl.
- rewrite Z.spec_pow_pos.
+ rewrite ZZ.spec_pow_pos.
  destr_eqb; nzsimpl; intros.
- apply Qeq_sym; apply Qpower_positive_0.
- rewrite N.spec_pow_pos in *.
- assert (0 < N.to_Z d ^ ' p)%Z by
-  (apply Zpower_gt_0; auto with zarith).
- romega.
- exfalso.
- rewrite N.spec_pow_pos in *. nsubst.
- rewrite Zpower_0_l in *; [romega|discriminate].
- rewrite Qpower_decomp.
- red; simpl; do 3 f_equal.
- rewrite Z2P_correct by (generalize (N.spec_pos d); romega).
- rewrite N.spec_pow_pos. auto.
+ - apply Qeq_sym; apply Qpower_positive_0.
+ - rewrite NN.spec_pow_pos in *.
+   assert (0 < NN.to_Z d ^ ' p)%Z by
+    (apply Z.pow_pos_nonneg; auto with zarith).
+   romega.
+ - exfalso.
+   rewrite NN.spec_pow_pos in *. nsubst.
+   rewrite Z.pow_0_l' in *; [romega|discriminate].
+ - rewrite Qpower_decomp.
+   red; simpl; do 3 f_equal.
+   apply Pos2Z.inj. rewrite Pos2Z.inj_pow.
+   rewrite 2 Z2Pos.id by (generalize (NN.spec_pos d); romega).
+   now rewrite NN.spec_pow_pos.
  Qed.
 
  Instance strong_spec_power_pos x p `(Reduced x) : Reduced (power_pos x p).
@@ -976,10 +975,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  unfold Reduced; rewrite strong_spec_red, Qred_iff; simpl.
  destr_eqb; nzsimpl; simpl; intros.
  exfalso.
- rewrite N.spec_pow_pos in *. nsubst.
- rewrite Zpower_0_l in *; [romega|discriminate].
- rewrite Z2P_correct in *; auto.
- rewrite N.spec_pow_pos, Z.spec_pow_pos; auto.
+ rewrite NN.spec_pow_pos in *. nsubst.
+ rewrite Z.pow_0_l' in *; [romega|discriminate].
+ rewrite Z2Pos.id in *; auto.
+ rewrite NN.spec_pow_pos, ZZ.spec_pow_pos; auto.
  rewrite Zgcd_1_rel_prime in *.
  apply rel_prime_Zpower; auto with zarith.
  Qed.
@@ -1086,7 +1085,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
   [[add x y]] = [[x]] + [[y]].
  Proof.
  unfold to_Qc.
- apply trans_equal with (!! ([x] + [y])).
+ transitivity (!! ([x] + [y])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
  apply Qred_complete; apply spec_add; auto.
@@ -1100,7 +1099,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
   [[add_norm x y]] = [[x]] + [[y]].
  Proof.
  unfold to_Qc.
- apply trans_equal with (!! ([x] + [y])).
+ transitivity (!! ([x] + [y])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
  apply Qred_complete; apply spec_add_norm; auto.
@@ -1148,7 +1147,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
   [[mul x y]] = [[x]] * [[y]].
  Proof.
  unfold to_Qc.
- apply trans_equal with (!! ([x] * [y])).
+ transitivity (!! ([x] * [y])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
  apply Qred_complete; apply spec_mul; auto.
@@ -1162,7 +1161,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
    [[mul_norm x y]] = [[x]] * [[y]].
  Proof.
  unfold to_Qc.
- apply trans_equal with (!! ([x] * [y])).
+ transitivity (!! ([x] * [y])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
  apply Qred_complete; apply spec_mul_norm; auto.
@@ -1186,7 +1185,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
    [[inv x]] =  /[[x]].
  Proof.
  unfold to_Qc.
- apply trans_equal with (!! (/[x])).
+ transitivity (!! (/[x])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
  apply Qred_complete; apply spec_inv; auto.
@@ -1200,7 +1199,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
    [[inv_norm x]] =  /[[x]].
  Proof.
  unfold to_Qc.
- apply trans_equal with (!! (/[x])).
+ transitivity (!! (/[x])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
  apply Qred_complete; apply spec_inv_norm; auto.
@@ -1248,7 +1247,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_squarec x: [[square x]] = [[x]]^2.
  Proof.
  unfold to_Qc.
- apply trans_equal with (!! ([x]^2)).
+ transitivity (!! ([x]^2)).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
  apply Qred_complete; apply spec_square; auto.
@@ -1262,24 +1261,24 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Qed.
 
  Theorem spec_power_posc x p:
-   [[power_pos x p]] = [[x]] ^ nat_of_P p.
+   [[power_pos x p]] = [[x]] ^ Pos.to_nat p.
  Proof.
  unfold to_Qc.
- apply trans_equal with (!! ([x]^Zpos p)).
+ transitivity (!! ([x]^Zpos p)).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
  apply Qred_complete; apply spec_power_pos; auto.
- induction p using Pind.
+ induction p using Pos.peano_ind.
  simpl; ring.
- rewrite Psucc_S; simpl Qcpower.
+ rewrite Pos2Nat.inj_succ; simpl Qcpower.
  rewrite <- IHp; clear IHp.
  unfold Qcmult, Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
  apply Qred_complete.
- setoid_replace ([x] ^ ' Psucc p)%Q with ([x] * [x] ^ ' p)%Q.
+ setoid_replace ([x] ^ ' Pos.succ p)%Q with ([x] * [x] ^ ' p)%Q.
  apply Qmult_comp; apply Qeq_sym; apply Qred_correct.
  simpl.
- rewrite Pplus_one_succ_l.
+ rewrite <- Pos.add_1_l.
  rewrite Qpower_plus_positive; simpl; apply Qeq_refl.
  Qed.
 
-- 
cgit v1.2.3