Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def

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

1 files changed, 72 insertions, 87 deletions

diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index 6b6ad7423..9a95669f5 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -6,13 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Nnat ZArith_base ROmega ZArithRing Zdiv_def Zdiv Morphisms.
+Require Import Nnat ZArith_base ROmega ZArithRing Zdiv Morphisms.
 
 Local Open Scope Z_scope.
 
 (** This file provides results about the Round-Toward-Zero Euclidean
   division [Zquotrem], whose projections are [Zquot] and [Zrem].
-  Definition of this division can be found in file [Zdiv_def].
+  Definition of this division can be found in file [BinIntDef].
 
   This division and the one defined in Zdiv agree only on positive
   numbers. Otherwise, Zdiv performs Round-Toward-Bottom (a.k.a Floor).
@@ -29,15 +29,15 @@ Lemma Ndiv_Zquot : forall a b:N,
 Proof.
   intros.
   destruct a; destruct b; simpl; auto.
-  unfold N.div, Zquot; simpl. destruct N.pos_div_eucl; auto.
+  unfold N.div, Z.quot; simpl. destruct N.pos_div_eucl; auto.
 Qed.
 
 Lemma Nmod_Zrem : forall a b:N,
-  Z_of_N (a mod b) = Zrem (Z_of_N a) (Z_of_N b).
+  Z.of_N (a mod b) = Z.rem (Z.of_N a) (Z.of_N b).
 Proof.
   intros.
   destruct a; destruct b; simpl; auto.
-  unfold N.modulo, Zrem; simpl; destruct N.pos_div_eucl; auto.
+  unfold N.modulo, Z.rem; simpl; destruct N.pos_div_eucl; auto.
 Qed.
 
 (** * Characterization of this euclidean division. *)
@@ -46,13 +46,13 @@ Qed.
    has been chosen to be [a], so this equation holds even for [b=0].
 *)
 
-Notation Z_quot_rem_eq := Z_quot_rem_eq (only parsing).
+Notation Z_quot_rem_eq := Z.quot_rem' (only parsing).
 
 (** Then, the inequalities constraining the remainder:
     The remainder is bounded by the divisor, in term of absolute values *)
 
 Theorem Zrem_lt : forall a b:Z, b<>0 ->
-  Zabs (Zrem a b) < Zabs b.
+  Z.abs (Z.rem a b) < Z.abs b.
 Proof.
   apply Z.rem_bound_abs.
 Qed.
@@ -61,35 +61,27 @@ Qed.
    nullity of [a], a general result is to be stated in the following form:
 *)
 
-Theorem Zrem_sgn : forall a b:Z,
-  0 <= Zsgn (Zrem a b) * Zsgn a.
+Theorem Zrem_sgn a b : 0 <= Z.sgn (Z.rem a b) * Z.sgn a.
 Proof.
   destruct b as [ |b|b]; destruct a as [ |a|a]; simpl; auto with zarith;
-  unfold Zrem, Zquotrem; destruct N.pos_div_eucl;
+  unfold Z.rem, Z.quotrem; destruct N.pos_div_eucl;
   simpl; destruct n0; simpl; auto with zarith.
 Qed.
 
 (** This can also be said in a simplier way: *)
 
-Theorem Zsgn_pos_iff : forall z, 0 <= Zsgn z <-> 0 <= z.
+Theorem Zrem_sgn2 a b : 0 <= (Z.rem a b) * a.
 Proof.
- destruct z; simpl; intuition auto with zarith.
-Qed.
-
-Theorem Zrem_sgn2 : forall a b:Z,
-  0 <= (Zrem a b) * a.
-Proof.
-  intros; rewrite <-Zsgn_pos_iff, Zsgn_Zmult; apply Zrem_sgn.
+  rewrite <-Z.sgn_nonneg, Z.sgn_mul; apply Zrem_sgn.
 Qed.
 
 (** Reformulation of [Zquot_lt] and [Zrem_sgn] in 2
   then 4 particular cases. *)
 
-Theorem Zrem_lt_pos : forall a b:Z, 0<=a -> b<>0 ->
-  0 <= Zrem a b < Zabs b.
+Theorem Zrem_lt_pos a b : 0<=a -> b<>0 -> 0 <= Z.rem a b < Z.abs b.
 Proof.
   intros.
