Zdiv seen as a quasi-instantation of generic ZDivFloor from theories/Numbers

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

1 files changed, 84 insertions, 373 deletions

diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index f3e656970..06aa2b660 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -18,11 +18,8 @@
 *)
 
 Require Export ZArith_base.
-Require Import Zbool.
-Require Import Omega.
-Require Import ZArithRing.
-Require Import Zcomplements.
-Require Export Setoid.
+Require Import Zbool Omega ZArithRing Zcomplements Setoid Morphisms.
+Require ZDivFloor ZBinary.
 Open Local Scope Z_scope.
 
 (** * Definitions of Euclidian operations *)
@@ -303,6 +300,28 @@ Proof.
   apply Z_div_mod_eq; auto.
 Qed.
 
+(** We know enough to prove that [Zdiv] and [Zmod] are instances of
+    one of the abstract Euclidean divisions of Numbers. *)
+
+Module ZDiv <: ZDivFloor.ZDiv ZBinary.ZBinAxiomsMod.
+ Definition div := Zdiv.
+ Definition modulo := Zmod.
+ Program Instance div_wd : Proper (eq==>eq==>eq) div.
+ Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
+
+ Definition div_mod := Z_div_mod_eq_full.
+ Definition mod_pos_bound : forall a b:Z, 0<b -> 0<=a mod b<b.
+ Proof. intros; apply Z_mod_lt; auto with zarith. Qed.
+ Definition mod_neg_bound := Z_mod_neg.
+End ZDiv.
+
+Module ZDivMod := ZBinary.ZBinAxiomsMod <+ ZDiv.
+
+(** We hence benefit from generic results about this abstract division. *)
+
+Module Z := ZDivFloor.ZDivPropFunct ZDivMod.
+
+
 (** Existence theorem *)
 
 Theorem Zdiv_eucl_exist : forall (b:Z)(Hb:b>0)(a:Z),
@@ -340,58 +359,27 @@ Theorem Zdiv_mod_unique_2 :
  forall b q1 q2 r1 r2:Z,
   Remainder r1 b -> Remainder r2 b ->
   b*q1+r1 = b*q2+r2 -> q1=q2 /\ r1=r2.
-Proof.
-unfold Remainder.
-intros b q1 q2 r1 r2 Hr1 Hr2 H.
-destruct (Z_eq_dec q1 q2) as [Hq|Hq].
-split; trivial.
-rewrite Hq in H; omega.
-elim (Zlt_not_le (Zabs (r2 - r1)) (Zabs b)).
-omega with *.
-replace (r2-r1) with (b*(q1-q2)) by (rewrite Zmult_minus_distr_l; omega).
-replace (Zabs b) with ((Zabs b)*1) by ring.
-rewrite Zabs_Zmult.
-apply Zmult_le_compat_l; auto with *.
-omega with *.
-Qed.
+Proof. exact Z.div_mod_unique. Qed.
 
 Theorem Zdiv_unique_full:
  forall a b q r, Remainder r b ->
    a = b*q + r -> q = a/b.
-Proof.
-  intros.
-  assert (b <> 0) by (unfold Remainder in *; omega with *).
-  generalize (Z_div_mod_full a b H1).
-  unfold Zdiv; destruct Zdiv_eucl as (q',r').
-  intros (H2,H3); rewrite H2 in H0.
-  destruct (Zdiv_mod_unique_2 b q q' r r'); auto.
-Qed.
+Proof. exact Z.div_unique. Qed.
 
 Theorem Zdiv_unique:
  forall a b q r, 0 <= r < b ->
    a = b*q + r -> q = a/b.
-Proof.
-  intros; eapply Zdiv_unique_full; eauto.
-Qed.
+Proof. intros; eapply Zdiv_unique_full; eauto. Qed.
 
 Theorem Zmod_unique_full:
  forall a b q r, Remainder r b ->
   a = b*q + r ->  r = a mod b.
-Proof.
-  intros.
-  assert (b <> 0) by (unfold Remainder in *; omega with *).
-  generalize (Z_div_mod_full a b H1).
-  unfold Zmod; destruct Zdiv_eucl as (q',r').
-  intros (H2,H3); rewrite H2 in H0.
-  destruct (Zdiv_mod_unique_2 b q q' r r'); auto.
-Qed.
+Proof. exact Z.mod_unique. Qed.
 
 Theorem Zmod_unique:
  forall a b q r, 0 <= r < b ->
   a = b*q + r -> r = a mod b.
