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

7 files changed, 236 insertions, 335 deletions

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 94ea4906c..7f70d6efd 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -20,7 +20,7 @@ Delimit Scope Q_scope with Q.
 Bind Scope Q_scope with Q.
 Arguments Qmake _%Z _%positive.
 Open Scope Q_scope.
-Ltac simpl_mult := repeat rewrite Zpos_mult_morphism.
+Ltac simpl_mult := rewrite ?Pos2Z.inj_mul.
 
 (** [a#b] denotes the fraction [a] over [b]. *)
 
@@ -58,79 +58,65 @@ Qed.
 Definition Qcompare (p q : Q) := (Qnum p * QDen q ?= Qnum q * QDen p)%Z.
 Notation "p ?= q" := (Qcompare p q) : Q_scope.
 
-Lemma Qeq_alt : forall p q, (p == q) <-> (p ?= q) = Eq.
+Lemma Qeq_alt p q : (p == q) <-> (p ?= q) = Eq.
 Proof.
-unfold Qeq, Qcompare; intros; split; intros.
-rewrite H; apply Zcompare_refl.
-apply Zcompare_Eq_eq; auto.
+symmetry. apply Z.compare_eq_iff.
 Qed.
 
-Lemma Qlt_alt : forall p q, (p<q) <-> (p?=q = Lt).
+Lemma Qlt_alt p q : (p<q) <-> (p?=q = Lt).
 Proof.
-unfold Qlt, Qcompare, Zlt; split; auto.
+reflexivity.
 Qed.
 
-Lemma Qgt_alt : forall p q, (p>q) <-> (p?=q = Gt).
+Lemma Qgt_alt p q : (p>q) <-> (p?=q = Gt).
 Proof.
-unfold Qlt, Qcompare, Zlt.
-intros; rewrite Zcompare_Gt_Lt_antisym; split; auto.
+symmetry. apply Z.gt_lt_iff.
 Qed.
 
-Lemma Qle_alt : forall p q, (p<=q) <-> (p?=q <> Gt).
+Lemma Qle_alt p q : (p<=q) <-> (p?=q <> Gt).
 Proof.
-unfold Qle, Qcompare, Zle; split; auto.
+reflexivity.
 Qed.
 
-Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt).
+Lemma Qge_alt p q : (p>=q) <-> (p?=q <> Lt).
 Proof.
-unfold Qle, Qcompare, Zle.
-split; intros; contradict H.
-rewrite Zcompare_Gt_Lt_antisym; auto.
-rewrite Zcompare_Gt_Lt_antisym in H; auto.
+symmetry. apply Z.ge_le_iff.
 Qed.
 
 Hint Unfold Qeq Qlt Qle : qarith.
 Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith.
 
-Lemma Qcompare_antisym : forall x y, CompOpp (x ?= y) = (y ?= x).
+Lemma Qcompare_antisym x y : CompOpp (x ?= y) = (y ?= x).
 Proof.
- unfold "?=". intros. apply Zcompare_antisym.
+ symmetry. apply Z.compare_antisym.
 Qed.
 
-Lemma Qcompare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (x ?= y).
+Lemma Qcompare_spec x y : CompareSpec (x==y) (x<y) (y<x) (x ?= y).
 Proof.
- intros.
- destruct (x ?= y) as [ ]_eqn:H; constructor; auto.
- rewrite Qeq_alt; auto.
- rewrite Qlt_alt, <- Qcompare_antisym, H; auto.
+ unfold Qeq, Qlt, Qcompare. case Z.compare_spec; now constructor.
 Qed.
 
 (** * Properties of equality. *)
 
-Theorem Qeq_refl : forall x, x == x.
+Theorem Qeq_refl x : x == x.
 Proof.
  auto with qarith.
 Qed.
 
-Theorem Qeq_sym : forall x y, x == y -> y == x.
+Theorem Qeq_sym x y : x == y -> y == x.
 Proof.
  auto with qarith.
 Qed.
 
-Theorem Qeq_trans : forall x y z, x == y -> y == z -> x == z.
+Theorem Qeq_trans x y z : x == y -> y == z -> x == z.
 Proof.
-unfold Qeq; intros.
-apply Zmult_reg_l with (QDen y).
-auto with qarith.
-transitivity (Qnum x * QDen y * QDen z)%Z; try ring.
-rewrite H.
-transitivity (Qnum y * QDen z * QDen x)%Z; try ring.
-rewrite H0; ring.
+unfold Qeq; intros XY YZ.
+apply Z.mul_reg_r with (QDen y); [auto with qarith|].
+now rewrite Z.mul_shuffle0, XY, Z.mul_shuffle0, YZ, Z.mul_shuffle0.
 Qed.
 
-Hint Resolve Qeq_refl : qarith.
-Hint Resolve Qeq_sym : qarith.
-Hint Resolve Qeq_trans : qarith.
+Hint Immediate Qeq_sym : qarith.
+Hint Resolve Qeq_refl Qeq_trans : qarith.
 
 (** In a word, [Qeq] is a setoid equality. *)
 
@@ -139,50 +125,48 @@ Proof. split; red; eauto with qarith. Qed.
 
 (** Furthermore, this equality is decidable: *)
 
-Theorem Qeq_dec : forall x y, {x==y} + {~ x==y}.
+Theorem Qeq_dec x y : {x==y} + {~ x==y}.
 Proof.
- intros; case (Z_eq_dec (Qnum x * QDen y) (Qnum y * QDen x)); auto.
+ apply Z.eq_dec.
 Defined.
 
 Definition Qeq_bool x y :=
   (Zeq_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z.
 
 Definition Qle_bool x y :=
-  (Zle_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z.
+  (Z.leb (Qnum x * QDen y) (Qnum y * QDen x))%Z.
 
-Lemma Qeq_bool_iff : forall x y, Qeq_bool x y = true <-> x == y.
+Lemma Qeq_bool_iff x y : Qeq_bool x y = true <-> x == y.
 Proof.
-  unfold Qeq_bool, Qeq; intros.
   symmetry; apply Zeq_is_eq_bool.
 Qed.
 
-Lemma Qeq_bool_eq : forall x y, Qeq_bool x y = true -> x == y.
+Lemma Qeq_bool_eq x y : Qeq_bool x y = true -> x == y.
 Proof.
-  intros; rewrite <- Qeq_bool_iff; auto.
+  apply Qeq_bool_iff.
 Qed.
 
-Lemma Qeq_eq_bool : forall x y, x == y -> Qeq_bool x y = true.
+Lemma Qeq_eq_bool x y : x == y -> Qeq_bool x y = true.
 Proof.
-  intros; rewrite Qeq_bool_iff; auto.
+  apply Qeq_bool_iff.
 Qed.
 
-Lemma Qeq_bool_neq : forall x y, Qeq_bool x y = false -> ~ x == y.
+Lemma Qeq_bool_neq x y : Qeq_bool x y = false -> ~ x == y.
 Proof.
-  intros x y H; rewrite <- Qeq_bool_iff, H; discriminate.
+  rewrite <- Qeq_bool_iff. now intros ->.
 Qed.
 
-Lemma Qle_bool_iff : forall x y, Qle_bool x y = true <-> x <= y.
+Lemma Qle_bool_iff x y : Qle_bool x y = true <-> x <= y.
 Proof.
-  unfold Qle_bool, Qle; intros.
   symmetry; apply Zle_is_le_bool.
 Qed.
 
-Lemma Qle_bool_imp_le : forall x y, Qle_bool x y = true -> x <= y.
+Lemma Qle_bool_imp_le x y : Qle_bool x y = true -> x <= y.
 Proof.
-  intros; rewrite <- Qle_bool_iff; auto.
+  apply Qle_bool_iff.
 Qed.
 
-Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x.
+Theorem Qnot_eq_sym x y : ~x == y -> ~y == x.
 Proof.
  auto with qarith.
 Qed.
@@ -223,12 +207,9 @@ Infix "/" := Qdiv : Q_scope.
 
 Notation " ' x " := (Zpos x) (at level 20, no associativity) : Z_scope.
 
-Lemma Qmake_Qdiv : forall a b, a#b==inject_Z a/inject_Z ('b).
+Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z ('b).
 Proof.
-intros a b.
-unfold Qeq.
-simpl.
-ring.
+unfold Qeq. simpl. ring.
 Qed.
 
 (** * Setoid compatibility results *)
@@ -281,17 +262,13 @@ Instance Qinv_comp : Proper (Qeq==>Qeq) Qinv.
 Proof.
   unfold Qeq, Qinv; simpl.
   Open Scope Z_scope.
-  intros (p1, p2) (q1, q2); simpl.
-  case p1; simpl.
-  intros.
-  assert (q1 = 0).
-  elim (Zmult_integral q1 ('p2)); auto with zarith.
-  intros; discriminate.
-  subst; auto.
-  case q1; simpl; intros; try discriminate.
-  rewrite (Pmult_comm p2 p); rewrite (Pmult_comm q2 p0); auto.
-  case q1; simpl; intros; try discriminate.
-  rewrite (Pmult_comm p2 p); rewrite (Pmult_comm q2 p0); auto.
+  intros (p1, p2) (q1, q2) EQ; simpl in *.
+  destruct q1; simpl in *.
+  - apply Z.mul_eq_0 in EQ. destruct EQ; now subst.
+  - destruct p1; simpl in *; try discriminate.
+    now rewrite Pos.mul_comm, <- EQ, Pos.mul_comm.
+  - destruct p1; simpl in *; try discriminate.
+    now rewrite Pos.mul_comm, <- EQ, Pos.mul_comm.
   Close Scope Z_scope.
 Qed.
 
@@ -368,7 +345,7 @@ Qed.
 Lemma Qplus_0_r : forall x, x+0 == x.
 Proof.
   intros (x1, x2); unfold Qeq, Qplus; simpl.
-  rewrite Pmult_comm; simpl; ring.
+  rewrite Pos.mul_comm; simpl; ring.
 Qed.
 
 (** Commutativity of addition: *)
@@ -376,7 +353,7 @@ Qed.
 Theorem Qplus_comm : forall x y, x+y == y+x.
 Proof.
   intros (x1, x2); unfold Qeq, Qplus; simpl.
-  intros; rewrite Pmult_comm; ring.
+  intros; rewrite Pos.mul_comm; ring.
 Qed.
 
 
@@ -419,7 +396,7 @@ Qed.
 
 Theorem Qmult_assoc : forall n m p, n*(m*p)==(n*m)*p.
 Proof.
-  intros; red; simpl; rewrite Pmult_assoc; ring.
+  intros; red; simpl; rewrite Pos.mul_assoc; ring.
 Qed.
 
 (** multiplication and zero *)
@@ -444,15 +421,15 @@ Qed.
 Theorem Qmult_1_r : forall n, n*1==n.
 Proof.
   intro; red; simpl.
-  rewrite Zmult_1_r with (n := Qnum n).
-  rewrite Pmult_comm; simpl; trivial.
+  rewrite Z.mul_1_r with (n := Qnum n).
+  rewrite Pos.mul_comm; simpl; trivial.
 Qed.
 
 (** Commutativity of multiplication *)
 
 Theorem Qmult_comm : forall x y, x*y==y*x.
 Proof.
-  intros; red; simpl; rewrite Pmult_comm; ring.
+  intros; red; simpl; rewrite Pos.mul_comm; ring.
 Qed.
 
 (** Distributivity over [Qadd] *)
@@ -474,17 +451,15 @@ Qed.
 Theorem Qmult_integral : forall x y, x*y==0 -> x==0 \/ y==0.
 Proof.
   intros (x1,x2) (y1,y2).
-  unfold Qeq, Qmult; simpl; intros.
-  destruct (Zmult_integral (x1*1)%Z (y1*1)%Z); auto.
-  rewrite <- H; ring.
+  unfold Qeq, Qmult; simpl.
+  now rewrite <- Z.mul_eq_0, !Z.mul_1_r.
 Qed.
 
 Theorem Qmult_integral_l : forall x y, ~ x == 0 -> x*y == 0 -> y == 0.
 Proof.
   intros (x1, x2) (y1, y2).
-  unfold Qeq, Qmult; simpl; intros.
-  apply Zmult_integral_l with x1; auto with zarith.
-  rewrite <- H0; ring.
+  unfold Qeq, Qmult; simpl.
+  rewrite !Z.mul_1_r, Z.mul_eq_0. intuition.
 Qed.
 
 
@@ -561,12 +536,12 @@ Qed.
 
 (** * Properties of order upon Q. *)
 
-Lemma Qle_refl : forall x, x<=x.
+Lemma Qle_refl x : x<=x.
 Proof.
   unfold Qle; auto with zarith.
 Qed.
 
-Lemma Qle_antisym : forall x y, x<=y -> y<=x -> x==y.
+Lemma Qle_antisym x y : x<=y -> y<=x -> x==y.
 Proof.
   unfold Qle, Qeq; auto with zarith.
 Qed.
@@ -575,52 +550,46 @@ Lemma Qle_trans : forall x y z, x<=y -> y<=z -> x<=z.
 Proof.
   unfold Qle; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros.
   Open Scope Z_scope.
-  apply Zmult_le_reg_r with ('y2).
-  red; trivial.
-  apply Zle_trans with (y1 * 'x2 * 'z2).
-  replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring.
-  apply Zmult_le_compat_r; auto with zarith.
-  replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring.
-  replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring.
-  apply Zmult_le_compat_r; auto with zarith.
+  apply Z.mul_le_mono_pos_r with ('y2); [easy|].
+  apply Z.le_trans with (y1 * 'x2 * 'z2).
+  - rewrite Z.mul_shuffle0. now apply Z.mul_le_mono_pos_r.
+  - rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1).
+    now apply Z.mul_le_mono_pos_r.
   Close Scope Z_scope.
 Qed.
 
 Hint Resolve Qle_trans : qarith.
 
-Lemma Qlt_irrefl : forall x, ~x<x.
+Lemma Qlt_irrefl x : ~x<x.
 Proof.
  unfold Qlt. auto with zarith.
 Qed.
 
-Lemma Qlt_not_eq : forall x y, x<y -> ~ x==y.
+Lemma Qlt_not_eq x y : x<y -> ~ x==y.
 Proof.
   unfold Qlt, Qeq; auto with zarith.
 Qed.
 
 Lemma Zle_Qle (x y: Z): (x <= y)%Z = (inject_Z x <= inject_Z y).
 Proof.
- unfold Qle. intros. simpl.
- do 2 rewrite Zmult_1_r. reflexivity.
+ unfold Qle. simpl. now rewrite !Z.mul_1_r.
 Qed.
 
 Lemma Zlt_Qlt (x y: Z): (x < y)%Z = (inject_Z x < inject_Z y).
 Proof.
- unfold Qlt. intros. simpl.
- do 2 rewrite Zmult_1_r. reflexivity.
+ unfold Qlt. simpl. now rewrite !Z.mul_1_r.
 Qed.
 
 
 (** Large = strict or equal *)
 
-Lemma Qle_lteq : forall x y, x<=y <-> x<y \/ x==y.
+Lemma Qle_lteq x y : x<=y <-> x<y \/ x==y.
 Proof.
- intros.
  rewrite Qeq_alt, Qle_alt, Qlt_alt.
  destruct (x ?= y); intuition; discriminate.
 Qed.
 
-Lemma Qlt_le_weak : forall x y, x<y -> x<=y.
+Lemma Qlt_le_weak x y : x<y -> x<=y.
 Proof.
   unfold Qle, Qlt; auto with zarith.
 Qed.
@@ -629,15 +598,11 @@ Lemma Qle_lt_trans : forall x y z, x<=y -> y<z -> x<z.
 Proof.
   unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros.
   Open Scope Z_scope.
-  apply Zgt_lt.
-  apply Zmult_gt_reg_r with ('y2).
-  red; trivial.
-  apply Zgt_le_trans with (y1 * 'x2 * 'z2).
-  replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring.
-  replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring.
-  apply Zmult_gt_compat_r; auto with zarith.
-  replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring.
-  apply Zmult_le_compat_r; auto with zarith.
+  apply Z.mul_lt_mono_pos_r with ('y2); [easy|].
+  apply Z.le_lt_trans with (y1 * 'x2 * 'z2).
+  - rewrite Z.mul_shuffle0. now apply Z.mul_le_mono_pos_r.
+  - rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1).
+    now apply Z.mul_lt_mono_pos_r.
   Close Scope Z_scope.
 Qed.
 
@@ -645,15 +610,11 @@ Lemma Qlt_le_trans : forall x y z, x<y -> y<=z -> x<z.
 Proof.
   unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros.
   Open Scope Z_scope.
-  apply Zgt_lt.
-  apply Zmult_gt_reg_r with ('y2).
-  red; trivial.
-  apply Zle_gt_trans with (y1 * 'x2 * 'z2).
-  replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring.
-  replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring.
-  apply Zmult_le_compat_r; auto with zarith.
-  replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring.
-  apply Zmult_gt_compat_r; auto with zarith.
+  apply Z.mul_lt_mono_pos_r with ('y2); [easy|].
+  apply Z.lt_le_trans with (y1 * 'x2 * 'z2).
+  - rewrite Z.mul_shuffle0. now apply Z.mul_lt_mono_pos_r.
+  - rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1).
+    now apply Z.mul_le_mono_pos_r.
   Close Scope Z_scope.
 Qed.
 
@@ -688,7 +649,7 @@ Qed.
 
 Lemma Qle_lt_or_eq : forall x y, x<=y -> x<y \/ x==y.
 Proof.
-  unfold Qle, Qlt, Qeq; intros; apply Zle_lt_or_eq; auto.
+  unfold Qle, Qlt, Qeq; intros; now apply Z.lt_eq_cases.
 Qed.
 
 Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le
@@ -713,7 +674,7 @@ Defined.
 Lemma Qopp_le_compat : forall p q, p<=q -> -q <= -p.
 Proof.
   intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl.
-  do 2 rewrite <- Zopp_mult_distr_l; omega.
+  rewrite !Z.mul_opp_l. omega.
 Qed.
 
 Hint Resolve Qopp_le_compat : qarith.
@@ -721,15 +682,13 @@ Hint Resolve Qopp_le_compat : qarith.
 Lemma Qle_minus_iff : forall p q, p <= q <-> 0 <= q+-p.
 Proof.
   intros (x1,x2) (y1,y2); unfold Qle; simpl.
-  rewrite <- Zopp_mult_distr_l.
-  split; omega.
+  rewrite Z.mul_opp_l. omega.
 Qed.
 
 Lemma Qlt_minus_iff : forall p q, p < q <-> 0 < q+-p.
 Proof.
   intros (x1,x2) (y1,y2); unfold Qlt; simpl.
-  rewrite <- Zopp_mult_distr_l.
-  split; omega.
+  rewrite Z.mul_opp_l. omega.
 Qed.
 
 Lemma Qplus_le_compat :
@@ -740,8 +699,8 @@ Proof.
   Open Scope Z_scope.
   intros.
   match goal with |- ?a <= ?b => ring_simplify a b end.
-  rewrite Zplus_comm.
-  apply Zplus_le_compat.
+  rewrite Z.add_comm.
+  apply Z.add_le_mono.
   match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end.
   auto with zarith.
   match goal with |- ?a <= ?b => ring_simplify x1 y1 ('x2) ('y2) a b end.
@@ -757,13 +716,12 @@ Proof.
   Open Scope Z_scope.
   intros.
   match goal with |- ?a < ?b => ring_simplify a b end.
-  rewrite Zplus_comm.
-  apply Zplus_le_lt_compat.
+  rewrite Z.add_comm.
+  apply Z.add_le_lt_mono.
   match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end.
   auto with zarith.
   match goal with |- ?a < ?b => ring_simplify x1 y1 ('x2) ('y2) a b end.
-  assert (forall p, 0 < ' p) by reflexivity.
-  repeat (apply Zmult_lt_compat_r; auto).
+  do 2 (apply Z.mul_lt_mono_pos_r;try easy).
   Close Scope Z_scope.
 Qed.
 
@@ -802,20 +760,20 @@ Proof.
   intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl.
   Open Scope Z_scope.
   intros; simpl_mult.
-  replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring.
-  replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring.
-  apply Zmult_le_compat_r; auto with zarith.
+  rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1).
+  apply Z.mul_le_mono_nonneg_r; auto with zarith.
   Close Scope Z_scope.
 Qed.
 
-Lemma Qmult_lt_0_le_reg_r : forall x y z, 0 <  z  -> x*z <= y*z -> x <= y.
+Lemma Qmult_lt_0_le_reg_r : forall x y z, 0 < z  -> x*z <= y*z -> x <= y.
 Proof.
   intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl.
   Open Scope Z_scope.
   simpl_mult.
-  replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring.
-  replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring.
-  intros; apply Zmult_le_reg_r with (c1*'c2); auto with zarith.
+  rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1).
+  intros LT LE.
+  apply Z.mul_le_mono_pos_r in LE; trivial.
+  apply Z.mul_pos_pos; [omega|easy].
   Close Scope Z_scope.
 Qed.
 
@@ -837,12 +795,9 @@ Proof.
   intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl.
   Open Scope Z_scope.
   intros; simpl_mult.
-  replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring.
-  replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring.
-  apply Zmult_lt_compat_r; auto with zarith.
-  apply Zmult_lt_0_compat.
-  omega.
-  compute; auto.
+  rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1).
+  apply Z.mul_lt_mono_pos_r; auto with zarith.
+  apply Z.mul_pos_pos; [omega|reflexivity].
   Close Scope Z_scope.
 Qed.
 
@@ -852,15 +807,9 @@ Proof.
  intros (a1,a2) (b1,b2) (c1,c2).
  unfold Qle, Qlt; simpl.
  simpl_mult.
- replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring.
- replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring.
- assert (forall p, 0 < ' p) by reflexivity.
- split; intros.
-  apply Zmult_lt_reg_r with (c1*'c2); auto with zarith.
-  apply Zmult_lt_0_compat; auto with zarith.
- apply Zmult_lt_compat_r; auto with zarith.
- apply Zmult_lt_0_compat. omega.
- compute; auto.
+ rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1).
+ intro LT. rewrite <- Z.mul_lt_mono_pos_r. reflexivity.
+ apply Z.mul_pos_pos; [omega|reflexivity].
  Close Scope Z_scope.
 Qed.
 
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v
index 557fabc89..5ae668b05 100644
--- a/theories/QArith/Qabs.v
+++ b/theories/QArith/Qabs.v
@@ -11,7 +11,7 @@ Require Export Qreduction.
 
 Hint Resolve Qlt_le_weak : qarith.
 
-Definition Qabs (x:Q) := let (n,d):=x in (Zabs n#d).
+Definition Qabs (x:Q) := let (n,d):=x in (Z.abs n#d).
 
 Lemma Qabs_case : forall (x:Q) (P : Q -> Type), (0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P (Qabs x).
 Proof.
@@ -26,9 +26,9 @@ intros [xn xd] [yn yd] H.
 simpl.
 unfold Qeq in *.
 simpl in *.
-change (' yd)%Z with (Zabs (' yd)).
-change (' xd)%Z with (Zabs (' xd)).
-repeat rewrite <- Zabs_Zmult.
+change (' yd)%Z with (Z.abs (' yd)).
+change (' xd)%Z with (Z.abs (' xd)).
+repeat rewrite <- Z.abs_mul.
 congruence.
 Qed.
 
@@ -61,7 +61,7 @@ auto.
 apply (Qopp_le_compat x 0).
 Qed.
 
-Lemma Zabs_Qabs : forall n d, (Zabs n#d)==Qabs (n#d).
+Lemma Zabs_Qabs : forall n d, (Z.abs n#d)==Qabs (n#d).
 Proof.
 intros [|n|n]; reflexivity.
 Qed.
@@ -85,25 +85,25 @@ intros [xn xd] [yn yd].
 unfold Qplus.
 unfold Qle.
 simpl.
-apply Zmult_le_compat_r;auto with *.
-change (' yd)%Z with (Zabs (' yd)).
-change (' xd)%Z with (Zabs (' xd)).
-repeat rewrite <- Zabs_Zmult.
-apply Zabs_triangle.
+apply Z.mul_le_mono_nonneg_r;auto with *.
+change (' yd)%Z with (Z.abs (' yd)).
+change (' xd)%Z with (Z.abs (' xd)).
+repeat rewrite <- Z.abs_mul.
+apply Z.abs_triangle.
 Qed.
 
 Lemma Qabs_Qmult : forall a b, Qabs (a*b) == (Qabs a)*(Qabs b).
 Proof.
 intros [an ad] [bn bd].
 simpl.
-rewrite Zabs_Zmult.
+rewrite Z.abs_mul.
 reflexivity.
 Qed.
 
 Lemma Qabs_Qminus x y: Qabs (x - y) = Qabs (y - x).
 Proof.
  unfold Qminus, Qopp. simpl.
- rewrite Pmult_comm, <- Zabs_Zopp.
+ rewrite Pos.mul_comm, <- Z.abs_opp.
  do 2 f_equal. ring.
 Qed.
 
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index fea2ba398..05a27cc43 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -22,39 +22,39 @@ Arguments Qcmake this%Q _.
 Open Scope Qc_scope.
 
 Lemma Qred_identity :
-  forall q:Q, Zgcd (Qnum q) (QDen q) = 1%Z -> Qred q = q.
+  forall q:Q, Z.gcd (Qnum q) (QDen q) = 1%Z -> Qred q = q.
 Proof.
   unfold Qred; intros (a,b); simpl.
-  generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)).
+  generalize (Z.ggcd_gcd a ('b)) (Z.ggcd_correct_divisors a ('b)).
   intros.
   rewrite H1 in H; clear H1.
-  destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst.
+  destruct (Z.ggcd a ('b)) as (g,(aa,bb)); simpl in *; subst.
   destruct H0.
-  rewrite Zmult_1_l in H, H0.
+  rewrite Z.mul_1_l in H, H0.
   subst; simpl; auto.
 Qed.
 
 Lemma Qred_identity2 :
-  forall q:Q, Qred q = q -> Zgcd (Qnum q) (QDen q) = 1%Z.
+  forall q:Q, Qred q = q -> Z.gcd (Qnum q) (QDen q) = 1%Z.
 Proof.
   unfold Qred; intros (a,b); simpl.
-  generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)) (Zgcd_is_pos a ('b)).
+  generalize (Z.ggcd_gcd a ('b)) (Z.ggcd_correct_divisors a ('b)) (Z.gcd_nonneg a ('b)).
   intros.
   rewrite <- H; rewrite <- H in H1; clear H.
-  destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst.
+  destruct (Z.ggcd a ('b)) as (g,(aa,bb)); simpl in *; subst.
   injection H2; intros; clear H2.
   destruct H0.
   clear H0 H3.
   destruct g as [|g|g]; destruct bb as [|bb|bb]; simpl in *; try discriminate.
   f_equal.
-  apply Pmult_reg_r with bb.
+  apply Pos.mul_reg_r with bb.
   injection H2; intros.
   rewrite <- H0.
   rewrite H; simpl; auto.
   elim H1; auto.
 Qed.
 
-Lemma Qred_iff : forall q:Q, Qred q = q <-> Zgcd (Qnum q) (QDen q) = 1%Z.
+Lemma Qred_iff : forall q:Q, Qred q = q <-> Z.gcd (Qnum q) (QDen q) = 1%Z.
 Proof.
   split; intros.
   apply Qred_identity2; auto.
diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v
index 5e27f3814..811bfb6df 100644
--- a/theories/QArith/Qfield.v
+++ b/theories/QArith/Qfield.v
@@ -38,7 +38,7 @@ Proof.
   exact Hp.
 Qed.
 
-Lemma Qpower_theory : power_theory 1 Qmult Qeq Z_of_N Qpower.
+Lemma Qpower_theory : power_theory 1 Qmult Qeq Z.of_N Qpower.
 Proof.
 constructor.
 intros r [|n];
@@ -66,7 +66,7 @@ Ltac Qpow_tac t :=
   match t with
   | Z0 => N0
   | Zpos ?n => Ncst (Npos n)
-  | Z_of_N ?n => Ncst n
+  | Z.of_N ?n => Ncst n
   | NtoZ ?n => Ncst n
   | _ => NotConstant
   end.
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index b05ee6495..700b4f3b2 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.v
@@ -101,10 +101,9 @@ Lemma Qpower_plus_positive : forall a n m, Qpower_positive a (n+m) == (Qpower_po
 Proof.
 intros a n m.
 unfold Qpower_positive.
-apply pow_pos_Pplus.
+apply pow_pos_add.
 apply Q_Setoid.
 apply Qmult_comp.
-apply Qmult_comm.
 apply Qmult_assoc.
 Qed.
 
@@ -114,21 +113,18 @@ intros a [|n|n]; simpl; try reflexivity.
 symmetry; apply Qinv_involutive.
 Qed.
 
-Lemma Qpower_minus_positive : forall a (n m:positive), (Pcompare n m Eq=Gt)%positive -> Qpower_positive a (n-m)%positive == (Qpower_positive a n)/(Qpower_positive a m).
+Lemma Qpower_minus_positive : forall a (n m:positive),
+  (m < n)%positive ->
+  Qpower_positive a (n-m)%positive == (Qpower_positive a n)/(Qpower_positive a m).
 Proof.
 intros a n m H.
-destruct (Qeq_dec a 0).
- rewrite q.
- repeat rewrite Qpower_positive_0.
- reflexivity.
-rewrite <- (Qdiv_mult_l (Qpower_positive a (n - m)) (Qpower_positive a m)) by
- (apply Qpower_not_0_positive; assumption).
-apply Qdiv_comp;[|reflexivity].
-rewrite Qmult_comm.
-rewrite <- Qpower_plus_positive.
-rewrite Pplus_minus.
-reflexivity.
-assumption.
+destruct (Qeq_dec a 0) as [EQ|NEQ].
+- now rewrite EQ, !Qpower_positive_0.
+- rewrite <- (Qdiv_mult_l (Qpower_positive a (n - m)) (Qpower_positive a m)) by
+   (now apply Qpower_not_0_positive).
+  f_equiv.
+  rewrite <- Qpower_plus_positive.
+  now rewrite Pos.sub_add.
 Qed.
 
 Lemma Qpower_plus : forall a n m, ~a==0 -> a^(n+m) == a^n*a^m.
@@ -140,8 +136,6 @@ rewrite ?Z.pos_sub_spec;
 case Pos.compare_spec; intros H0; simpl; subst;
  try rewrite Qpower_minus_positive;
  try (field; try split; apply Qpower_not_0_positive);
- try assumption;
- apply ZC2;
  assumption.
 Qed.
 
@@ -158,13 +152,14 @@ apply Qpower_plus.
 assumption.
 Qed.
 
-Lemma Qpower_mult_positive : forall a n m, Qpower_positive a (n*m) == Qpower_positive (Qpower_positive a n) m.
+Lemma Qpower_mult_positive : forall a n m,
+  Qpower_positive a (n*m) == Qpower_positive (Qpower_positive a n) m.
 Proof.
 intros a n m.
-induction n using Pind.
+induction n using Pos.peano_ind.
  reflexivity.
-rewrite Pmult_Sn_m.
-rewrite Pplus_one_succ_l.
+rewrite Pos.mul_succ_l.
+rewrite <- Pos.add_1_l.
 do 2 rewrite Qpower_plus_positive.
 rewrite IHn.
 rewrite Qmult_power_positive.
@@ -184,11 +179,11 @@ Qed.
 Lemma Zpower_Qpower : forall (a n:Z), (0<=n)%Z -> inject_Z (a^n) == (inject_Z a)^n.
 Proof.
 intros a [|n|n] H;[reflexivity| |elim H; reflexivity].
-induction n using Pind.
+induction n using Pos.peano_ind.
  replace (a^1)%Z with a by ring.
  ring.
-rewrite Zpos_succ_morphism.
-unfold Zsucc.
+rewrite Pos2Z.inj_succ.
+unfold Z.succ.
 rewrite Zpower_exp; auto with *; try discriminate.
 rewrite Qpower_plus' by discriminate.
 rewrite <- IHn by discriminate.
@@ -209,31 +204,20 @@ setoid_replace (0+ - a) with (-a) in A by ring.
 apply Qmult_le_0_compat; assumption.
 Qed.
 
-Theorem Qpower_decomp: forall p x y,
-  Qpower_positive (x #y) p == x ^ Zpos p # (Z2P ((Zpos y) ^ Zpos p)).
-Proof.
-induction p; intros; unfold Qmult; simpl.
-(* xI *)
-rewrite IHp, xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l.
-repeat rewrite Zpower_pos_is_exp.
-red; unfold Qmult, Qnum, Qden, Zpower.
-repeat rewrite Zpos_mult_morphism.
-repeat rewrite Z2P_correct.
-repeat rewrite Zpower_pos_1_r; ring.
-apply Zpower_pos_pos; red; auto.
-repeat apply Zmult_lt_0_compat; red; auto;
- apply Zpower_pos_pos; red; auto.
-(* xO *)
-rewrite IHp, <-Pplus_diag.
-repeat rewrite Zpower_pos_is_exp.
-red; unfold Qmult, Qnum, Qden, Zpower.
-repeat rewrite Zpos_mult_morphism.
-repeat rewrite Z2P_correct; try ring.
-apply Zpower_pos_pos; red; auto.
-repeat apply Zmult_lt_0_compat; auto;
- apply Zpower_pos_pos; red; auto.
-(* xO *)
-unfold Qmult; simpl.
-red; simpl; rewrite Zpower_pos_1_r;
- rewrite Zpos_mult_morphism; ring.
+Theorem Qpower_decomp p x y :
+  Qpower_positive (x#y) p = x ^ Zpos p # (y ^ p).
+Proof.
+induction p; intros; simpl Qpower_positive; rewrite ?IHp.
+- (* xI *)
+  unfold Qmult, Qnum, Qden. f_equal.
+  + now rewrite <- Z.pow_twice_r, <- Z.pow_succ_r.
+  + apply Pos2Z.inj; rewrite !Pos2Z.inj_mul, !Pos2Z.inj_pow.
+    now rewrite <- Z.pow_twice_r, <- Z.pow_succ_r.
+- (* xO *)
+  unfold Qmult, Qnum, Qden. f_equal.
+  + now rewrite <- Z.pow_twice_r.
+  + apply Pos2Z.inj; rewrite !Pos2Z.inj_mul, !Pos2Z.inj_pow.
+    now rewrite <- Z.pow_twice_r.
+- (* xO *)
+  now rewrite Z.pow_1_r, Pos.pow_1_r.
 Qed.
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index e39eca0cb..73ebea492 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -11,46 +11,29 @@
 Require Export QArith_base.
 Require Import Znumtheory.
 
-(** First, a function that (tries to) build a positive back from a Z. *)
+Notation Z2P := Z.to_pos (compat "8.3").
+Notation Z2P_correct := Z2Pos.id (compat "8.3").
 
-Definition Z2P (z : Z) :=
-  match z with
-  | Z0 => 1%positive
-  | Zpos p => p
-  | Zneg p => p
-  end.
-
-Lemma Z2P_correct : forall z : Z, (0 < z)%Z -> Zpos (Z2P z) = z.
-Proof.
- simple destruct z; simpl in |- *; auto; intros; discriminate.
-Qed.
-
-Lemma Z2P_correct2 : forall z : Z, 0%Z <> z -> Zpos (Z2P z) = Zabs z.
-Proof.
- simple destruct z; simpl in |- *; auto; intros; elim H; auto.
-Qed.
-
-(** Simplification of fractions using [Zgcd].
+(** Simplification of fractions using [Z.gcd].
   This version can compute within Coq. *)
 
 Definition Qred (q:Q) :=
   let (q1,q2) := q in
-  let (r1,r2) := snd (Zggcd q1 ('q2))
-  in r1#(Z2P r2).
+  let (r1,r2) := snd (Z.ggcd q1 ('q2))
+  in r1#(Z.to_pos r2).
 
 Lemma Qred_correct : forall q, (Qred q) == q.
 Proof.
   unfold Qred, Qeq; intros (n,d); simpl.
-  generalize (Zggcd_gcd n ('d)) (Zgcd_nonneg n ('d))
-    (Zggcd_correct_divisors n ('d)).
-  destruct (Zggcd n (Zpos d)) as (g,(nn,dd)); simpl.
+  generalize (Z.ggcd_gcd n ('d)) (Z.gcd_nonneg n ('d))
+    (Z.ggcd_correct_divisors n ('d)).
+  destruct (Z.ggcd n (Zpos d)) as (g,(nn,dd)); simpl.
   Open Scope Z_scope.
   intros Hg LE (Hn,Hd). rewrite Hd, Hn.
   rewrite <- Hg in LE; clear Hg.
   assert (0 <> g) by (intro; subst; discriminate).
-  rewrite Z2P_correct. ring.
-  apply Zmult_gt_0_lt_0_reg_r with g; auto with zarith.
-  now rewrite Zmult_comm, <- Hd.
+  rewrite Z2Pos.id. ring.
+  rewrite <- (Z.mul_pos_cancel_l g); [now rewrite <- Hd | omega].
   Close Scope Z_scope.
 Qed.
 
@@ -59,68 +42,54 @@ Proof.
   intros (a,b) (c,d).
   unfold Qred, Qeq in *; simpl in *.
   Open Scope Z_scope.
-  generalize (Zggcd_gcd a ('b)) (Zgcd_is_gcd a ('b))
-    (Zgcd_nonneg a ('b)) (Zggcd_correct_divisors a ('b)).
-  destruct (Zggcd a (Zpos b)) as (g,(aa,bb)).
-  generalize (Zggcd_gcd c ('d)) (Zgcd_is_gcd c ('d))
-    (Zgcd_nonneg c ('d)) (Zggcd_correct_divisors c ('d)).
-  destruct (Zggcd c (Zpos d)) as (g',(cc,dd)).
-  simpl.
-  intro H; rewrite <- H; clear H.
-  intros Hg'1 Hg'2 (Hg'3,Hg'4).
-  intro H; rewrite <- H; clear H.
-  intros Hg1 Hg2 (Hg3,Hg4).
-  intros.
-  assert (g <> 0) by (intro; subst g; discriminate).
-  assert (g' <> 0) by (intro; subst g'; discriminate).
+  intros H.
+  generalize (Z.ggcd_gcd a ('b)) (Zgcd_is_gcd a ('b))
+    (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)).
+  destruct (Z.ggcd a (Zpos b)) as (g,(aa,bb)).
+  simpl. intros <- Hg1 Hg2 (Hg3,Hg4).
+  assert (Hg0 : g <> 0) by (intro; now subst g).
+  generalize (Z.ggcd_gcd c ('d)) (Zgcd_is_gcd c ('d))
+    (Z.gcd_nonneg c ('d)) (Z.ggcd_correct_divisors c ('d)).
+  destruct (Z.ggcd c (Zpos d)) as (g',(cc,dd)).
+  simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4).
+  assert (Hg'0 : g' <> 0) by (intro; now subst g').
 
   elim (rel_prime_cross_prod aa bb cc dd).
-  congruence.
-  unfold rel_prime in |- *.
-  (*rel_prime*)
-  constructor.
-  exists aa; auto with zarith.
-  exists bb; auto with zarith.
-  intros.
-  inversion Hg1.
-  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 x'.
-  apply Zmult_reg_l with g; auto. rewrite Hx at 1; ring.
-  (* /rel_prime *)
-  unfold rel_prime in |- *.
-  (* rel_prime *)
-  constructor.
-  exists cc; auto with zarith.
-  exists dd; auto with zarith.
-  intros.
-  inversion Hg'1.
-  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 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.
-  omega.
-  rewrite Zmult_comm.
-  rewrite <- Hg4; compute; auto.
-  assert (0<dd); [|auto with zarith].
-  apply Zmult_gt_0_lt_0_reg_r with g'.
-  omega.
-  rewrite Zmult_comm.
-  rewrite <- Hg'4; compute; auto.
-  apply Zmult_reg_l with (g'*g).
-  intro H2; elim (Zmult_integral _ _ H2); auto.
-  replace (g'*g*(aa*dd)) with ((g*aa)*(g'*dd)); [|ring].
-  replace (g'*g*(bb*cc)) with ((g'*cc)*(g*bb)); [|ring].
-  rewrite <- Hg3; rewrite <- Hg4; rewrite <- Hg'3; rewrite <- Hg'4; auto.
+  - congruence.
+  - (*rel_prime*)
+    constructor.
+    * exists aa; auto with zarith.
+    * exists bb; auto with zarith.
+    * intros x Ha Hb.
+      destruct Hg1 as (Hg11,Hg12,Hg13).
+      destruct (Hg13 (g*x)) as (x',Hx).
+      { rewrite Hg3.
+        destruct Ha as (xa,Hxa); exists xa; rewrite Hxa; ring. }
+      { rewrite Hg4.
+        destruct Hb as (xb,Hxb); exists xb; rewrite Hxb; ring. }
+      exists x'.
+      apply Z.mul_reg_l with g; auto. rewrite Hx at 1; ring.
+  - (* rel_prime *)
+    constructor.
+    * exists cc; auto with zarith.
+    * exists dd; auto with zarith.
+    * intros x Hc Hd.
+      inversion Hg'1 as (Hg'11,Hg'12,Hg'13).
+      destruct (Hg'13 (g'*x)) as (x',Hx).
+      { rewrite Hg'3.
+        destruct Hc as (xc,Hxc); exists xc; rewrite Hxc; ring. }
+      { rewrite Hg'4.
+        destruct Hd as (xd,Hxd); exists xd; rewrite Hxd; ring. }
+      exists x'.
+      apply Z.mul_reg_l with g'; auto. rewrite Hx at 1; ring.
+  - apply Z.lt_gt.
+    rewrite <- (Z.mul_pos_cancel_l g); [now rewrite <- Hg4 | omega].
+  - apply Z.lt_gt.
+    rewrite <- (Z.mul_pos_cancel_l g'); [now rewrite <- Hg'4 | omega].
+  - apply Z.mul_reg_l with (g*g').
+    * rewrite Z.mul_eq_0. now destruct 1.
+    * rewrite Z.mul_shuffle1, <- Hg3, <- Hg'4.
+      now rewrite Z.mul_shuffle1, <- Hg'3, <- Hg4, H, Z.mul_comm.
   Close Scope Z_scope.
 Qed.
 
@@ -137,39 +106,39 @@ Definition Qminus' x y := Qred (Qminus x y).
 
 Lemma Qplus'_correct : forall p q : Q, (Qplus' p q)==(Qplus p q).
 Proof.
-  intros; unfold Qplus' in |- *; apply Qred_correct; auto.
+  intros; unfold Qplus'; apply Qred_correct; auto.
 Qed.
 
 Lemma Qmult'_correct : forall p q : Q, (Qmult' p q)==(Qmult p q).
 Proof.
-  intros; unfold Qmult' in |- *; apply Qred_correct; auto.
+  intros; unfold Qmult'; apply Qred_correct; auto.
 Qed.
 
 Lemma Qminus'_correct : forall p q : Q, (Qminus' p q)==(Qminus p q).
 Proof.
-  intros; unfold Qminus' in |- *; apply Qred_correct; auto.
+  intros; unfold Qminus'; apply Qred_correct; auto.
 Qed.
 
 Add Morphism Qplus' : Qplus'_comp.
 Proof.
-  intros; unfold Qplus' in |- *.
-  rewrite H; rewrite H0; auto with qarith.
+  intros; unfold Qplus'.
+  rewrite H, H0; auto with qarith.
 Qed.
 
 Add Morphism Qmult' : Qmult'_comp.
-  intros; unfold Qmult' in |- *.
-  rewrite H; rewrite H0; auto with qarith.
+  intros; unfold Qmult'.
+  rewrite H, H0; auto with qarith.
 Qed.
 
 Add Morphism Qminus' : Qminus'_comp.
-  intros; unfold Qminus' in |- *.
-  rewrite H; rewrite H0; auto with qarith.
+  intros; unfold Qminus'.
+  rewrite H, H0; auto with qarith.
 Qed.
 
 Lemma Qred_opp: forall q, Qred (-q) = - (Qred q).
 Proof.
   intros (x, y); unfold Qred; simpl.
-  rewrite Zggcd_opp; case Zggcd; intros p1 (p2, p3); simpl.
+  rewrite Z.ggcd_opp; case Z.ggcd; intros p1 (p2, p3); simpl.
   unfold Qopp; auto.
 Qed.
 
@@ -178,4 +147,3 @@ Theorem Qred_compare: forall x y,
 Proof.
   intros x y; apply Qcompare_comp; apply Qeq_sym; apply Qred_correct.
 Qed.
-
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index ce363a33b..cfc1fb141 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -11,7 +11,7 @@ Require Import QArith.
 Lemma Qopp_lt_compat: forall p q : Q, p < q -> - q < - p.
 Proof.
 intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl.
-do 2 rewrite <- Zopp_mult_distr_l; omega.
+rewrite !Z.mul_opp_l; omega.
 Qed.
 
 Hint Resolve Qopp_lt_compat : qarith.
@@ -20,7 +20,7 @@ Hint Resolve Qopp_lt_compat : qarith.
 
 Coercion Local inject_Z : Z >-> Q.
 
-Definition Qfloor (x:Q) := let (n,d) := x in Zdiv n (Zpos d).
+Definition Qfloor (x:Q) := let (n,d) := x in Z.div n (Zpos d).
 Definition Qceiling (x:Q) := (-(Qfloor (-x)))%Z.
 
 Lemma Qfloor_Z : forall z:Z, Qfloor z = z.
@@ -46,7 +46,7 @@ simpl.
 unfold Qle.
 simpl.
 replace (n*1)%Z with n by ring.
-rewrite Zmult_comm.
+rewrite Z.mul_comm.
 apply Z_mult_div_ge.
 auto with *.
 Qed.
@@ -81,7 +81,7 @@ ring_simplify.
 replace (n / ' d * ' d + ' d)%Z with
   (('d * (n / 'd) + n mod 'd) + 'd - n mod 'd)%Z by ring.
 rewrite <- Z_div_mod_eq; auto with*.
-rewrite <- Zlt_plus_swap.
+rewrite <- Z.lt_add_lt_sub_r.
 destruct (Z_mod_lt n ('d)); auto with *.
 Qed.
 
@@ -107,7 +107,7 @@ unfold Qle in *.
 simpl in *.
 rewrite <- (Zdiv_mult_cancel_r xn ('xd) ('yd)); auto with *.
 rewrite <- (Zdiv_mult_cancel_r yn ('yd) ('xd)); auto with *.
-rewrite (Zmult_comm ('yd) ('xd)).
+rewrite (Z.mul_comm ('yd) ('xd)).
 apply Z_div_le; auto with *.
 Qed.
 
@@ -125,7 +125,7 @@ Hint Resolve Qceiling_resp_le : qarith.
 Add Morphism Qfloor with signature Qeq ==> eq as Qfloor_comp.
 Proof.
 intros x y H.
-apply Zle_antisym.
+apply Z.le_antisymm.
  auto with *.
 symmetry in H; auto with *.
 Qed.
@@ -133,7 +133,7 @@ Qed.
 Add Morphism Qceiling with signature Qeq ==> eq as Qceiling_comp.
 Proof.
 intros x y H.
-apply Zle_antisym.
+apply Z.le_antisymm.
  auto with *.
 symmetry in H; auto with *.
 Qed.
@@ -142,9 +142,9 @@ Lemma Zdiv_Qdiv (n m: Z): (n / m)%Z = Qfloor (n / m).
 Proof.
  unfold Qfloor. intros. simpl.
  destruct m as [?|?|p]; simpl.
-  now rewrite Zdiv_0_r, Zmult_0_r.
-  now rewrite Zmult_1_r.
- rewrite <- Zopp_eq_mult_neg_1.
- rewrite <- (Zopp_involutive (Zpos p)).
+  now rewrite Zdiv_0_r, Z.mul_0_r.
+  now rewrite Z.mul_1_r.
+ rewrite <- Z.opp_eq_mul_m1.
+ rewrite <- (Z.opp_involutive (Zpos p)).
  now rewrite Zdiv_opp_opp.
 Qed.