-  assert (0 <= Zrem a b).
+  assert (0 <= Z.rem a b).
    generalize (Zrem_sgn a b).
    destruct (Zle_lt_or_eq 0 a H).
    rewrite <- Zsgn_pos in H1; rewrite H1. romega with *.
@@ -97,11 +89,10 @@ Proof.
   generalize (Zrem_lt a b H0); romega with *.
 Qed.
 
-Theorem Zrem_lt_neg : forall a b:Z, a<=0 -> b<>0 ->
-  -Zabs b < Zrem a b <= 0.
+Theorem Zrem_lt_neg a b : a<=0 -> b<>0 -> -Z.abs b < Z.rem a b <= 0.
 Proof.
   intros.
-  assert (Zrem a b <= 0).
+  assert (Z.rem a b <= 0).
    generalize (Zrem_sgn a b).
    destruct (Zle_lt_or_eq a 0 H).
    rewrite <- Zsgn_neg in H1; rewrite H1; romega with *.
@@ -109,22 +100,22 @@ Proof.
   generalize (Zrem_lt a b H0); romega with *.
 Qed.
 
-Theorem Zrem_lt_pos_pos : forall a b:Z, 0<=a -> 0<b -> 0 <= Zrem a b < b.
+Theorem Zrem_lt_pos_pos a b : 0<=a -> 0<b -> 0 <= Z.rem a b < b.
 Proof.
   intros; generalize (Zrem_lt_pos a b); romega with *.
 Qed.
 
-Theorem Zrem_lt_pos_neg : forall a b:Z, 0<=a -> b<0 -> 0 <= Zrem a b < -b.
+Theorem Zrem_lt_pos_neg a b : 0<=a -> b<0 -> 0 <= Z.rem a b < -b.
 Proof.
   intros; generalize (Zrem_lt_pos a b); romega with *.
 Qed.
 
-Theorem Zrem_lt_neg_pos : forall a b:Z, a<=0 -> 0<b -> -b < Zrem a b <= 0.
+Theorem Zrem_lt_neg_pos a b : a<=0 -> 0<b -> -b < Z.rem a b <= 0.
 Proof.
   intros; generalize (Zrem_lt_neg a b); romega with *.
 Qed.
 
-Theorem Zrem_lt_neg_neg : forall a b:Z, a<=0 -> b<0 -> b < Zrem a b <= 0.
+Theorem Zrem_lt_neg_neg a b : a<=0 -> b<0 -> b < Z.rem a b <= 0.
 Proof.
   intros; generalize (Zrem_lt_neg a b); romega with *.
 Qed.
@@ -133,49 +124,49 @@ Qed.
 
 (* The precise equalities that are invalid with "historic" Zdiv. *)
 
-Theorem Zquot_opp_l : forall a b:Z, (-a)÷b = -(a÷b).
+Theorem Zquot_opp_l a b : (-a)÷b = -(a÷b).
 Proof.
  destruct a; destruct b; simpl; auto;
-  unfold Zquot, Zquotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
+  unfold Z.quot, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
 Qed.
 
-Theorem Zquot_opp_r : forall a b:Z, a÷(-b) = -(a÷b).
+Theorem Zquot_opp_r a b : a÷(-b) = -(a÷b).
 Proof.
  destruct a; destruct b; simpl; auto;
-  unfold Zquot, Zquotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
+  unfold Z.quot, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
 Qed.
 
-Theorem Zrem_opp_l : forall a b:Z, Zrem (-a) b = -(Zrem a b).
+Theorem Zrem_opp_l a b : Z.rem (-a) b = -(Z.rem a b).
 Proof.
  destruct a; destruct b; simpl; auto;
-  unfold Zrem, Zquotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
+  unfold Z.rem, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
 Qed.
 
-Theorem Zrem_opp_r : forall a b:Z, Zrem a (-b) = Zrem a b.
+Theorem Zrem_opp_r a b : Z.rem a (-b) = Z.rem a b.
 Proof.
  destruct a; destruct b; simpl; auto;