-Proof.
-  intros; eapply Zmod_unique_full; eauto.
-Qed.
+Proof. intros; eapply Zmod_unique_full; eauto. Qed.
 
 (** * Basic values of divisions and modulo. *)
 
@@ -415,70 +403,44 @@ Proof.
   destruct a; simpl; auto.
 Qed.
 
+Ltac zero_or_not a :=
+  destruct (Z_eq_dec a 0);
+  [subst; rewrite ?Zmod_0_l, ?Zdiv_0_l, ?Zmod_0_r, ?Zdiv_0_r;
+   auto with zarith|].
+
 Lemma Zmod_1_r: forall a, a mod 1 = 0.
-Proof.
-  intros; symmetry; apply Zmod_unique with a; auto with zarith.
-Qed.
+Proof. intros. zero_or_not a. apply Z.mod_1_r. Qed.
 
 Lemma Zdiv_1_r: forall a, a/1 = a.
-Proof.
-  intros; symmetry; apply Zdiv_unique with 0; auto with zarith.
-Qed.
+Proof. intros. zero_or_not a. apply Z.div_1_r. Qed.
 
 Hint Resolve Zmod_0_l Zmod_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_1_r
  : zarith.
 
 Lemma Zdiv_1_l: forall a, 1 < a -> 1/a = 0.
-Proof.
-  intros; symmetry; apply Zdiv_unique with 1; auto with zarith.
-Qed.
+Proof. exact Z.div_1_l. Qed.
 
 Lemma Zmod_1_l: forall a, 1 < a ->  1 mod a = 1.
-Proof.
-  intros; symmetry; apply Zmod_unique with 0; auto with zarith.
-Qed.
+Proof. exact Z.mod_1_l. Qed.
 
 Lemma Z_div_same_full : forall a:Z, a<>0 -> a/a = 1.
-Proof.
-  intros; symmetry; apply Zdiv_unique_full with 0; auto with *; red; omega.
-Qed.
+Proof. exact Z.div_same. Qed.
 
 Lemma Z_mod_same_full : forall a, a mod a = 0.
-Proof.
-  destruct a; intros; symmetry.
-  compute; auto.
-  apply Zmod_unique with 1; auto with *; omega with *.
-  apply Zmod_unique_full with 1; auto with *; red; omega with *.
-Qed.
+Proof. intros. zero_or_not a. apply Z.mod_same; auto. Qed.
 
 Lemma Z_mod_mult : forall a b, (a*b) mod b = 0.
-Proof.
-  intros a b; destruct (Z_eq_dec b 0) as [Hb|Hb].
-  subst; simpl; rewrite Zmod_0_r; auto.
-  symmetry; apply Zmod_unique_full with a; [ red; omega | ring ].
-Qed.
+Proof. intros. zero_or_not b. apply Z.mod_mul. auto. Qed.
 
 Lemma Z_div_mult_full : forall a b:Z, b <> 0 -> (a*b)/b = a.
-Proof.
-  intros; symmetry; apply Zdiv_unique_full with 0; auto with zarith;
-   [ red; omega | ring].
-Qed.
+Proof. exact Z.div_mul. Qed.
 
 (** * Order results about Zmod and Zdiv *)
 
 (* Division of positive numbers is positive. *)
 
 Lemma Z_div_pos: forall a b, b > 0 -> 0 <= a -> 0 <= a/b.
-Proof.
-  intros.
-  rewrite (Z_div_mod_eq a b H) in H0.
-  assert (H1:=Z_mod_lt a b H).
-  destruct (Z_lt_le_dec (a/b) 0); auto.
-  assert (b*(a/b) <= -b).
-   replace (-b) with (b*-1); [ | ring].
-   apply Zmult_le_compat_l; auto with zarith.
-  omega.
-Qed.
+Proof. intros. apply Z.div_pos; auto with zarith. Qed.
 
 Lemma Z_div_ge0: forall a b, b > 0 -> a >= 0 -> a/b >=0.
 Proof.