-  unfold Zrem, Zquotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
+  unfold Z.rem, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
 Qed.
 
-Theorem Zquot_opp_opp : forall a b:Z, (-a)÷(-b) = a÷b.
+Theorem Zquot_opp_opp a b : (-a)÷(-b) = a÷b.
 Proof.
  destruct a; destruct b; simpl; auto;
-  unfold Zquot, Zquotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
+  unfold Z.quot, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
 Qed.
 
-Theorem Zrem_opp_opp : forall a b:Z, Zrem (-a) (-b) = -(Zrem a b).
+Theorem Zrem_opp_opp a b : Z.rem (-a) (-b) = -(Z.rem a b).
 Proof.
  destruct a; destruct b; simpl; auto;
-  unfold Zrem, Zquotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
+  unfold Z.rem, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith.
 Qed.
 
 (** * Unicity results *)
 
 Definition Remainder a b r :=
-  (0 <= a /\ 0 <= r < Zabs b) \/ (a <= 0 /\ -Zabs b < r <= 0).
+  (0 <= a /\ 0 <= r < Z.abs b) \/ (a <= 0 /\ -Z.abs b < r <= 0).
 
 Definition Remainder_alt a b r :=
-  Zabs r < Zabs b /\ 0 <= r * a.
+  Z.abs r < Z.abs b /\ 0 <= r * a.
 
 Lemma Remainder_equiv : forall a b r,
  Remainder a b r <-> Remainder_alt a b r.
@@ -185,13 +176,13 @@ Proof.
   romega with *.
   rewrite <-(Zmult_opp_opp).
   apply Zmult_le_0_compat; romega.
-  assert (0 <= Zsgn r * Zsgn a) by (rewrite <-Zsgn_Zmult, Zsgn_pos_iff; auto).
-  destruct r; simpl Zsgn in *; romega with *.
+  assert (0 <= Z.sgn r * Z.sgn a) by (rewrite <-Z.sgn_mul, Z.sgn_nonneg; auto).
+  destruct r; simpl Z.sgn in *; romega with *.
 Qed.
 
 Theorem Zquot_mod_unique_full:
  forall a b q r, Remainder a b r ->
-   a = b*q + r -> q = a÷b /\ r = Zrem a b.
+   a = b*q + r -> q = a÷b /\ r = Z.rem a b.
 Proof.
   destruct 1 as [(H,H0)|(H,H0)]; intros.
   apply Zdiv_mod_unique with b; auto.
@@ -201,7 +192,7 @@ Proof.
 
   rewrite <- (Zopp_involutive a).
   rewrite Zquot_opp_l, Zrem_opp_l.
-  generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Zrem (-a) b)).
+  generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Z.rem (-a) b)).
   generalize (Zrem_lt_pos (-a) b).
   rewrite <-Z_quot_rem_eq, <-Zopp_mult_distr_r, <-Zopp_plus_distr, <-H1.
   romega with *.
@@ -221,24 +212,24 @@ Proof. exact Z.quot_unique. Qed.
 
 Theorem Zrem_unique_full:
  forall a b q r, Remainder a b r ->
-  a = b*q + r -> r = Zrem a b.
+  a = b*q + r -> r = Z.rem a b.
 Proof.
  intros; destruct (Zquot_mod_unique_full a b q r); auto.
 Qed.
 
 Theorem Zrem_unique:
  forall a b q r, 0 <= a -> 0 <= r < b ->
-   a = b*q + r -> r = Zrem a b.
+   a = b*q + r -> r = Z.rem a b.
 Proof. exact Z.rem_unique. Qed.
 
 (** * Basic values of divisions and modulo. *)
 
-Lemma Zrem_0_l: forall a, Zrem 0 a = 0.
+Lemma Zrem_0_l: forall a, Z.rem 0 a = 0.
 Proof.
   destruct a; simpl; auto.
 Qed.
 
-Lemma Zrem_0_r: forall a, Zrem a 0 = a.
+Lemma Zrem_0_r: forall a, Z.rem a 0 = a.
 Proof.
   destruct a; simpl; auto.
 Qed.
@@ -253,7 +244,7 @@ Proof.
   destruct a; simpl; auto.
 Qed.
 