@@ -489,145 +451,68 @@ Qed.
     the division is strictly decreasing. *)
 
 Lemma Z_div_lt : forall a b:Z, b >= 2 -> a > 0 -> a/b < a.
-Proof.
-  intros. cut (b > 0); [ intro Hb | omega ].
-  generalize (Z_div_mod a b Hb).
-  cut (a >= 0); [ intro Ha | omega ].
-  generalize (Z_div_ge0 a b Hb Ha).
-  unfold Zdiv in |- *; case (Zdiv_eucl a b); intros q r H1 [H2 H3].
-  cut (a >= 2 * q -> q < a); [ intro h; apply h; clear h | intros; omega ].
-  apply Zge_trans with (b * q).
-  omega.
-  auto with zarith.
-Qed.
-
+Proof. intros. apply Z.div_lt; auto with zarith. Qed.
 
 (** A division of a small number by a bigger one yields zero. *)
 
 Theorem Zdiv_small: forall a b, 0 <= a < b -> a/b = 0.
-Proof.
-  intros a b H; apply sym_equal; apply Zdiv_unique with a; auto with zarith.
-Qed.
+Proof. exact Z.div_small. Qed.
 
 (** Same situation, in term of modulo: *)
 
 Theorem Zmod_small: forall a n, 0 <= a < n -> a mod n = a.
-Proof.
-  intros a b H; apply sym_equal; apply Zmod_unique with 0; auto with zarith.
-Qed.
+Proof. exact Z.mod_small. Qed.
 
 (** [Zge] is compatible with a positive division. *)
 
 Lemma Z_div_ge : forall a b c:Z, c > 0 -> a >= b -> a/c >= b/c.
-Proof.
-  intros a b c cPos aGeb.
-  generalize (Z_div_mod_eq a c cPos).
-  generalize (Z_mod_lt a c cPos).
-  generalize (Z_div_mod_eq b c cPos).
-  generalize (Z_mod_lt b c cPos).
-  intros.
-  elim (Z_ge_lt_dec (a / c) (b / c)); trivial.
-  intro.
-  absurd (b - a >= 1).
-  omega.
-  replace (b-a) with (c * (b/c-a/c) + b mod c - a mod c) by
-    (symmetry; pattern a at 1; rewrite H2; pattern b at 1; rewrite H0; ring).
-  assert (c * (b / c - a / c) >= c * 1).
-  apply Zmult_ge_compat_l.
-  omega.
-  omega.
-  assert (c * 1 = c).
-  ring.
-  omega.
-Qed.
+Proof. intros. apply Zle_ge. apply Z.div_le_mono; auto with zarith. Qed.
 
 (** Same, with [Zle]. *)
 
 Lemma Z_div_le : forall a b c:Z, c > 0 -> a <= b -> a/c <= b/c.
-Proof.
-  intros a b c H H0.
-  apply Zge_le.
-  apply Z_div_ge; auto with *.
-Qed.
+Proof. intros. apply Z.div_le_mono; auto with zarith. Qed.
 
 (** With our choice of division, rounding of (a/b) is always done toward bottom: *)
 
 Lemma Z_mult_div_ge : forall a b:Z, b > 0 -> b*(a/b) <= a.
-Proof.
-  intros a b H; generalize (Z_div_mod_eq a b H) (Z_mod_lt a b H); omega.
-Qed.
+Proof. intros. apply Z.mul_div_le; auto with zarith. Qed.
 
 Lemma Z_mult_div_ge_neg : forall a b:Z, b < 0 -> b*(a/b) >= a.
-Proof.
-  intros a b H.
-  generalize (Z_div_mod_eq_full a _ (Zlt_not_eq _ _ H)) (Z_mod_neg a _ H); omega.
-Qed.
+Proof. intros. apply Zle_ge. apply Z.mul_div_ge; auto with zarith. Qed.
 
 (** The previous inequalities are exact iff the modulo is zero. *)
 
 Lemma Z_div_exact_full_1 : forall a b:Z, a = b*(a/b) -> a mod b = 0.
-Proof.
-  intros; destruct (Z_eq_dec b 0) as [Hb|Hb].
-  subst b; simpl in *; subst; auto.
-  generalize (Z_div_mod_eq_full a b Hb); omega.
-Qed.
+Proof. intros a b. zero_or_not b. rewrite Z.div_exact; auto. Qed.
 
 Lemma Z_div_exact_full_2 : forall a b:Z, b <> 0 -> a mod b = 0 -> a = b*(a/b).
-Proof.
-  intros; generalize (Z_div_mod_eq_full a b H); omega.
-Qed.
+Proof. intros; rewrite Z.div_exact; auto. Qed.
 
 (** A modulo cannot grow beyond its starting point. *)
 
 Theorem Zmod_le: forall a b, 0 < b -> 0 <= a -> a mod b <= a.
-Proof.
-  intros a b H1 H2; case (Zle_or_lt b a); intros H3.
-  case (Z_mod_lt a b); auto with zarith.
-  rewrite Zmod_small; auto with zarith.
-Qed.
+Proof. intros. apply Z.mod_le; auto. Qed.
 
 (** Some additionnal inequalities about Zdiv. *)
 
 Theorem Zdiv_lt_upper_bound:
   forall a b q, 0 < b -> a < q*b -> a/b < q.
-Proof.
-  intros a b q H1 H2.
-  apply Zmult_lt_reg_r with b; auto with zarith.
-  apply Zle_lt_trans with (2 := H2).
-  pattern a at 2; rewrite (Z_div_mod_eq a b); auto with zarith.
-  rewrite (Zmult_comm b); case (Z_mod_lt a b); auto with zarith.
-Qed.
+Proof. intros a b q; rewrite Zmult_comm; apply Z.div_lt_upper_bound. Qed.
 
 Theorem Zdiv_le_upper_bound:
   forall a b q, 0 < b -> a <= q*b -> a/b <= q.
-Proof.
-  intros.
-  rewrite <- (Z_div_mult_full q b); auto with zarith.
-  apply Z_div_le; auto with zarith.
-Qed.
+Proof. intros a b q; rewrite Zmult_comm; apply Z.div_le_upper_bound. Qed.
 
 Theorem Zdiv_le_lower_bound:
   forall a b q, 0 < b -> q*b <= a -> q <= a/b.
-Proof.
-  intros.
-  rewrite <- (Z_div_mult_full q b); auto with zarith.
-  apply Z_div_le; auto with zarith.
-Qed.
+Proof. intros a b q; rewrite Zmult_comm; apply Z.div_le_lower_bound. Qed.
 
 (** A division of respect opposite monotonicity for the divisor *)
 
 Lemma Zdiv_le_compat_l: forall p q r, 0 <= p -> 0 < q < r ->
     p / r <= p / q.
-Proof.
-  intros p q r H H1.
-  apply Zdiv_le_lower_bound; auto with zarith.
-  rewrite Zmult_comm.
-  pattern p at 2; rewrite (Z_div_mod_eq p r); auto with zarith.
-  apply Zle_trans with (r * (p / r)); auto with zarith.
-  apply Zmult_le_compat_r; auto with zarith.
-  apply Zdiv_le_lower_bound; auto with zarith.
-  case (Z_mod_lt p r); auto with zarith.
-Qed.
+Proof. intros; apply Z.div_le_compat_l; auto with zarith. Qed.
 
 Theorem Zdiv_sgn: forall a b,
   0 <= Zsgn (a/b) * Zsgn a * Zsgn b.
@@ -640,215 +525,91 @@ Qed.
 (** * Relations between usual operations and Zmod and Zdiv *)
 
 Lemma Z_mod_plus_full : forall a b c:Z, (a + b * c) mod c = a mod c.
-Proof.
-  intros; destruct (Z_eq_dec c 0) as [Hc|Hc].
-  subst; do 2 rewrite Zmod_0_r; auto.
-  symmetry; apply Zmod_unique_full with (a/c+b); auto with zarith.
-  red; generalize (Z_mod_lt a c)(Z_mod_neg a c); omega.
-  rewrite Zmult_plus_distr_r, Zmult_comm.
-  generalize (Z_div_mod_eq_full a c Hc); omega.
-Qed.
+Proof. intros. zero_or_not c. apply Z.mod_add; auto. Qed.
 
 Lemma Z_div_plus_full : forall a b c:Z, c <> 0 -> (a + b * c) / c = a / c + b.