-Lemma Zrem_1_r: forall a, Zrem a 1 = 0.
+Lemma Zrem_1_r: forall a, Z.rem a 1 = 0.
 Proof. exact Z.rem_1_r. Qed.
 
 Lemma Zquot_1_r: forall a, a÷1 = a.
@@ -265,21 +256,21 @@ Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Zquot_1_r Zrem_1_r
 Lemma Zquot_1_l: forall a, 1 < a -> 1÷a = 0.
 Proof. exact Z.quot_1_l. Qed.
 
-Lemma Zrem_1_l: forall a, 1 < a -> Zrem 1 a = 1.
+Lemma Zrem_1_l: forall a, 1 < a -> Z.rem 1 a = 1.
 Proof. exact Z.rem_1_l. Qed.
 
 Lemma Z_quot_same : forall a:Z, a<>0 -> a÷a = 1.
 Proof. exact Z.quot_same. Qed.
 
 Ltac zero_or_not a :=
-  destruct (Z_eq_dec a 0);
+  destruct (Z.eq_dec a 0);
   [subst; rewrite ?Zrem_0_l, ?Zquot_0_l, ?Zrem_0_r, ?Zquot_0_r;
    auto with zarith|].
 
-Lemma Z_rem_same : forall a, Zrem a a = 0.
+Lemma Z_rem_same : forall a, Z.rem a a = 0.
 Proof. intros. zero_or_not a. apply Z.rem_same; auto. Qed.
 
-Lemma Z_rem_mult : forall a b, Zrem (a*b) b = 0.
+Lemma Z_rem_mult : forall a b, Z.rem (a*b) b = 0.
 Proof. intros. zero_or_not b. apply Z.rem_mul; auto. Qed.
 
 Lemma Z_quot_mult : forall a b:Z, b <> 0 -> (a*b)÷b = a.
@@ -305,7 +296,7 @@ Proof. exact Z.quot_small. Qed.
 
 (** Same situation, in term of modulo: *)
 
-Theorem Zrem_small: forall a n, 0 <= a < n -> Zrem a n = a.
+Theorem Zrem_small: forall a n, 0 <= a < n -> Z.rem a n = a.
 Proof. exact Z.rem_small. Qed.
 
 (** [Zge] is compatible with a positive division. *)
@@ -324,12 +315,12 @@ Proof. intros. zero_or_not b. apply Z.mul_quot_ge; auto with zarith. Qed.
 (** The previous inequalities between [b*(a÷b)] and [a] are exact
     iff the modulo is zero. *)
 
-Lemma Z_quot_exact_full : forall a b:Z, a = b*(a÷b) <-> Zrem a b = 0.
+Lemma Z_quot_exact_full : forall a b:Z, a = b*(a÷b) <-> Z.rem a b = 0.
 Proof. intros. zero_or_not b. intuition. apply Z.quot_exact; auto. Qed.
 
 (** A modulo cannot grow beyond its starting point. *)
 
-Theorem Zrem_le: forall a b, 0 <= a -> 0 <= b -> Zrem a b <= a.
+Theorem Zrem_le: forall a b, 0 <= a -> 0 <= b -> Z.rem a b <= a.
 Proof. intros. zero_or_not b. apply Z.rem_le; auto with zarith. Qed.
 
 (** Some additionnal inequalities about Zdiv. *)
@@ -347,10 +338,10 @@ Theorem Zquot_le_lower_bound:
 Proof. intros a b q; rewrite Zmult_comm; apply Z.quot_le_lower_bound. Qed.
 
 Theorem Zquot_sgn: forall a b,
-  0 <= Zsgn (a÷b) * Zsgn a * Zsgn b.
+  0 <= Z.sgn (a÷b) * Z.sgn a * Z.sgn b.
 Proof.
   destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith;
-  unfold Zquot; simpl; destruct N.pos_div_eucl; simpl; destruct n; simpl; auto with zarith.
+  unfold Z.quot; simpl; destruct N.pos_div_eucl; simpl; destruct n; simpl; auto with zarith.
 Qed.
 
 (** * Relations between usual operations and Zmod and Zdiv *)
@@ -361,7 +352,7 @@ Qed.
 
 Lemma Z_rem_plus : forall a b c:Z,
  0 <= (a+b*c) * a ->
- Zrem (a + b * c) c = Zrem a c.
+ Z.rem (a + b * c) c = Z.rem a c.
 Proof. intros. zero_or_not c. apply Z.rem_add; auto with zarith. Qed.
 
 Lemma Z_quot_plus : forall a b c:Z,
@@ -388,14 +379,14 @@ Proof.
 Qed.
 
 Lemma Zmult_rem_distr_l: forall a b c,
-  Zrem (c*a) (c*b) = c * (Zrem a b).
+  Z.rem (c*a) (c*b) = c * (Z.rem a b).
 Proof.
  intros. zero_or_not c. rewrite (Zmult_comm c b). zero_or_not b.
  rewrite (Zmult_comm b c). apply Z.mul_rem_distr_l; auto.
 Qed.
 
 Lemma Zmult_rem_distr_r: forall a b c,
-  Zrem (a*c) (b*c) = (Zrem a b) * c.
+  Z.rem (a*c) (b*c) = (Z.rem a b) * c.
 Proof.
  intros. zero_or_not b. rewrite (Zmult_comm b c). zero_or_not c.
  rewrite (Zmult_comm c b). apply Z.mul_rem_distr_r; auto.
@@ -403,11 +394,11 @@ Qed.
 
 (** Operations modulo. *)
 
-Theorem Zrem_rem: forall a n, Zrem (Zrem a n) n = Zrem a n.
+Theorem Zrem_rem: forall a n, Z.rem (Z.rem a n) n = Z.rem a n.
 Proof. intros. zero_or_not n. apply Z.rem_rem; auto. Qed.
 
 Theorem Zmult_rem: forall a b n,
- Zrem (a * b) n = Zrem (Zrem a n * Zrem b n) n.
+ Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n.
 Proof. intros. zero_or_not n. apply Z.mul_rem; auto. Qed.
 
 (** addition and modulo
@@ -420,26 +411,26 @@ Proof. intros. zero_or_not n. apply Z.mul_rem; auto. Qed.
 
 Theorem Zplus_rem: forall a b n,
  0 <= a * b ->
- Zrem (a + b) n = Zrem (Zrem a n + Zrem b n) n.
+ Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) n.
 Proof. intros. zero_or_not n. apply Z.add_rem; auto. Qed.
 
 Lemma Zplus_rem_idemp_l: forall a b n,
  0 <= a * b ->
- Zrem (Zrem a n + b) n = Zrem (a + b) n.
+ Z.rem (Z.rem a n + b) n = Z.rem (a + b) n.
 Proof. intros. zero_or_not n. apply Z.add_rem_idemp_l; auto. Qed.
 
 Lemma Zplus_rem_idemp_r: forall a b n,
  0 <= a*b ->
- Zrem (b + Zrem a n) n = Zrem (b + a) n.
+ Z.rem (b + Z.rem a n) n = Z.rem (b + a) n.
 Proof.
  intros. zero_or_not n. apply Z.add_rem_idemp_r; auto.
  rewrite Zmult_comm; auto.
 Qed.
 
-Lemma Zmult_rem_idemp_l: forall a b n, Zrem (Zrem a n * b) n = Zrem (a * b) n.
+Lemma Zmult_rem_idemp_l: forall a b n, Z.rem (Z.rem a n * b) n = Z.rem (a * b) n.
 Proof. intros. zero_or_not n. apply Z.mul_rem_idemp_l; auto. Qed.
 
-Lemma Zmult_rem_idemp_r: forall a b n, Zrem (b * Zrem a n) n = Zrem (b * a) n.
+Lemma Zmult_rem_idemp_r: forall a b n, Z.rem (b * Z.rem a n) n = Z.rem (b * a) n.
 Proof. intros. zero_or_not n. apply Z.mul_rem_idemp_r; auto. Qed.
 
 (** Unlike with Zdiv, the following result is true without restrictions. *)
@@ -456,10 +447,10 @@ Theorem Zquot_mult_le:
  forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a÷b) <= (c*a)÷b.
 Proof. intros. zero_or_not b. apply Z.quot_mul_le; auto with zarith. Qed.
 