-Proof.
-  intro; symmetry.
-  apply Zdiv_unique_full with (a mod c); auto with zarith.
-  red; generalize (Z_mod_lt a c)(Z_mod_neg a c); omega.
-  rewrite Zmult_plus_distr_r, Zmult_comm.
-  generalize (Z_div_mod_eq_full a c H); omega.
-Qed.
+Proof. exact Z.div_add. Qed.
 
 Theorem Z_div_plus_full_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b.
-Proof.
-  intros a b c H; rewrite Zplus_comm; rewrite Z_div_plus_full;
-  try apply Zplus_comm; auto with zarith.
-Qed.
+Proof. exact Z.div_add_l. Qed.
 
 (** [Zopp] and [Zdiv], [Zmod].
     Due to the choice of convention for our Euclidean division,
     some of the relations about [Zopp] and divisions are rather complex. *)
 
 Lemma Zdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b.
-Proof.
-  intros [|a|a] [|b|b]; try reflexivity; unfold Zdiv; simpl;
-  destruct (Zdiv_eucl_POS a (Zpos b)); destruct z0; try reflexivity.
-Qed.
+Proof. intros. zero_or_not b. apply Z.div_opp_opp; auto. Qed.
 
 Lemma Zmod_opp_opp : forall a b:Z, (-a) mod (-b) = - (a mod b).
-Proof.
-  intros; destruct (Z_eq_dec b 0) as [Hb|Hb].
-  subst; do 2 rewrite Zmod_0_r; auto.
-  intros; symmetry.
-  apply Zmod_unique_full with ((-a)/(-b)); auto.
-  generalize (Z_mod_remainder a b Hb); destruct 1; [right|left]; omega.
-  rewrite Zdiv_opp_opp.
-  pattern a at 1; rewrite (Z_div_mod_eq_full a b Hb); ring.
-Qed.
+Proof. intros. zero_or_not b. apply Z.mod_opp_opp; auto. Qed.
 
 Lemma Z_mod_zero_opp_full : forall a b:Z, a mod b = 0 -> (-a) mod b = 0.
-Proof.
-  intros; destruct (Z_eq_dec b 0) as [Hb|Hb].
-  subst; rewrite Zmod_0_r; auto.
-  rewrite Z_div_exact_full_2 with a b; auto.
-  replace (- (b * (a / b))) with (0 + - (a / b) * b).
-  rewrite Z_mod_plus_full; auto.
-  ring.
-Qed.
+Proof. intros. zero_or_not b. apply Z.mod_opp_l_z; auto. Qed.
 
 Lemma Z_mod_nz_opp_full : forall a b:Z, a mod b <> 0 ->
  (-a) mod b = b - (a mod b).
-Proof.
-  intros.
-  assert (b<>0) by (contradict H; subst; rewrite Zmod_0_r; auto).
-  symmetry; apply Zmod_unique_full with (-1-a/b); auto.
-  generalize (Z_mod_remainder a b H0); destruct 1; [left|right]; omega.
-  rewrite Zmult_minus_distr_l.
-  pattern a at 1; rewrite (Z_div_mod_eq_full a b H0); ring.
-Qed.
+Proof. intros. zero_or_not b. apply Z.mod_opp_l_nz; auto. Qed.
 
 Lemma Z_mod_zero_opp_r : forall a b:Z, a mod b = 0 -> a mod (-b) = 0.
-Proof.
-  intros.
-  rewrite <- (Zopp_involutive a).
-  rewrite Zmod_opp_opp.
-  rewrite Z_mod_zero_opp_full; auto.
-Qed.
+Proof. intros. zero_or_not b. apply Z.mod_opp_r_z; auto. Qed.
 
 Lemma Z_mod_nz_opp_r : forall a b:Z, a mod b <> 0 ->
  a mod (-b) = (a mod b) - b.
-Proof.
-  intros.
-  pattern a at 1; rewrite <- (Zopp_involutive a).
-  rewrite Zmod_opp_opp.
-  rewrite Z_mod_nz_opp_full; auto; omega.
-Qed.
+Proof. intros. zero_or_not b. apply Z.mod_opp_r_nz; auto. Qed.
 
 Lemma Z_div_zero_opp_full : forall a b:Z, a mod b = 0 -> (-a)/b = -(a/b).