-(** Zrem is related to divisibility (see more in Znumtheory) *)
+(** Z.rem is related to divisibility (see more in Znumtheory) *)
 
 Lemma Zrem_divides : forall a b,
- Zrem a b = 0 <-> exists c, a = b*c.
+ Z.rem a b = 0 <-> exists c, a = b*c.
 Proof.
  intros. zero_or_not b. firstorder.
  rewrite Z.rem_divide; trivial.
@@ -469,7 +460,7 @@ Qed.
 (** Particular case : dividing by 2 is related with parity *)
 
 Lemma Zquot2_odd_remainder : forall a,
- Remainder a 2 (if Zodd_bool a then Zsgn a else 0).
+ Remainder a 2 (if Z.odd a then Z.sgn a else 0).
 Proof.
  intros [ |p|p]. simpl.
  left. simpl. auto with zarith.
@@ -477,15 +468,9 @@ Proof.
  right. destruct p; simpl; split; now auto with zarith.
 Qed.
 
-Lemma Zquot2_quot : forall a, Zquot2 a = a÷2.
-Proof.
- intros.
- apply Zquot_unique_full with (if Zodd_bool a then Zsgn a else 0).
- apply Zquot2_odd_remainder.
- apply Zquot2_odd_eqn.
-Qed.
+Notation Zquot2_quot := Zquot2_quot (only parsing).
 
-Lemma Zrem_odd : forall a, Zrem a 2 = if Zodd_bool a then Zsgn a else 0.
+Lemma Zrem_odd : forall a, Z.rem a 2 = if Z.odd a then Z.sgn a else 0.
 Proof.
  intros. symmetry.
  apply Zrem_unique_full with (Zquot2 a).
@@ -493,18 +478,18 @@ Proof.
  apply Zquot2_odd_eqn.
 Qed.
 
-Lemma Zrem_even : forall a, Zrem a 2 = if Zeven_bool a then 0 else Zsgn a.
+Lemma Zrem_even : forall a, Z.rem a 2 = if Z.even a then 0 else Z.sgn a.
 Proof.
  intros a. rewrite Zrem_odd, Zodd_even_bool. now destruct Zeven_bool.
 Qed.
 
-Lemma Zeven_rem : forall a, Zeven_bool a = Zeq_bool (Zrem a 2) 0.
+Lemma Zeven_rem : forall a, Z.even a = Zeq_bool (Z.rem a 2) 0.
 Proof.
  intros a. rewrite Zrem_even.
  destruct a as [ |p|p]; trivial; now destruct p.
 Qed.
 
-Lemma Zodd_rem : forall a, Zodd_bool a = negb (Zeq_bool (Zrem a 2) 0).
+Lemma Zodd_rem : forall a, Z.odd a = negb (Zeq_bool (Z.rem a 2) 0).
 Proof.
  intros a. rewrite Zrem_odd.
  destruct a as [ |p|p]; trivial; now destruct p.
@@ -515,7 +500,7 @@ Qed.
 (** They agree at least on positive numbers: *)
 
 Theorem Zquotrem_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b ->
-  a÷b = a/b /\ Zrem a b = a mod b.
+  a÷b = a/b /\ Z.rem a b = a mod b.
 Proof.
   intros.
   apply Zdiv_mod_unique with b.
@@ -535,7 +520,7 @@ Proof.
 Qed.
 
 Theorem Zrem_Zmod_pos : forall a b, 0 <= a -> 0 < b ->
-  Zrem a b = a mod b.
+  Z.rem a b = a mod b.
 Proof.
  intros a b Ha Hb; generalize (Zquotrem_Zdiv_eucl_pos a b Ha Hb);
  intuition.
@@ -544,7 +529,7 @@ Qed.
 (** Modulos are null at the same places *)
 
 Theorem Zrem_Zmod_zero : forall a b, b<>0 ->
- (Zrem a b = 0 <-> a mod b = 0).
+ (Z.rem a b = 0 <-> a mod b = 0).
 Proof.
  intros.
  rewrite Zrem_divides, Zmod_divides; intuition.