-Proof.
-  intros; destruct (Z_eq_dec b 0) as [Hb|Hb].
-  subst; do 2 rewrite Zdiv_0_r; auto.
-  symmetry; apply Zdiv_unique_full with 0; auto.
-  red; omega.
-  pattern a at 1; rewrite (Z_div_mod_eq_full a b Hb).
-  rewrite H; ring.
-Qed.
+Proof. intros. zero_or_not b. apply Z.div_opp_l_z; auto. Qed.
 
 Lemma Z_div_nz_opp_full : forall a b:Z, a mod b <> 0 ->
  (-a)/b = -(a/b)-1.
-Proof.
-  intros.
-  assert (b<>0) by (contradict H; subst; rewrite Zmod_0_r; auto).
-  symmetry; apply Zdiv_unique_full with (b-a mod b); auto.
-  generalize (Z_mod_remainder a b H0); destruct 1; [left|right]; omega.
-  pattern a at 1; rewrite (Z_div_mod_eq_full a b H0); ring.
-Qed.
+Proof. intros a b. zero_or_not b. intros; rewrite Z.div_opp_l_nz; auto. Qed.
 
 Lemma Z_div_zero_opp_r : forall a b:Z, a mod b = 0 -> a/(-b) = -(a/b).
-Proof.
-  intros.
-  pattern a at 1; rewrite <- (Zopp_involutive a).
-  rewrite Zdiv_opp_opp.
-  rewrite Z_div_zero_opp_full; auto.
-Qed.
+Proof. intros. zero_or_not b. apply Z.div_opp_r_z; auto. Qed.
 
 Lemma Z_div_nz_opp_r : forall a b:Z, a mod b <> 0 ->
  a/(-b) = -(a/b)-1.
-Proof.
-  intros.
-  pattern a at 1; rewrite <- (Zopp_involutive a).
-  rewrite Zdiv_opp_opp.
-  rewrite Z_div_nz_opp_full; auto; omega.
-Qed.
+Proof. intros a b. zero_or_not b. intros; rewrite Z.div_opp_r_nz; auto. Qed.
 
 (** Cancellations. *)
 
 Lemma Zdiv_mult_cancel_r : forall a b c:Z,
  c <> 0 -> (a*c)/(b*c) = a/b.
-Proof.
-assert (X: forall a b c, b > 0 -> c > 0 -> (a*c) / (b*c) = a / b).
- intros a b c Hb Hc.
- symmetry.
- apply Zdiv_unique with ((a mod b)*c); auto with zarith.
- destruct (Z_mod_lt a b Hb); split.
- apply Zmult_le_0_compat; auto with zarith.
- apply Zmult_lt_compat_r; auto with zarith.
- pattern a at 1; rewrite (Z_div_mod_eq a b Hb); ring.
-intros a b c Hc.
-destruct (Z_dec b 0) as [Hb|Hb].
-destruct Hb as [Hb|Hb]; destruct (not_Zeq_inf _ _ Hc); auto with *.
-rewrite <- (Zdiv_opp_opp a), <- (Zmult_opp_opp b), <-(Zmult_opp_opp a);
- auto with *.
-rewrite <- (Zdiv_opp_opp a), <- Zdiv_opp_opp, Zopp_mult_distr_l,
- Zopp_mult_distr_l; auto with *.
-rewrite <- Zdiv_opp_opp, Zopp_mult_distr_r, Zopp_mult_distr_r; auto with *.
-rewrite Hb; simpl; do 2 rewrite Zdiv_0_r; auto.
-Qed.
+Proof. intros. zero_or_not b. apply Z.div_mul_cancel_r; auto. Qed.
 
 Lemma Zdiv_mult_cancel_l : forall a b c:Z,
  c<>0 -> (c*a)/(c*b) = a/b.
 Proof.
-  intros.
-  rewrite (Zmult_comm c a); rewrite (Zmult_comm c b).
-  apply Zdiv_mult_cancel_r; auto.
+ intros. rewrite (Zmult_comm c b); zero_or_not b.
+ rewrite (Zmult_comm b c). apply Z.div_mul_cancel_l; auto.
 Qed.
 
 Lemma Zmult_mod_distr_l: forall a b c,
   (c*a) mod (c*b) = c * (a mod b).
 Proof.
-  intros; destruct (Z_eq_dec c 0) as [Hc|Hc].
-  subst; simpl; rewrite Zmod_0_r; auto.
-  destruct (Z_eq_dec b 0) as [Hb|Hb].
-  subst; repeat rewrite Zmult_0_r || rewrite Zmod_0_r; auto.
-  assert (c*b <> 0).
-   contradict Hc; eapply Zmult_integral_l; eauto.
-  rewrite (Zplus_minus_eq _ _ _ (Z_div_mod_eq_full (c*a) (c*b) H)).
-  rewrite (Zplus_minus_eq _ _ _ (Z_div_mod_eq_full a b Hb)).
-  rewrite Zdiv_mult_cancel_l; auto with zarith.
-  ring.
+ intros. zero_or_not c. rewrite (Zmult_comm c b); zero_or_not b.
+ rewrite (Zmult_comm b c). apply Z.mul_mod_distr_l; auto.
 Qed.
 
 Lemma Zmult_mod_distr_r: forall a b c,
   (a*c) mod (b*c) = (a mod b) * c.
 Proof.
-  intros; repeat rewrite (fun x => (Zmult_comm x c)).
-  apply Zmult_mod_distr_l; auto.
+ intros. zero_or_not b. rewrite (Zmult_comm b c); zero_or_not c.
+ rewrite (Zmult_comm c b). apply Z.mul_mod_distr_r; auto.
 Qed.
 
 (** Operations modulo. *)
 
 Theorem Zmod_mod: forall a n, (a mod n) mod n = a mod n.
-Proof.
-  intros; destruct (Z_eq_dec n 0) as [Hb|Hb].
-  subst; do 2 rewrite Zmod_0_r; auto.
-  pattern a at 2; rewrite (Z_div_mod_eq_full a n); auto with zarith.
-  rewrite Zplus_comm; rewrite Zmult_comm.
-  apply sym_equal; apply Z_mod_plus_full; auto with zarith.
-Qed.
+Proof. intros. zero_or_not n. apply Z.mod_mod; auto. Qed.
 
 Theorem Zmult_mod: forall a b n,
  (a * b) mod n = ((a mod n) * (b mod n)) mod n.
-Proof.
-  intros; destruct (Z_eq_dec n 0) as [Hb|Hb].
-  subst; do 2 rewrite Zmod_0_r; auto.
-  pattern a at 1; rewrite (Z_div_mod_eq_full a n); auto with zarith.
-  pattern b at 1; rewrite (Z_div_mod_eq_full b n); auto with zarith.
-  set (A:=a mod n); set (B:=b mod n); set (A':=a/n); set (B':=b/n).
-  replace ((n*A' + A) * (n*B' + B))
-   with (A*B + (A'*B+B'*A+n*A'*B')*n) by ring.
-  apply Z_mod_plus_full; auto with zarith.
-Qed.
+Proof. intros. zero_or_not n. apply Z.mul_mod; auto. Qed.
 
 Theorem Zplus_mod: forall a b n,
  (a + b) mod n = (a mod n + b mod n) mod n.
-Proof.
-  intros; destruct (Z_eq_dec n 0) as [Hb|Hb].
-  subst; do 2 rewrite Zmod_0_r; auto.
-  pattern a at 1; rewrite (Z_div_mod_eq_full a n); auto with zarith.
-  pattern b at 1; rewrite (Z_div_mod_eq_full b n); auto with zarith.
-  replace ((n * (a / n) + a mod n) + (n * (b / n) + b mod n))
-     with ((a mod n + b mod n) + (a / n + b / n) * n) by ring.
-  apply Z_mod_plus_full; auto with zarith.
-Qed.
+Proof. intros. zero_or_not n. apply Z.add_mod; auto. Qed.
 
 Theorem Zminus_mod: forall a b n,
  (a - b) mod n = (a mod n - b mod n) mod n.
@@ -954,30 +715,8 @@ Qed.
 
 Lemma Zdiv_Zdiv : forall a b c, 0<=b -> 0<=c -> (a/b)/c = a/(b*c).
 Proof.
-  intros a b c Hb Hc.
-  destruct (Zle_lt_or_eq _ _ Hb); [ | subst; rewrite Zdiv_0_r, Zdiv_0_r, Zdiv_0_l; auto].
-  destruct (Zle_lt_or_eq _ _ Hc); [ | subst; rewrite Zmult_0_r, Zdiv_0_r, Zdiv_0_r; auto].
-  pattern a at 2;rewrite (Z_div_mod_eq_full a b);auto with zarith.
-  pattern (a/b) at 2;rewrite (Z_div_mod_eq_full (a/b) c);auto with zarith.
-  replace (b * (c * (a / b / c) + (a / b) mod c) + a mod b) with
-    ((a / b / c)*(b * c)  + (b * ((a / b) mod c) + a mod b)) by ring.
-  rewrite Z_div_plus_full_l; auto with zarith.
-  rewrite (Zdiv_small (b * ((a / b) mod c) + a mod b)).
-  ring.
-  split.
-  apply Zplus_le_0_compat;auto with zarith.
-  apply Zmult_le_0_compat;auto with zarith.
-  destruct (Z_mod_lt (a/b) c);auto with zarith.
-  destruct (Z_mod_lt a b);auto with zarith.
-  apply Zle_lt_trans with (b * ((a / b) mod c) + (b-1)).
-  destruct (Z_mod_lt a b);auto with zarith.
-  apply Zle_lt_trans with (b * (c-1) + (b - 1)).
-  apply Zplus_le_compat;auto with zarith.
-  destruct (Z_mod_lt (a/b) c);auto with zarith.
-  replace (b * (c - 1) + (b - 1)) with (b*c-1);try ring;auto with zarith.
-  intro H1;
-  assert (H2: c <> 0) by auto with zarith;
-  rewrite (Zmult_integral_l _ _ H2 H1) in H; auto with zarith.
+ intros. zero_or_not b. rewrite Zmult_comm. zero_or_not c.
+ rewrite Zmult_comm. apply Z.div_div; auto with zarith.
 Qed.
 
 (** Unfortunately, the previous result isn't always true on negative numbers.
@@ -988,41 +727,13 @@ Qed.
 Theorem Zdiv_mult_le:
  forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b.
 Proof.
-  intros a b c H1 H2 H3.
-  destruct (Zle_lt_or_eq _ _ H2);
-   [ | subst; rewrite Zdiv_0_r, Zdiv_0_r, Zmult_0_r; auto].
-  case (Z_mod_lt a b); auto with zarith; intros Hu1 Hu2.
-  case (Z_mod_lt c b); auto with zarith; intros Hv1 Hv2.
-  apply Zmult_le_reg_r with b; auto with zarith.
-  rewrite <- Zmult_assoc.
-  replace (a / b * b) with (a - a mod b).
-  replace (c * a / b * b) with (c * a - (c * a) mod b).
-  rewrite Zmult_minus_distr_l.
-  unfold Zminus; apply Zplus_le_compat_l.
-  match goal with |- - ?X <= -?Y => assert (Y <= X); auto with zarith end.
-  apply Zle_trans with ((c mod b) * (a mod b)); auto with zarith.
-  rewrite Zmult_mod; auto with zarith.
-  apply (Zmod_le ((c mod b) * (a mod b)) b); auto with zarith.
-  apply Zmult_le_compat_r; auto with zarith.
-  apply (Zmod_le c b); auto.
-  pattern (c * a) at 1; rewrite (Z_div_mod_eq (c * a) b); try ring;
-    auto with zarith.
-  pattern a at 1; rewrite (Z_div_mod_eq a b); try ring; auto with zarith.
-Qed.
+ intros. zero_or_not b. apply Z.div_mul_le; auto with zarith. Qed.
 
 (** Zmod is related to divisibility (see more in Znumtheory) *)
 
 Lemma Zmod_divides : forall a b, b<>0 ->
  (a mod b = 0 <-> exists c, a = b*c).
-Proof.
- split; intros.
- exists (a/b).
- pattern a at 1; rewrite (Z_div_mod_eq_full a b); auto with zarith.
- destruct H0 as [c Hc].
- symmetry.
- apply Zmod_unique_full with c; auto with zarith.
- red; omega with *.
-Qed.
+Proof. exact Z.mod_divides. Qed.
 
 (** * Compatibility *)