Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(* -*- coding: utf-8 -*- *)
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Euclidean Division

Initial Contribution by Claude Marché and Xavier Urbain

Require Export ZArith_base.
Require Import Zbool Omega ZArithRing Zcomplements Setoid Morphisms.
Local Open Scope Z_scope.

The definition of the division is now in BinIntDef, the initial specifications and properties are in BinInt.

Notation Zdiv_eucl_POS := Z.pos_div_eucl (only parsing).
Notation Zmod := Z.modulo (only parsing).

Notation Z_div_mod_eq_full := Z.div_mod (only parsing).
Notation Zmod_POS_bound := Z.pos_div_eucl_bound (only parsing).
Notation Zmod_pos_bound := Z.mod_pos_bound (only parsing).
Notation Zmod_neg_bound := Z.mod_neg_bound (only parsing).

Main division theorems

NB: many things are stated twice for compatibility reasons

Lemma Z_div_mod_POS :
  forall b:Z,
    b > 0 ->
    forall a:positive,
      let (q, r) := Z.pos_div_eucl a b in Zpos a = b * q + r /\ 0 <= r < b.forall b : Z,
b > 0 ->
forall a : positive,
let (q, r) := Z.pos_div_eucl a b in
Z.pos a = b * q + r /\ 0 <= r < b
Proof.forall b : Z,
b > 0 ->
forall a : positive,
let (q, r) := Z.pos_div_eucl a b in
Z.pos a = b * q + r /\ 0 <= r < b
 intros b Hb a.b:Z
Hb:b > 0
a:positive
let (q, r) := Z.pos_div_eucl a b in
Z.pos a = b * q + r /\ 0 <= r < b Z.swap_greater.b:Z
Hb:0 < b
a:positive
let (q, r) := Z.pos_div_eucl a b in
Z.pos a = b * q + r /\ 0 <= r < b
 generalize (Z.pos_div_eucl_eq a b Hb) (Z.pos_div_eucl_bound a b Hb).b:Z
Hb:0 < b
a:positive
(let (q, r) := Z.pos_div_eucl a b in
 Z.pos a = q * b + r) ->
0 <= snd (Z.pos_div_eucl a b) < b ->
let (q, r) := Z.pos_div_eucl a b in
Z.pos a = b * q + r /\ 0 <= r < b
 destruct Z.pos_div_eucl.b:Z
Hb:0 < b
a:positive
z, z0:Z
Z.pos a = z * b + z0 ->
0 <= snd (z, z0) < b ->
Z.pos a = b * z + z0 /\ 0 <= z0 < b rewrite Z.mul_comm.b:Z
Hb:0 < b
a:positive
z, z0:Z
Z.pos a = b * z + z0 ->
0 <= snd (z, z0) < b ->
Z.pos a = b * z + z0 /\ 0 <= z0 < b auto.
Qed.

Theorem Z_div_mod a b :
  b > 0 ->
  let (q, r) := Z.div_eucl a b in a = b * q + r /\ 0 <= r < b.a, b:Z
b > 0 ->
let (q, r) := Z.div_eucl a b in
a = b * q + r /\ 0 <= r < b
Proof.a, b:Z
b > 0 ->
let (q, r) := Z.div_eucl a b in
a = b * q + r /\ 0 <= r < b
 Z.swap_greater.a, b:Z
0 < b ->
let (q, r) := Z.div_eucl a b in
a = b * q + r /\ 0 <= r < b intros Hb.a, b:Z
Hb:0 < b
let (q, r) := Z.div_eucl a b in
a = b * q + r /\ 0 <= r < b
 assert (Hb' : b<>0) by (now destruct b).a, b:Z
Hb:0 < b
Hb':b <> 0
let (q, r) := Z.div_eucl a b in
a = b * q + r /\ 0 <= r < b
 generalize (Z.div_eucl_eq a b Hb') (Z.mod_pos_bound a b Hb).a, b:Z
Hb:0 < b
Hb':b <> 0
(let (q, r) := Z.div_eucl a b in a = b * q + r) ->
0 <= a mod b < b ->
let (q, r) := Z.div_eucl a b in
a = b * q + r /\ 0 <= r < b
 unfold Z.modulo.a, b:Z
Hb:0 < b
Hb':b <> 0
(let (q, r) := Z.div_eucl a b in a = b * q + r) ->
0 <= (let (_, r) := Z.div_eucl a b in r) < b ->
let (q, r) := Z.div_eucl a b in
a = b * q + r /\ 0 <= r < b destruct Z.div_eucl.a, b:Z
Hb:0 < b
Hb':b <> 0
z, z0:Z
a = b * z + z0 ->
0 <= z0 < b -> a = b * z + z0 /\ 0 <= z0 < b auto.
Qed.

For stating the fully general result, let's give a short name to the condition on the remainder.

Definition Remainder r b :=  0 <= r < b \/ b < r <= 0.

Another equivalent formulation:

Definition Remainder_alt r b :=  Z.abs r < Z.abs b /\ Z.sgn r <> - Z.sgn b.

(* In the last formulation, [ Z.sgn r <> - Z.sgn b ] is less nice than saying
    [ Z.sgn r = Z.sgn b ], but at least it works even when [r] is null. *)

Lemma Remainder_equiv : forall r b, Remainder r b <-> Remainder_alt r b.forall r b : Z, Remainder r b <-> Remainder_alt r b
Proof.forall r b : Z, Remainder r b <-> Remainder_alt r b
 intros; unfold Remainder, Remainder_alt; omega with *.
Qed.

Hint Unfold Remainder : core.

Now comes the fully general result about Euclidean division.

Theorem Z_div_mod_full a b :
  b <> 0 ->
  let (q, r) := Z.div_eucl a b in a = b * q + r /\ Remainder r b.a, b:Z
b <> 0 ->
let (q, r) := Z.div_eucl a b in
a = b * q + r /\ Remainder r b
Proof.a, b:Z
b <> 0 ->
let (q, r) := Z.div_eucl a b in
a = b * q + r /\ Remainder r b
 intros Hb.a, b:Z
Hb:b <> 0
let (q, r) := Z.div_eucl a b in
a = b * q + r /\ Remainder r b
 generalize (Z.div_eucl_eq a b Hb)
  (Z.mod_pos_bound a b) (Z.mod_neg_bound a b).a, b:Z
Hb:b <> 0
(let (q, r) := Z.div_eucl a b in a = b * q + r) ->
(0 < b -> 0 <= a mod b < b) ->
(b < 0 -> b < a mod b <= 0) ->
let (q, r) := Z.div_eucl a b in
a = b * q + r /\ Remainder r b
 unfold Z.modulo.a, b:Z
Hb:b <> 0
(let (q, r) := Z.div_eucl a b in a = b * q + r) ->
(0 < b -> 0 <= (let (_, r) := Z.div_eucl a b in r) < b) ->
(b < 0 -> b < (let (_, r) := Z.div_eucl a b in r) <= 0) ->
let (q, r) := Z.div_eucl a b in
a = b * q + r /\ Remainder r b destruct Z.div_eucl as (q,r).a, b:Z
Hb:b <> 0
q, r:Z
a = b * q + r ->
(0 < b -> 0 <= r < b) ->
(b < 0 -> b < r <= 0) ->
a = b * q + r /\ Remainder r b
 intros EQ POS NEG.a, b:Z
Hb:b <> 0
q, r:Z
EQ:a = b * q + r
POS:0 < b -> 0 <= r < b
NEG:b < 0 -> b < r <= 0
a = b * q + r /\ Remainder r b
 split; auto.a, b:Z
Hb:b <> 0
q, r:Z
EQ:a = b * q + r
POS:0 < b -> 0 <= r < b
NEG:b < 0 -> b < r <= 0
Remainder r b
 red; destruct b.a:Z
Hb:0 <> 0
q, r:Z
EQ:a = 0 * q + r
POS:0 < 0 -> 0 <= r < 0
NEG:0 < 0 -> 0 < r <= 0
0 <= r < 0 \/ 0 < r <= 0
a:Z
p:positive
Hb:Z.pos p <> 0
q, r:Z
EQ:a = Z.pos p * q + r
POS:0 < Z.pos p -> 0 <= r < Z.pos p
NEG:Z.pos p < 0 -> Z.pos p < r <= 0
0 <= r < Z.pos p \/ Z.pos p < r <= 0
a:Z
p:positive
Hb:Z.neg p <> 0
q, r:Z
EQ:a = Z.neg p * q + r
POS:0 < Z.neg p -> 0 <= r < Z.neg p
NEG:Z.neg p < 0 -> Z.neg p < r <= 0
0 <= r < Z.neg p \/ Z.neg p < r <= 0
  now destruct Hb.a:Z
p:positive
Hb:Z.pos p <> 0
q, r:Z
EQ:a = Z.pos p * q + r
POS:0 < Z.pos p -> 0 <= r < Z.pos p
NEG:Z.pos p < 0 -> Z.pos p < r <= 0
0 <= r < Z.pos p \/ Z.pos p < r <= 0
a:Z
p:positive
Hb:Z.neg p <> 0
q, r:Z
EQ:a = Z.neg p * q + r
POS:0 < Z.neg p -> 0 <= r < Z.neg p
NEG:Z.neg p < 0 -> Z.neg p < r <= 0
0 <= r < Z.neg p \/ Z.neg p < r <= 0 left; now apply POS.a:Z
p:positive
Hb:Z.neg p <> 0
q, r:Z
EQ:a = Z.neg p * q + r
POS:0 < Z.neg p -> 0 <= r < Z.neg p
NEG:Z.neg p < 0 -> Z.neg p < r <= 0
0 <= r < Z.neg p \/ Z.neg p < r <= 0 right; now apply NEG.
Qed.

The same results as before, stated separately in terms of Z.div and Z.modulo

Lemma Z_mod_remainder a b : b<>0 -> Remainder (a mod b) b.a, b:Z
b <> 0 -> Remainder (a mod b) b
Proof.a, b:Z
b <> 0 -> Remainder (a mod b) b
  unfold Z.modulo; intros Hb; generalize (Z_div_mod_full a b Hb); auto.a, b:Z
Hb:b <> 0
(let (q, r) := Z.div_eucl a b in
 a = b * q + r /\ Remainder r b) ->
Remainder (let (_, r) := Z.div_eucl a b in r) b
  destruct Z.div_eucl; tauto.
Qed.

Lemma Z_mod_lt a b : b > 0 -> 0 <= a mod b < b.a, b:Z
b > 0 -> 0 <= a mod b < b
Proof (fun Hb => Z.mod_pos_bound a b (Z.gt_lt _ _ Hb)).

Lemma Z_mod_neg a b : b < 0 -> b < a mod b <= 0.a, b:Z
b < 0 -> b < a mod b <= 0
Proof (Z.mod_neg_bound a b).

Lemma Z_div_mod_eq a b : b > 0 -> a = b*(a/b) + (a mod b).a, b:Z
b > 0 -> a = b * (a / b) + a mod b
Proof.a, b:Z
b > 0 -> a = b * (a / b) + a mod b
  intros Hb; apply Z.div_mod; auto with zarith.
Qed.

Lemma Zmod_eq_full a b : b<>0 -> a mod b = a - (a/b)*b.a, b:Z
b <> 0 -> a mod b = a - a / b * b
Proof.a, b:Z
b <> 0 -> a mod b = a - a / b * b intros.a, b:Z
H:b <> 0
a mod b = a - a / b * b rewrite Z.mul_comm.a, b:Z
H:b <> 0
a mod b = a - b * (a / b) now apply Z.mod_eq. Qed.

Lemma Zmod_eq a b : b>0 -> a mod b = a - (a/b)*b.a, b:Z
b > 0 -> a mod b = a - a / b * b
Proof.a, b:Z
b > 0 -> a mod b = a - a / b * b intros.a, b:Z
H:b > 0
a mod b = a - a / b * b apply Zmod_eq_full.a, b:Z
H:b > 0
b <> 0 now destruct b. Qed.

Existence theorem

Theorem Zdiv_eucl_exist : forall (b:Z)(Hb:b>0)(a:Z),
 {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < b}.forall b : Z,
b > 0 ->
forall a : Z,
{qr : Z * Z |
let (q, r) := qr in a = b * q + r /\ 0 <= r < b}
Proof.forall b : Z,
b > 0 ->
forall a : Z,
{qr : Z * Z |
let (q, r) := qr in a = b * q + r /\ 0 <= r < b}
  intros b Hb a.b:Z
Hb:b > 0
a:Z
{qr : Z * Z |
let (q, r) := qr in a = b * q + r /\ 0 <= r < b}
  exists (Z.div_eucl a b).b:Z
Hb:b > 0
a:Z
let (q, r) := Z.div_eucl a b in
a = b * q + r /\ 0 <= r < b
  exact (Z_div_mod a b Hb).
Qed.

Arguments Zdiv_eucl_exist : default implicits.

Uniqueness theorems

Theorem Zdiv_mod_unique b q1 q2 r1 r2 :
  0 <= r1 < Z.abs b -> 0 <= r2 < Z.abs b ->
  b*q1+r1 = b*q2+r2 -> q1=q2 /\ r1=r2.b, q1, q2, r1, r2:Z
0 <= r1 < Z.abs b ->
0 <= r2 < Z.abs b ->
b * q1 + r1 = b * q2 + r2 -> q1 = q2 /\ r1 = r2
Proof.b, q1, q2, r1, r2:Z
0 <= r1 < Z.abs b ->
0 <= r2 < Z.abs b ->
b * q1 + r1 = b * q2 + r2 -> q1 = q2 /\ r1 = r2
intros Hr1 Hr2 H.b, q1, q2, r1, r2:Z
Hr1:0 <= r1 < Z.abs b
Hr2:0 <= r2 < Z.abs b
H:b * q1 + r1 = b * q2 + r2
q1 = q2 /\ r1 = r2 rewrite <- (Z.abs_sgn b), <- !Z.mul_assoc in H.b, q1, q2, r1, r2:Z
Hr1:0 <= r1 < Z.abs b
Hr2:0 <= r2 < Z.abs b
H:Z.abs b * (Z.sgn b * q1) + r1 =
Z.abs b * (Z.sgn b * q2) + r2
q1 = q2 /\ r1 = r2
destruct (Z.div_mod_unique (Z.abs b) (Z.sgn b * q1) (Z.sgn b * q2) r1 r2); auto.b, q1, q2, r1, r2:Z
Hr1:0 <= r1 < Z.abs b
Hr2:0 <= r2 < Z.abs b
H:Z.abs b * (Z.sgn b * q1) + r1 =
Z.abs b * (Z.sgn b * q2) + r2
H0:Z.sgn b * q1 = Z.sgn b * q2
H1:r1 = r2
q1 = q2 /\ r1 = r2
split; trivial.b, q1, q2, r1, r2:Z
Hr1:0 <= r1 < Z.abs b
Hr2:0 <= r2 < Z.abs b
H:Z.abs b * (Z.sgn b * q1) + r1 =
Z.abs b * (Z.sgn b * q2) + r2
H0:Z.sgn b * q1 = Z.sgn b * q2
H1:r1 = r2
q1 = q2
apply Z.mul_cancel_l with (Z.sgn b); trivial.b, q1, q2, r1, r2:Z
Hr1:0 <= r1 < Z.abs b
Hr2:0 <= r2 < Z.abs b
H:Z.abs b * (Z.sgn b * q1) + r1 =
Z.abs b * (Z.sgn b * q2) + r2
H0:Z.sgn b * q1 = Z.sgn b * q2
H1:r1 = r2
Z.sgn b <> 0
rewrite Z.sgn_null_iff, <- Z.abs_0_iff.b, q1, q2, r1, r2:Z
Hr1:0 <= r1 < Z.abs b
Hr2:0 <= r2 < Z.abs b
H:Z.abs b * (Z.sgn b * q1) + r1 =
Z.abs b * (Z.sgn b * q2) + r2
H0:Z.sgn b * q1 = Z.sgn b * q2
H1:r1 = r2
Z.abs b <> 0 destruct Hr1; Z.order.
Qed.

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.forall b q1 q2 r1 r2 : Z,
Remainder r1 b ->
Remainder r2 b ->
b * q1 + r1 = b * q2 + r2 -> q1 = q2 /\ r1 = r2
Proof Z.div_mod_unique.

Theorem Zdiv_unique_full:
 forall a b q r, Remainder r b ->
   a = b*q + r -> q = a/b.forall a b q r : Z,
Remainder r b -> a = b * q + r -> q = a / b
Proof Z.div_unique.

Theorem Zdiv_unique:
 forall a b q r, 0 <= r < b ->
   a = b*q + r -> q = a/b.forall a b q r : Z,
0 <= r < b -> a = b * q + r -> q = a / b
Proof.forall a b q r : Z,
0 <= r < b -> a = b * q + r -> q = a / b 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.forall a b q r : Z,
Remainder r b -> a = b * q + r -> r = a mod b
Proof Z.mod_unique.

Theorem Zmod_unique:
 forall a b q r, 0 <= r < b ->
  a = b*q + r -> r = a mod b.forall a b q r : Z,
0 <= r < b -> a = b * q + r -> r = a mod b
Proof.forall a b q r : Z,
0 <= r < b -> a = b * q + r -> r = a mod b intros; eapply Zmod_unique_full; eauto. Qed.

Basic values of divisions and modulo.

Lemma Zmod_0_l: forall a, 0 mod a = 0.forall a : Z, 0 mod a = 0
Proof.forall a : Z, 0 mod a = 0
  destruct a; simpl; auto.
Qed.

Lemma Zmod_0_r: forall a, a mod 0 = 0.forall a : Z, a mod 0 = 0
Proof.forall a : Z, a mod 0 = 0
  destruct a; simpl; auto.
Qed.

Lemma Zdiv_0_l: forall a, 0/a = 0.forall a : Z, 0 / a = 0
Proof.forall a : Z, 0 / a = 0
  destruct a; simpl; auto.
Qed.

Lemma Zdiv_0_r: forall a, a/0 = 0.forall a : Z, a / 0 = 0
Proof.forall a : Z, a / 0 = 0
  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.forall a : Z, a mod 1 = 0
Proof.forall a : Z, a mod 1 = 0 intros.a:Z
a mod 1 = 0 zero_or_not a.a:Z
n:a <> 0
a mod 1 = 0 apply Z.mod_1_r. Qed.

Lemma Zdiv_1_r: forall a, a/1 = a.forall a : Z, a / 1 = a
Proof.forall a : Z, a / 1 = a intros.a:Z
a / 1 = a zero_or_not a.a:Z
n:a <> 0
a / 1 = 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.forall a : Z, 1 < a -> 1 / a = 0
Proof Z.div_1_l.

Lemma Zmod_1_l: forall a, 1 < a ->  1 mod a = 1.forall a : Z, 1 < a -> 1 mod a = 1
Proof Z.mod_1_l.

Lemma Z_div_same_full : forall a:Z, a<>0 -> a/a = 1.forall a : Z, a <> 0 -> a / a = 1
Proof Z.div_same.

Lemma Z_mod_same_full : forall a, a mod a = 0.forall a : Z, a mod a = 0
Proof.forall a : Z, a mod a = 0 intros.a:Z
a mod a = 0 zero_or_not a.a:Z
n:a <> 0
a mod a = 0 apply Z.mod_same; auto. Qed.

Lemma Z_mod_mult : forall a b, (a*b) mod b = 0.forall a b : Z, (a * b) mod b = 0
Proof.forall a b : Z, (a * b) mod b = 0 intros.a, b:Z
(a * b) mod b = 0 zero_or_not b.a, b:Z
n:b <> 0
(a * b) mod b = 0 apply Z.mod_mul.a, b:Z
n:b <> 0
b <> 0 auto. Qed.

Lemma Z_div_mult_full : forall a b:Z, b <> 0 -> (a*b)/b = a.forall a b : Z, b <> 0 -> a * b / b = a
Proof Z.div_mul.

Order results about Z.modulo and Z.div

(* Division of positive numbers is positive. *)

Lemma Z_div_pos: forall a b, b > 0 -> 0 <= a -> 0 <= a/b.forall a b : Z, b > 0 -> 0 <= a -> 0 <= a / b
Proof.forall a b : Z, b > 0 -> 0 <= a -> 0 <= a / b intros.a, b:Z
H:b > 0
H0:0 <= a
0 <= a / b apply Z.div_pos; auto with zarith. Qed.

Lemma Z_div_ge0: forall a b, b > 0 -> a >= 0 -> a/b >=0.forall a b : Z, b > 0 -> a >= 0 -> a / b >= 0
Proof.forall a b : Z, b > 0 -> a >= 0 -> a / b >= 0
  intros; generalize (Z_div_pos a b H); auto with zarith.
Qed.

As soon as the divisor is greater or equal than 2, the division is strictly decreasing.

Lemma Z_div_lt : forall a b:Z, b >= 2 -> a > 0 -> a/b < a.forall a b : Z, b >= 2 -> a > 0 -> a / b < a
Proof.forall a b : Z, b >= 2 -> a > 0 -> a / b < a intros.a, b:Z
H:b >= 2
H0:a > 0
a / b < a 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.forall a b : Z, 0 <= a < b -> a / b = 0
Proof Z.div_small.

Same situation, in term of modulo:

Theorem Zmod_small: forall a n, 0 <= a < n -> a mod n = a.forall a n : Z, 0 <= a < n -> a mod n = a
Proof Z.mod_small.

Z.ge is compatible with a positive division.

Lemma Z_div_ge : forall a b c:Z, c > 0 -> a >= b -> a/c >= b/c.forall a b c : Z, c > 0 -> a >= b -> a / c >= b / c
Proof.forall a b c : Z, c > 0 -> a >= b -> a / c >= b / c intros.a, b, c:Z
H:c > 0
H0:a >= b
a / c >= b / c apply Z.le_ge.a, b, c:Z
H:c > 0
H0:a >= b
b / c <= a / c apply Z.div_le_mono; auto with zarith. Qed.

Same, with Z.le.

Lemma Z_div_le : forall a b c:Z, c > 0 -> a <= b -> a/c <= b/c.forall a b c : Z, c > 0 -> a <= b -> a / c <= b / c
Proof.forall a b c : Z, c > 0 -> a <= b -> a / c <= b / c intros.a, b, c:Z
H:c > 0
H0:a <= b
a / c <= b / c 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.forall a b : Z, b > 0 -> b * (a / b) <= a
Proof.forall a b : Z, b > 0 -> b * (a / b) <= a intros.a, b:Z
H:b > 0
b * (a / b) <= a 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.forall a b : Z, b < 0 -> b * (a / b) >= a
Proof.forall a b : Z, b < 0 -> b * (a / b) >= a intros.a, b:Z
H:b < 0
b * (a / b) >= a apply Z.le_ge.a, b:Z
H:b < 0
a <= b * (a / b) 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.forall a b : Z, a = b * (a / b) -> a mod b = 0
Proof.forall a b : Z, a = b * (a / b) -> a mod b = 0 intros a b.a, b:Z
a = b * (a / b) -> a mod b = 0 zero_or_not b.a, b:Z
n:b <> 0
a = b * (a / b) -> a mod b = 0 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).forall a b : Z,
b <> 0 -> a mod b = 0 -> a = b * (a / b)
Proof.forall a b : Z,
b <> 0 -> a mod b = 0 -> a = b * (a / b) 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.forall a b : Z, 0 < b -> 0 <= a -> a mod b <= a
Proof.forall a b : Z, 0 < b -> 0 <= a -> a mod b <= a intros.a, b:Z
H:0 < b
H0:0 <= a
a mod b <= a apply Z.mod_le; auto. Qed.

Some additional inequalities about Z.div.

Theorem Zdiv_lt_upper_bound:
  forall a b q, 0 < b -> a < q*b -> a/b < q.forall a b q : Z, 0 < b -> a < q * b -> a / b < q
Proof.forall a b q : Z, 0 < b -> a < q * b -> a / b < q intros a b q; rewrite Z.mul_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.forall a b q : Z, 0 < b -> a <= q * b -> a / b <= q
Proof.forall a b q : Z, 0 < b -> a <= q * b -> a / b <= q intros a b q; rewrite Z.mul_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.forall a b q : Z, 0 < b -> q * b <= a -> q <= a / b
Proof.forall a b q : Z, 0 < b -> q * b <= a -> q <= a / b intros a b q; rewrite Z.mul_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.forall p q r : Z,
0 <= p -> 0 < q < r -> p / r <= p / q
Proof.forall p q r : Z,
0 <= p -> 0 < q < r -> p / r <= p / q intros; apply Z.div_le_compat_l; auto with zarith. Qed.

Theorem Zdiv_sgn: forall a b,
  0 <= Z.sgn (a/b) * Z.sgn a * Z.sgn b.forall a b : Z, 0 <= Z.sgn (a / b) * Z.sgn a * Z.sgn b
Proof.forall a b : Z, 0 <= Z.sgn (a / b) * Z.sgn a * Z.sgn b
  destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith;
  generalize (Z.div_pos (Zpos a) (Zpos b)); unfold Z.div, Z.div_eucl;
  destruct Z.pos_div_eucl as (q,r); destruct r; omega with *.
Qed.

Relations between usual operations and Z.modulo and Z.div

Lemma Z_mod_plus_full : forall a b c:Z, (a + b * c) mod c = a mod c.forall a b c : Z, (a + b * c) mod c = a mod c
Proof.forall a b c : Z, (a + b * c) mod c = a mod c intros.a, b, c:Z
(a + b * c) mod c = a mod c zero_or_not c.a, b, c:Z
n:c <> 0
(a + b * c) mod c = a mod 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.forall a b c : Z,
c <> 0 -> (a + b * c) / c = a / c + b
Proof Z.div_add.

Theorem Z_div_plus_full_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b.forall a b c : Z,
b <> 0 -> (a * b + c) / b = a + c / b
Proof Z.div_add_l.

Z.opp and Z.div, Z.modulo. Due to the choice of convention for our Euclidean division, some of the relations about Z.opp and divisions are rather complex.

Lemma Zdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b.forall a b : Z, - a / - b = a / b
Proof.forall a b : Z, - a / - b = a / b intros.a, b:Z
- a / - b = a / b zero_or_not b.a, b:Z
n:b <> 0
- a / - b = a / b apply Z.div_opp_opp; auto. Qed.

Lemma Zmod_opp_opp : forall a b:Z, (-a) mod (-b) = - (a mod b).forall a b : Z, - a mod - b = - (a mod b)
Proof.forall a b : Z, - a mod - b = - (a mod b) intros.a, b:Z
- a mod - b = - (a mod b) zero_or_not b.a, b:Z
n:b <> 0
- a mod - b = - (a mod 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.forall a b : Z, a mod b = 0 -> - a mod b = 0
Proof.forall a b : Z, a mod b = 0 -> - a mod b = 0 intros.a, b:Z
H:a mod b = 0
- a mod b = 0 zero_or_not b.a, b:Z
H:a mod b = 0
n:b <> 0
- a mod b = 0 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).forall a b : Z,
a mod b <> 0 -> - a mod b = b - a mod b
Proof.forall a b : Z,
a mod b <> 0 -> - a mod b = b - a mod b intros.a, b:Z
H:a mod b <> 0
- a mod b = b - a mod b zero_or_not b.a, b:Z
H:a mod b <> 0
n:b <> 0
- a mod b = b - a mod 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.forall a b : Z, a mod b = 0 -> a mod - b = 0
Proof.forall a b : Z, a mod b = 0 -> a mod - b = 0 intros.a, b:Z
H:a mod b = 0
a mod - b = 0 zero_or_not b.a, b:Z
H:a mod b = 0
n:b <> 0
a mod - b = 0 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.forall a b : Z,
a mod b <> 0 -> a mod - b = a mod b - b
Proof.forall a b : Z,
a mod b <> 0 -> a mod - b = a mod b - b intros.a, b:Z
H:a mod b <> 0
a mod - b = a mod b - b zero_or_not b.a, b:Z
H:a mod b <> 0
n:b <> 0
a mod - b = a mod b - 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).forall a b : Z, a mod b = 0 -> - a / b = - (a / b)
Proof.forall a b : Z, a mod b = 0 -> - a / b = - (a / b) intros.a, b:Z
H:a mod b = 0
- a / b = - (a / b) zero_or_not b.a, b:Z
H:a mod b = 0
n:b <> 0
- a / b = - (a / 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.forall a b : Z,
a mod b <> 0 -> - a / b = - (a / b) - 1
Proof.forall a b : Z,
a mod b <> 0 -> - a / b = - (a / b) - 1 intros a b.a, b:Z
a mod b <> 0 -> - a / b = - (a / b) - 1 zero_or_not b.a, b:Z
n:b <> 0
a mod b <> 0 -> - a / b = - (a / b) - 1 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).forall a b : Z, a mod b = 0 -> a / - b = - (a / b)
Proof.forall a b : Z, a mod b = 0 -> a / - b = - (a / b) intros.a, b:Z
H:a mod b = 0
a / - b = - (a / b) zero_or_not b.a, b:Z
H:a mod b = 0
n:b <> 0
a / - b = - (a / 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.forall a b : Z,
a mod b <> 0 -> a / - b = - (a / b) - 1
Proof.forall a b : Z,
a mod b <> 0 -> a / - b = - (a / b) - 1 intros a b.a, b:Z
a mod b <> 0 -> a / - b = - (a / b) - 1 zero_or_not b.a, b:Z
n:b <> 0
a mod b <> 0 -> a / - b = - (a / b) - 1 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.forall a b c : Z, c <> 0 -> a * c / (b * c) = a / b
Proof.forall a b c : Z, c <> 0 -> a * c / (b * c) = a / b intros.a, b, c:Z
H:c <> 0
a * c / (b * c) = a / b zero_or_not b.a, b, c:Z
H:c <> 0
n:b <> 0
a * c / (b * c) = a / 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.forall a b c : Z, c <> 0 -> c * a / (c * b) = a / b
Proof.forall a b c : Z, c <> 0 -> c * a / (c * b) = a / b
 intros.a, b, c:Z
H:c <> 0
c * a / (c * b) = a / b rewrite (Z.mul_comm c b); zero_or_not b.a, b, c:Z
H:c <> 0
n:b <> 0
c * a / (b * c) = a / b
 rewrite (Z.mul_comm b c).a, b, c:Z
H:c <> 0
n:b <> 0
c * a / (c * b) = a / b 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).forall a b c : Z, (c * a) mod (c * b) = c * (a mod b)
Proof.forall a b c : Z, (c * a) mod (c * b) = c * (a mod b)
 intros.a, b, c:Z
(c * a) mod (c * b) = c * (a mod b) zero_or_not c.a, b, c:Z
n:c <> 0
(c * a) mod (c * b) = c * (a mod b) rewrite (Z.mul_comm c b); zero_or_not b.a, b, c:Z
n:c <> 0
n0:b <> 0
(c * a) mod (b * c) = c * (a mod b)
 rewrite (Z.mul_comm b c).a, b, c:Z
n:c <> 0
n0:b <> 0
(c * a) mod (c * b) = c * (a mod b) 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.forall a b c : Z, (a * c) mod (b * c) = a mod b * c
Proof.forall a b c : Z, (a * c) mod (b * c) = a mod b * c
 intros.a, b, c:Z
(a * c) mod (b * c) = a mod b * c zero_or_not b.a, b, c:Z
n:b <> 0
(a * c) mod (b * c) = a mod b * c rewrite (Z.mul_comm b c); zero_or_not c.a, b, c:Z
n:b <> 0
n0:c <> 0
(a * c) mod (c * b) = a mod b * c
 rewrite (Z.mul_comm c b).a, b, c:Z
n:b <> 0
n0:c <> 0
(a * c) mod (b * c) = a mod b * c apply Z.mul_mod_distr_r; auto.
Qed.

Operations modulo.

Theorem Zmod_mod: forall a n, (a mod n) mod n = a mod n.forall a n : Z, (a mod n) mod n = a mod n
Proof.forall a n : Z, (a mod n) mod n = a mod n intros.a, n:Z
(a mod n) mod n = a mod n zero_or_not n.a, n:Z
n0:n <> 0
(a mod n) mod n = a mod 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.forall a b n : Z,
(a * b) mod n = (a mod n * (b mod n)) mod n
Proof.forall a b n : Z,
(a * b) mod n = (a mod n * (b mod n)) mod n intros.a, b, n:Z
(a * b) mod n = (a mod n * (b mod n)) mod n zero_or_not n.a, b, n:Z
n0:n <> 0
(a * b) mod n = (a mod n * (b mod n)) mod 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.forall a b n : Z,
(a + b) mod n = (a mod n + b mod n) mod n
Proof.forall a b n : Z,
(a + b) mod n = (a mod n + b mod n) mod n intros.a, b, n:Z
(a + b) mod n = (a mod n + b mod n) mod n zero_or_not n.a, b, n:Z
n0:n <> 0
(a + b) mod n = (a mod n + b mod n) mod 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.forall a b n : Z,
(a - b) mod n = (a mod n - b mod n) mod n
Proof.forall a b n : Z,
(a - b) mod n = (a mod n - b mod n) mod n
  intros.a, b, n:Z
(a - b) mod n = (a mod n - b mod n) mod n
  replace (a - b) with (a + (-1) * b); auto with zarith.a, b, n:Z
(a + -1 * b) mod n = (a mod n - b mod n) mod n
  replace (a mod n - b mod n) with (a mod n + (-1) * (b mod n)); auto with zarith.a, b, n:Z
(a + -1 * b) mod n = (a mod n + -1 * (b mod n)) mod n
  rewrite Zplus_mod.a, b, n:Z
(a mod n + (-1 * b) mod n) mod n =
(a mod n + -1 * (b mod n)) mod n
  rewrite Zmult_mod.a, b, n:Z
(a mod n + (-1 mod n * (b mod n)) mod n) mod n =
(a mod n + -1 * (b mod n)) mod n
  rewrite Zplus_mod with (b:=(-1) * (b mod n)).a, b, n:Z
(a mod n + (-1 mod n * (b mod n)) mod n) mod n =
((a mod n) mod n + (-1 * (b mod n)) mod n) mod n
  rewrite Zmult_mod.a, b, n:Z
(a mod n +
 ((-1 mod n) mod n * ((b mod n) mod n)) mod n) mod n =
((a mod n) mod n + (-1 * (b mod n)) mod n) mod n
  rewrite Zmult_mod with (b:= b mod n).a, b, n:Z
(a mod n +
 ((-1 mod n) mod n * ((b mod n) mod n)) mod n) mod n =
((a mod n) mod n +
 (-1 mod n * ((b mod n) mod n)) mod n) mod n
  repeat rewrite Zmod_mod; auto.
Qed.

Lemma Zplus_mod_idemp_l: forall a b n, (a mod n + b) mod n = (a + b) mod n.forall a b n : Z, (a mod n + b) mod n = (a + b) mod n
Proof.forall a b n : Z, (a mod n + b) mod n = (a + b) mod n
  intros; rewrite Zplus_mod, Zmod_mod, <- Zplus_mod; auto.
Qed.

Lemma Zplus_mod_idemp_r: forall a b n, (b + a mod n) mod n = (b + a) mod n.forall a b n : Z, (b + a mod n) mod n = (b + a) mod n
Proof.forall a b n : Z, (b + a mod n) mod n = (b + a) mod n
  intros; rewrite Zplus_mod, Zmod_mod, <- Zplus_mod; auto.
Qed.

Lemma Zminus_mod_idemp_l: forall a b n, (a mod n - b) mod n = (a - b) mod n.forall a b n : Z, (a mod n - b) mod n = (a - b) mod n
Proof.forall a b n : Z, (a mod n - b) mod n = (a - b) mod n
  intros; rewrite Zminus_mod, Zmod_mod, <- Zminus_mod; auto.
Qed.

Lemma Zminus_mod_idemp_r: forall a b n, (a - b mod n) mod n = (a - b) mod n.forall a b n : Z, (a - b mod n) mod n = (a - b) mod n
Proof.forall a b n : Z, (a - b mod n) mod n = (a - b) mod n
  intros; rewrite Zminus_mod, Zmod_mod, <- Zminus_mod; auto.
Qed.

Lemma Zmult_mod_idemp_l: forall a b n, (a mod n * b) mod n = (a * b) mod n.forall a b n : Z, (a mod n * b) mod n = (a * b) mod n
Proof.forall a b n : Z, (a mod n * b) mod n = (a * b) mod n
  intros; rewrite Zmult_mod, Zmod_mod, <- Zmult_mod; auto.
Qed.

Lemma Zmult_mod_idemp_r: forall a b n, (b * (a mod n)) mod n = (b * a) mod n.forall a b n : Z,
(b * (a mod n)) mod n = (b * a) mod n
Proof.forall a b n : Z,
(b * (a mod n)) mod n = (b * a) mod n
  intros; rewrite Zmult_mod, Zmod_mod, <- Zmult_mod; auto.
Qed.

For a specific number N, equality modulo N is hence a nice setoid equivalence, compatible with +, - and ×.

Section EqualityModulo.
Variable N:Z.

Definition eqm a b := (a mod N = b mod N).
Infix "==" := eqm (at level 70).

Lemma eqm_refl : forall a, a == a.N:Z
forall a : Z, a == a
Proof.N:Z
forall a : Z, a == a unfold eqm; auto. Qed.

Lemma eqm_sym : forall a b, a == b -> b == a.N:Z
forall a b : Z, a == b -> b == a
Proof.N:Z
forall a b : Z, a == b -> b == a unfold eqm; auto. Qed.

Lemma eqm_trans : forall a b c,
  a == b -> b == c -> a == c.N:Z
forall a b c : Z, a == b -> b == c -> a == c
Proof.N:Z
forall a b c : Z, a == b -> b == c -> a == c unfold eqm; eauto with *. Qed.

Instance eqm_setoid : Equivalence eqm.N:Z
Equivalence eqm
Proof.N:Z
Equivalence eqm
 constructor; [exact eqm_refl | exact eqm_sym | exact eqm_trans].
Qed.

Instance Zplus_eqm : Proper (eqm ==> eqm ==> eqm) Z.add.N:Z
Proper (eqm ==> eqm ==> eqm) Z.add
Proof.N:Z
Proper (eqm ==> eqm ==> eqm) Z.add
  unfold eqm; repeat red; intros.N, x, y:Z
H:x mod N = y mod N
x0, y0:Z
H0:x0 mod N = y0 mod N
(x + x0) mod N = (y + y0) mod N rewrite Zplus_mod, H, H0, <- Zplus_mod; auto.
Qed.

Instance Zminus_eqm : Proper (eqm ==> eqm ==> eqm) Z.sub.N:Z
Proper (eqm ==> eqm ==> eqm) Z.sub
Proof.N:Z
Proper (eqm ==> eqm ==> eqm) Z.sub
  unfold eqm; repeat red; intros.N, x, y:Z
H:x mod N = y mod N
x0, y0:Z
H0:x0 mod N = y0 mod N
(x - x0) mod N = (y - y0) mod N rewrite Zminus_mod, H, H0, <- Zminus_mod; auto.
Qed.

Instance Zmult_eqm : Proper (eqm ==> eqm ==> eqm) Z.mul.N:Z
Proper (eqm ==> eqm ==> eqm) Z.mul
Proof.N:Z
Proper (eqm ==> eqm ==> eqm) Z.mul
  unfold eqm; repeat red; intros.N, x, y:Z
H:x mod N = y mod N
x0, y0:Z
H0:x0 mod N = y0 mod N
(x * x0) mod N = (y * y0) mod N rewrite Zmult_mod, H, H0, <- Zmult_mod; auto.
Qed.

Instance Zopp_eqm : Proper (eqm ==> eqm) Z.opp.N:Z
Proper (eqm ==> eqm) Z.opp
Proof.N:Z
Proper (eqm ==> eqm) Z.opp
  intros x y H.N, x, y:Z
H:x == y
- x == - y change ((-x)==(-y)) with ((0-x)==(0-y)).N, x, y:Z
H:x == y
0 - x == 0 - y now rewrite H.
Qed.

Lemma Zmod_eqm : forall a, (a mod N) == a.N:Z
forall a : Z, a mod N == a
Proof.N:Z
forall a : Z, a mod N == a
  intros; exact (Zmod_mod a N).
Qed.

(* NB: Z.modulo and Z.div are not morphisms with respect to eqm.
    For instance, let (==) be (eqm 2). Then we have (3 == 1) but:
    ~ (3 mod 3 == 1 mod 3)
    ~ (1 mod 3 == 1 mod 1)
    ~ (3/3 == 1/3)
    ~ (1/3 == 1/1)
*)

End EqualityModulo.

Lemma Zdiv_Zdiv : forall a b c, 0<=b -> 0<=c -> (a/b)/c = a/(b*c).forall a b c : Z,
0 <= b -> 0 <= c -> a / b / c = a / (b * c)
Proof.forall a b c : Z,
0 <= b -> 0 <= c -> a / b / c = a / (b * c)
 intros.a, b, c:Z
H:0 <= b
H0:0 <= c
a / b / c = a / (b * c) zero_or_not b.a, b, c:Z
H:0 <= b
H0:0 <= c
n:b <> 0
a / b / c = a / (b * c) rewrite Z.mul_comm.a, b, c:Z
H:0 <= b
H0:0 <= c
n:b <> 0
a / b / c = a / (c * b) zero_or_not c.a, b, c:Z
H:0 <= b
H0:0 <= c
n:b <> 0
n0:c <> 0
a / b / c = a / (c * b)
 rewrite Z.mul_comm.a, b, c:Z
H:0 <= b
H0:0 <= c
n:b <> 0
n0:c <> 0
a / b / c = a / (b * c) apply Z.div_div; auto with zarith.
Qed.

Unfortunately, the previous result isn't always true on negative numbers. For instance: 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2)

Lemma Zmod_div : forall a b, a mod b / b = 0.forall a b : Z, a mod b / b = 0
Proof.forall a b : Z, a mod b / b = 0
 intros a b.a, b:Z
a mod b / b = 0
 zero_or_not b.a, b:Z
n:b <> 0
a mod b / b = 0
 auto using Z.mod_div.
Qed.

A last inequality:

Theorem Zdiv_mult_le:
 forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b.forall a b c : Z,
0 <= a -> 0 <= b -> 0 <= c -> c * (a / b) <= c * a / b
Proof.forall a b c : Z,
0 <= a -> 0 <= b -> 0 <= c -> c * (a / b) <= c * a / b
 intros.a, b, c:Z
H:0 <= a
H0:0 <= b
H1:0 <= c
c * (a / b) <= c * a / b zero_or_not b.a, b, c:Z
H:0 <= a
H0:0 <= b
H1:0 <= c
n:b <> 0
c * (a / b) <= c * a / b apply Z.div_mul_le; auto with zarith. Qed.

Z.modulo 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).forall a b : Z,
b <> 0 -> a mod b = 0 <-> (exists c : Z, a = b * c)
Proof.forall a b : Z,
b <> 0 -> a mod b = 0 <-> (exists c : Z, a = b * c)
 intros.a, b:Z
H:b <> 0
a mod b = 0 <-> (exists c : Z, a = b * c) rewrite Z.mod_divide; trivial.a, b:Z
H:b <> 0
(b | a) <-> (exists c : Z, a = b * c)
 split; intros (c,Hc); exists c; subst; auto with zarith.
Qed.

Particular case : dividing by 2 is related with parity

Lemma Zdiv2_div : forall a, Z.div2 a = a/2.forall a : Z, Z.div2 a = a / 2
Proof Z.div2_div.

Lemma Zmod_odd : forall a, a mod 2 = if Z.odd a then 1 else 0.forall a : Z, a mod 2 = (if Z.odd a then 1 else 0)
Proof.forall a : Z, a mod 2 = (if Z.odd a then 1 else 0)
 intros a.a:Z
a mod 2 = (if Z.odd a then 1 else 0) now rewrite <- Z.bit0_odd, <- Z.bit0_mod.
Qed.

Lemma Zmod_even : forall a, a mod 2 = if Z.even a then 0 else 1.forall a : Z, a mod 2 = (if Z.even a then 0 else 1)
Proof.forall a : Z, a mod 2 = (if Z.even a then 0 else 1)
 intros a.a:Z
a mod 2 = (if Z.even a then 0 else 1) rewrite Zmod_odd, Zodd_even_bool.a:Z
(if negb (Z.even a) then 1 else 0) =
(if Z.even a then 0 else 1) now destruct Z.even.
Qed.

Lemma Zodd_mod : forall a, Z.odd a = Zeq_bool (a mod 2) 1.forall a : Z, Z.odd a = Zeq_bool (a mod 2) 1
Proof.forall a : Z, Z.odd a = Zeq_bool (a mod 2) 1
 intros a.a:Z
Z.odd a = Zeq_bool (a mod 2) 1 rewrite Zmod_odd.a:Z
Z.odd a = Zeq_bool (if Z.odd a then 1 else 0) 1 now destruct Z.odd.
Qed.

Lemma Zeven_mod : forall a, Z.even a = Zeq_bool (a mod 2) 0.forall a : Z, Z.even a = Zeq_bool (a mod 2) 0
Proof.forall a : Z, Z.even a = Zeq_bool (a mod 2) 0
 intros a.a:Z
Z.even a = Zeq_bool (a mod 2) 0 rewrite Zmod_even.a:Z
Z.even a = Zeq_bool (if Z.even a then 0 else 1) 0 now destruct Z.even.
Qed.

Compatibility

Weaker results kept only for compatibility

Lemma Z_mod_same : forall a, a > 0 -> a mod a = 0.forall a : Z, a > 0 -> a mod a = 0
Proof.forall a : Z, a > 0 -> a mod a = 0
  intros; apply Z_mod_same_full.
Qed.

Lemma Z_div_same : forall a, a > 0 -> a/a = 1.forall a : Z, a > 0 -> a / a = 1
Proof.forall a : Z, a > 0 -> a / a = 1
  intros; apply Z_div_same_full; auto with zarith.
Qed.

Lemma Z_div_plus : forall a b c:Z, c > 0 -> (a + b * c) / c = a / c + b.forall a b c : Z, c > 0 -> (a + b * c) / c = a / c + b
Proof.forall a b c : Z, c > 0 -> (a + b * c) / c = a / c + b
  intros; apply Z_div_plus_full; auto with zarith.
Qed.

Lemma Z_div_mult : forall a b:Z, b > 0 -> (a*b)/b = a.forall a b : Z, b > 0 -> a * b / b = a
Proof.forall a b : Z, b > 0 -> a * b / b = a
  intros; apply Z_div_mult_full; auto with zarith.
Qed.

Lemma Z_mod_plus : forall a b c:Z, c > 0 -> (a + b * c) mod c = a mod c.forall a b c : Z, c > 0 -> (a + b * c) mod c = a mod c
Proof.forall a b c : Z, c > 0 -> (a + b * c) mod c = a mod c
  intros; apply Z_mod_plus_full; auto with zarith.
Qed.

Lemma Z_div_exact_1 : forall a b:Z, b > 0 -> a = b*(a/b) -> a mod b = 0.forall a b : Z,
b > 0 -> a = b * (a / b) -> a mod b = 0
Proof.forall a b : Z,
b > 0 -> a = b * (a / b) -> a mod b = 0
  intros; apply Z_div_exact_full_1; auto with zarith.
Qed.

Lemma Z_div_exact_2 : forall a b:Z, b > 0 -> a mod b = 0 -> a = b*(a/b).forall a b : Z,
b > 0 -> a mod b = 0 -> a = b * (a / b)
Proof.forall a b : Z,
b > 0 -> a mod b = 0 -> a = b * (a / b)
  intros; apply Z_div_exact_full_2; auto with zarith.
Qed.

Lemma Z_mod_zero_opp : forall a b:Z, b > 0 -> a mod b = 0 -> (-a) mod b = 0.forall a b : Z, b > 0 -> a mod b = 0 -> - a mod b = 0
Proof.forall a b : Z, b > 0 -> a mod b = 0 -> - a mod b = 0
  intros; apply Z_mod_zero_opp_full; auto with zarith.
Qed.

A direct way to compute Z.modulo

Fixpoint Zmod_POS (a : positive) (b : Z) : Z  :=
  match a with
   | xI a' =>
      let r := Zmod_POS a' b in
      let r' := (2 * r + 1) in
      if r' <? b then r' else (r' - b)
   | xO a' =>
      let r := Zmod_POS a' b in
      let r' := (2 * r) in
      if r' <? b then r' else (r' - b)
   | xH => if 2 <=? b then 1 else 0
  end.

Definition Zmod' a b :=
  match a with
   | Z0 => 0
   | Zpos a' =>
      match b with
       | Z0 => 0
       | Zpos _ => Zmod_POS a' b
       | Zneg b' =>
          let r := Zmod_POS a' (Zpos b') in
          match r  with Z0 =>  0 |  _  =>   b + r end
      end
   | Zneg a' =>
      match b with
       | Z0 => 0
       | Zpos _ =>
          let r := Zmod_POS a' b in
          match r with Z0 =>  0 | _  =>  b - r end
       | Zneg b' => - (Zmod_POS a' (Zpos b'))
      end
  end.


Theorem Zmod_POS_correct a b : Zmod_POS a b = snd (Z.pos_div_eucl a b).a:positive
b:Z
Zmod_POS a b = snd (Z.pos_div_eucl a b)
Proof.a:positive
b:Z
Zmod_POS a b = snd (Z.pos_div_eucl a b)
  induction a as [a IH|a IH| ]; simpl; rewrite ?IH.a:positive
b:Z
IH:Zmod_POS a b = snd (Z.pos_div_eucl a b)
(if
  match snd (Z.pos_div_eucl a b) with
  | 0 => 0
  | Z.pos y' => Z.pos y'~0
  | Z.neg y' => Z.neg y'~0
  end + 1 <? b
 then
  match snd (Z.pos_div_eucl a b) with
  | 0 => 0
  | Z.pos y' => Z.pos y'~0
  | Z.neg y' => Z.neg y'~0
  end + 1
 else
  match snd (Z.pos_div_eucl a b) with
  | 0 => 0
  | Z.pos y' => Z.pos y'~0
  | Z.neg y' => Z.neg y'~0
  end + 1 - b) =
snd
  (let (q, r) := Z.pos_div_eucl a b in
   if
    match r with
    | 0 => 0
    | Z.pos y' => Z.pos y'~0
    | Z.neg y' => Z.neg y'~0
    end + 1 <? b
   then
    (match q with
     | 0 => 0
     | Z.pos y' => Z.pos y'~0
     | Z.neg y' => Z.neg y'~0
     end,
    match r with
    | 0 => 0
    | Z.pos y' => Z.pos y'~0
    | Z.neg y' => Z.neg y'~0
    end + 1)
   else
    (match q with
     | 0 => 0
     | Z.pos y' => Z.pos y'~0
     | Z.neg y' => Z.neg y'~0
     end + 1,
    match r with
    | 0 => 0
    | Z.pos y' => Z.pos y'~0
    | Z.neg y' => Z.neg y'~0
    end + 1 - b))
a:positive
b:Z
IH:Zmod_POS a b = snd (Z.pos_div_eucl a b)
(if
  match snd (Z.pos_div_eucl a b) with
  | 0 => 0
  | Z.pos y' => Z.pos y'~0
  | Z.neg y' => Z.neg y'~0
  end <? b
 then
  match snd (Z.pos_div_eucl a b) with
  | 0 => 0
  | Z.pos y' => Z.pos y'~0
  | Z.neg y' => Z.neg y'~0
  end
 else
  match snd (Z.pos_div_eucl a b) with
  | 0 => 0
  | Z.pos y' => Z.pos y'~0
  | Z.neg y' => Z.neg y'~0
  end - b) =
snd
  (let (q, r) := Z.pos_div_eucl a b in
   if
    match r with
    | 0 => 0
    | Z.pos y' => Z.pos y'~0
    | Z.neg y' => Z.neg y'~0
    end <? b
   then
    (match q with
     | 0 => 0
     | Z.pos y' => Z.pos y'~0
     | Z.neg y' => Z.neg y'~0
     end,
    match r with
    | 0 => 0
    | Z.pos y' => Z.pos y'~0
    | Z.neg y' => Z.neg y'~0
    end)
   else
    (match q with
     | 0 => 0
     | Z.pos y' => Z.pos y'~0
     | Z.neg y' => Z.neg y'~0
     end + 1,
    match r with
    | 0 => 0
    | Z.pos y' => Z.pos y'~0
    | Z.neg y' => Z.neg y'~0
    end - b))
b:Z
(if 2 <=? b then 1 else 0) =
snd (if 2 <=? b then (0, 1) else (1, 0))
  destruct (Z.pos_div_eucl a b) as (p,q); simpl;
   case Z.ltb_spec; reflexivity.a:positive
b:Z
IH:Zmod_POS a b = snd (Z.pos_div_eucl a b)
(if
  match snd (Z.pos_div_eucl a b) with
  | 0 => 0
  | Z.pos y' => Z.pos y'~0
  | Z.neg y' => Z.neg y'~0
  end <? b
 then
  match snd (Z.pos_div_eucl a b) with
  | 0 => 0
  | Z.pos y' => Z.pos y'~0
  | Z.neg y' => Z.neg y'~0
  end
 else
  match snd (Z.pos_div_eucl a b) with
  | 0 => 0
  | Z.pos y' => Z.pos y'~0
  | Z.neg y' => Z.neg y'~0
  end - b) =
snd
  (let (q, r) := Z.pos_div_eucl a b in
   if
    match r with
    | 0 => 0
    | Z.pos y' => Z.pos y'~0
    | Z.neg y' => Z.neg y'~0
    end <? b
   then
    (match q with
     | 0 => 0
     | Z.pos y' => Z.pos y'~0
     | Z.neg y' => Z.neg y'~0
     end,
    match r with
    | 0 => 0
    | Z.pos y' => Z.pos y'~0
    | Z.neg y' => Z.neg y'~0
    end)
   else
    (match q with
     | 0 => 0
     | Z.pos y' => Z.pos y'~0
     | Z.neg y' => Z.neg y'~0
     end + 1,
    match r with
    | 0 => 0
    | Z.pos y' => Z.pos y'~0
    | Z.neg y' => Z.neg y'~0
    end - b))
b:Z
(if 2 <=? b then 1 else 0) =
snd (if 2 <=? b then (0, 1) else (1, 0))
  destruct (Z.pos_div_eucl a b) as (p,q); simpl;
   case Z.ltb_spec; reflexivity.b:Z
(if 2 <=? b then 1 else 0) =
snd (if 2 <=? b then (0, 1) else (1, 0))
  case Z.leb_spec; trivial.
Qed.

Theorem Zmod'_correct: forall a b, Zmod' a b = a mod b.forall a b : Z, Zmod' a b = a mod b
Proof.forall a b : Z, Zmod' a b = a mod b
  intros a b; unfold Z.modulo; case a; simpl; auto.a, b:Z
forall p : positive,
match b with
| 0 => 0
| Z.pos _ => Zmod_POS p b
| Z.neg b' =>
    match Zmod_POS p (Z.pos b') with
    | 0 => 0
    | _ => b + Zmod_POS p (Z.pos b')
    end
end =
(let (_, r) :=
   match b with
   | 0 => (0, 0)
   | Z.pos _ => Z.pos_div_eucl p b
   | Z.neg b' =>
       let (q, r) := Z.pos_div_eucl p (Z.pos b') in
       match r with
       | 0 => (- q, 0)
       | _ => (- (q + 1), b + r)
       end
   end in
 r)
a, b:Z
forall p : positive,
match b with
| 0 => 0
| Z.pos _ =>
    match Zmod_POS p b with
    | 0 => 0
    | _ => b - Zmod_POS p b
    end
| Z.neg b' => - Zmod_POS p (Z.pos b')
end =
(let (_, r) :=
   match b with
   | 0 => (0, 0)
   | Z.pos _ =>
       let (q, r) := Z.pos_div_eucl p b in
       match r with
       | 0 => (- q, 0)
       | _ => (- (q + 1), b - r)
       end
   | Z.neg b' =>
       let (q, r) := Z.pos_div_eucl p (Z.pos b') in
       (q, - r)
   end in
 r)
  intros p; case b; simpl; auto.a, b:Z
p:positive
forall p0 : positive,
Zmod_POS p (Z.pos p0) =
(let (_, r) := Z.pos_div_eucl p (Z.pos p0) in r)
a, b:Z
p:positive
forall p0 : positive,
match Zmod_POS p (Z.pos p0) with
| 0 => 0
| _ =>
    match Zmod_POS p (Z.pos p0) with
    | 0 => Z.neg p0
    | Z.pos y' => Z.pos_sub y' p0
    | Z.neg y' => Z.neg (p0 + y')
    end
end =
(let (_, r) :=
   let (q, r) := Z.pos_div_eucl p (Z.pos p0) in
   match r with
   | 0 => (- q, 0)
   | _ =>
       (- (q + 1),
       match r with
       | 0 => Z.neg p0
       | Z.pos y' => Z.pos_sub y' p0
       | Z.neg y' => Z.neg (p0 + y')
       end)
   end in
 r)
a, b:Z
forall p : positive,
match b with
| 0 => 0
| Z.pos _ =>
    match Zmod_POS p b with
    | 0 => 0
    | _ => b - Zmod_POS p b
    end
| Z.neg b' => - Zmod_POS p (Z.pos b')
end =
(let (_, r) :=
   match b with
   | 0 => (0, 0)
   | Z.pos _ =>
       let (q, r) := Z.pos_div_eucl p b in
       match r with
       | 0 => (- q, 0)
       | _ => (- (q + 1), b - r)
       end
   | Z.neg b' =>
       let (q, r) := Z.pos_div_eucl p (Z.pos b') in
       (q, - r)
   end in
 r)
  intros p1; refine (Zmod_POS_correct _ _); auto.a, b:Z
p:positive
forall p0 : positive,
match Zmod_POS p (Z.pos p0) with
| 0 => 0
| _ =>
    match Zmod_POS p (Z.pos p0) with
    | 0 => Z.neg p0
    | Z.pos y' => Z.pos_sub y' p0
    | Z.neg y' => Z.neg (p0 + y')
    end
end =
(let (_, r) :=
   let (q, r) := Z.pos_div_eucl p (Z.pos p0) in
   match r with
   | 0 => (- q, 0)
   | _ =>
       (- (q + 1),
       match r with
       | 0 => Z.neg p0
       | Z.pos y' => Z.pos_sub y' p0
       | Z.neg y' => Z.neg (p0 + y')
       end)
   end in
 r)
a, b:Z
forall p : positive,
match b with
| 0 => 0
| Z.pos _ =>
    match Zmod_POS p b with
    | 0 => 0
    | _ => b - Zmod_POS p b
    end
| Z.neg b' => - Zmod_POS p (Z.pos b')
end =
(let (_, r) :=
   match b with
   | 0 => (0, 0)
   | Z.pos _ =>
       let (q, r) := Z.pos_div_eucl p b in
       match r with
       | 0 => (- q, 0)
       | _ => (- (q + 1), b - r)
       end
   | Z.neg b' =>
       let (q, r) := Z.pos_div_eucl p (Z.pos b') in
       (q, - r)
   end in
 r)
  intros p1; rewrite Zmod_POS_correct; auto.a, b:Z
p, p1:positive
match snd (Z.pos_div_eucl p (Z.pos p1)) with
| 0 => 0
| _ =>
    match snd (Z.pos_div_eucl p (Z.pos p1)) with
    | 0 => Z.neg p1
    | Z.pos y' => Z.pos_sub y' p1
    | Z.neg y' => Z.neg (p1 + y')
    end
end =
(let (_, r) :=
   let (q, r) := Z.pos_div_eucl p (Z.pos p1) in
   match r with
   | 0 => (- q, 0)
   | _ =>
       (- (q + 1),
       match r with
       | 0 => Z.neg p1
       | Z.pos y' => Z.pos_sub y' p1
       | Z.neg y' => Z.neg (p1 + y')
       end)
   end in
 r)
a, b:Z
forall p : positive,
match b with
| 0 => 0
| Z.pos _ =>
    match Zmod_POS p b with
    | 0 => 0
    | _ => b - Zmod_POS p b
    end
| Z.neg b' => - Zmod_POS p (Z.pos b')
end =
(let (_, r) :=
   match b with
   | 0 => (0, 0)
   | Z.pos _ =>
       let (q, r) := Z.pos_div_eucl p b in
       match r with
       | 0 => (- q, 0)
       | _ => (- (q + 1), b - r)
       end
   | Z.neg b' =>
       let (q, r) := Z.pos_div_eucl p (Z.pos b') in
       (q, - r)
   end in
 r)
  case (Z.pos_div_eucl p (Zpos p1)); simpl; intros z1 z2; case z2; auto.a, b:Z
forall p : positive,
match b with
| 0 => 0
| Z.pos _ =>
    match Zmod_POS p b with
    | 0 => 0
    | _ => b - Zmod_POS p b
    end
| Z.neg b' => - Zmod_POS p (Z.pos b')
end =
(let (_, r) :=
   match b with
   | 0 => (0, 0)
   | Z.pos _ =>
       let (q, r) := Z.pos_div_eucl p b in
       match r with
       | 0 => (- q, 0)
       | _ => (- (q + 1), b - r)
       end
   | Z.neg b' =>
       let (q, r) := Z.pos_div_eucl p (Z.pos b') in
       (q, - r)
   end in
 r)
  intros p; case b; simpl; auto.a, b:Z
p:positive
forall p0 : positive,
match Zmod_POS p (Z.pos p0) with
| 0 => 0
| _ =>
    match - Zmod_POS p (Z.pos p0) with
    | 0 => Z.pos p0
    | Z.pos y' => Z.pos (p0 + y')
    | Z.neg y' => Z.pos_sub p0 y'
    end
end =
(let (_, r) :=
   let (q, r) := Z.pos_div_eucl p (Z.pos p0) in
   match r with
   | 0 => (- q, 0)
   | _ =>
       (- (q + 1),
       match - r with
       | 0 => Z.pos p0
       | Z.pos y' => Z.pos (p0 + y')
       | Z.neg y' => Z.pos_sub p0 y'
       end)
   end in
 r)
a, b:Z
p:positive
forall p0 : positive,
- Zmod_POS p (Z.pos p0) =
(let (_, r) :=
   let (q, r) := Z.pos_div_eucl p (Z.pos p0) in
   (q, - r) in
 r)
  intros p1; rewrite Zmod_POS_correct; auto.a, b:Z
p, p1:positive
match snd (Z.pos_div_eucl p (Z.pos p1)) with
| 0 => 0
| _ =>
    match - snd (Z.pos_div_eucl p (Z.pos p1)) with
    | 0 => Z.pos p1
    | Z.pos y' => Z.pos (p1 + y')
    | Z.neg y' => Z.pos_sub p1 y'
    end
end =
(let (_, r) :=
   let (q, r) := Z.pos_div_eucl p (Z.pos p1) in
   match r with
   | 0 => (- q, 0)
   | _ =>
       (- (q + 1),
       match - r with
       | 0 => Z.pos p1
       | Z.pos y' => Z.pos (p1 + y')
       | Z.neg y' => Z.pos_sub p1 y'
       end)
   end in
 r)
a, b:Z
p:positive
forall p0 : positive,
- Zmod_POS p (Z.pos p0) =
(let (_, r) :=
   let (q, r) := Z.pos_div_eucl p (Z.pos p0) in
   (q, - r) in
 r)
  case (Z.pos_div_eucl p (Zpos p1)); simpl; intros z1 z2; case z2; auto.a, b:Z
p:positive
forall p0 : positive,
- Zmod_POS p (Z.pos p0) =
(let (_, r) :=
   let (q, r) := Z.pos_div_eucl p (Z.pos p0) in
   (q, - r) in
 r)
  intros p1; rewrite Zmod_POS_correct; simpl; auto.a, b:Z
p, p1:positive
- snd (Z.pos_div_eucl p (Z.pos p1)) =
(let (_, r) :=
   let (q, r) := Z.pos_div_eucl p (Z.pos p1) in
   (q, - r) in
 r)
  case (Z.pos_div_eucl p (Zpos p1)); auto.
Qed.

Another convention is possible for division by negative numbers:

quotient is always the biggest integer smaller than or equal to a/b

remainder is hence always positive or null.

Theorem Zdiv_eucl_extended :
  forall b:Z,
    b <> 0 ->
    forall a:Z,
      {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b}.forall b : Z,
b <> 0 ->
forall a : Z,
{qr : Z * Z |
let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b}
Proof.forall b : Z,
b <> 0 ->
forall a : Z,
{qr : Z * Z |
let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b}
  intros b Hb a.b:Z
Hb:b <> 0
a:Z
{qr : Z * Z |
let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b}
  destruct (Z_le_gt_dec 0 b) as [Hb'|Hb'].b:Z
Hb:b <> 0
a:Z
Hb':0 <= b
{qr : Z * Z |
let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b}
b:Z
Hb:b <> 0
a:Z
Hb':0 > b
{qr : Z * Z |
let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b}
  -b:Z
Hb:b <> 0
a:Z
Hb':0 <= b
{qr : Z * Z |
let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b} assert (Hb'' : b > 0) by omega.b:Z
Hb:b <> 0
a:Z
Hb':0 <= b
Hb'':b > 0
{qr : Z * Z |
let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b}
    rewrite Z.abs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ].
  -b:Z
Hb:b <> 0
a:Z
Hb':0 > b
{qr : Z * Z |
let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b} assert (Hb'' : - b > 0) by omega.b:Z
Hb:b <> 0
a:Z
Hb':0 > b
Hb'':- b > 0
{qr : Z * Z |
let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b}
    destruct (Zdiv_eucl_exist Hb'' a) as ((q,r),[]).b:Z
Hb:b <> 0
a:Z
Hb':0 > b
Hb'':- b > 0
q, r:Z
H:a = - b * q + r
H0:0 <= r < - b
{qr : Z * Z |
let (q0, r0) := qr in
a = b * q0 + r0 /\ 0 <= r0 < Z.abs b}
    exists (- q, r).b:Z
Hb:b <> 0
a:Z
Hb':0 > b
Hb'':- b > 0
q, r:Z
H:a = - b * q + r
H0:0 <= r < - b
a = b * - q + r /\ 0 <= r < Z.abs b
    split.b:Z
Hb:b <> 0
a:Z
Hb':0 > b
Hb'':- b > 0
q, r:Z
H:a = - b * q + r
H0:0 <= r < - b
a = b * - q + r
b:Z
Hb:b <> 0
a:Z
Hb':0 > b
Hb'':- b > 0
q, r:Z
H:a = - b * q + r
H0:0 <= r < - b
0 <= r < Z.abs b
    +b:Z
Hb:b <> 0
a:Z
Hb':0 > b
Hb'':- b > 0
q, r:Z
H:a = - b * q + r
H0:0 <= r < - b
a = b * - q + r rewrite <- Z.mul_opp_comm; assumption.
    +b:Z
Hb:b <> 0
a:Z
Hb':0 > b
Hb'':- b > 0
q, r:Z
H:a = - b * q + r
H0:0 <= r < - b
0 <= r < Z.abs b rewrite Z.abs_neq; [ assumption | omega ].
Qed.

Arguments Zdiv_eucl_extended : default implicits.

Division and modulo in Z agree with same in nat:

Require Import PeanoNat.

Lemma div_Zdiv (n m: nat): m <> O ->
  Z.of_nat (n / m) = Z.of_nat n / Z.of_nat m.n, m:nat
m <> 0%nat ->
Z.of_nat (n / m) = Z.of_nat n / Z.of_nat m
Proof.n, m:nat
m <> 0%nat ->
Z.of_nat (n / m) = Z.of_nat n / Z.of_nat m
 intros.n, m:nat
H:m <> 0%nat
Z.of_nat (n / m) = Z.of_nat n / Z.of_nat m
 apply (Zdiv_unique _ _ _ (Z.of_nat (n mod m))).n, m:nat
H:m <> 0%nat
0 <= Z.of_nat (n mod m) < Z.of_nat m
n, m:nat
H:m <> 0%nat
Z.of_nat n =
Z.of_nat m * Z.of_nat (n / m) + Z.of_nat (n mod m)
  split.n, m:nat
H:m <> 0%nat
0 <= Z.of_nat (n mod m)
n, m:nat
H:m <> 0%nat
Z.of_nat (n mod m) < Z.of_nat m
n, m:nat
H:m <> 0%nat
Z.of_nat n =
Z.of_nat m * Z.of_nat (n / m) + Z.of_nat (n mod m) auto with zarith.n, m:nat
H:m <> 0%nat
Z.of_nat (n mod m) < Z.of_nat m
n, m:nat
H:m <> 0%nat
Z.of_nat n =
Z.of_nat m * Z.of_nat (n / m) + Z.of_nat (n mod m)
  now apply inj_lt, Nat.mod_upper_bound.n, m:nat
H:m <> 0%nat
Z.of_nat n =
Z.of_nat m * Z.of_nat (n / m) + Z.of_nat (n mod m)
 rewrite <- Nat2Z.inj_mul, <- Nat2Z.inj_add.n, m:nat
H:m <> 0%nat
Z.of_nat n = Z.of_nat (m * (n / m) + n mod m)
 now apply inj_eq, Nat.div_mod.
Qed.

Lemma mod_Zmod (n m: nat): m <> O ->
  Z.of_nat (n mod m) = (Z.of_nat n) mod (Z.of_nat m).n, m:nat
m <> 0%nat ->
Z.of_nat (n mod m) = Z.of_nat n mod Z.of_nat m
Proof.n, m:nat
m <> 0%nat ->
Z.of_nat (n mod m) = Z.of_nat n mod Z.of_nat m
 intros.n, m:nat
H:m <> 0%nat
Z.of_nat (n mod m) = Z.of_nat n mod Z.of_nat m
 apply (Zmod_unique _ _ (Z.of_nat n / Z.of_nat m)).n, m:nat
H:m <> 0%nat
0 <= Z.of_nat (n mod m) < Z.of_nat m
n, m:nat
H:m <> 0%nat
Z.of_nat n =
Z.of_nat m * (Z.of_nat n / Z.of_nat m) +
Z.of_nat (n mod m)
  split.n, m:nat
H:m <> 0%nat
0 <= Z.of_nat (n mod m)
n, m:nat
H:m <> 0%nat
Z.of_nat (n mod m) < Z.of_nat m
n, m:nat
H:m <> 0%nat
Z.of_nat n =
Z.of_nat m * (Z.of_nat n / Z.of_nat m) +
Z.of_nat (n mod m) auto with zarith.n, m:nat
H:m <> 0%nat
Z.of_nat (n mod m) < Z.of_nat m
n, m:nat
H:m <> 0%nat
Z.of_nat n =
Z.of_nat m * (Z.of_nat n / Z.of_nat m) +
Z.of_nat (n mod m)
  now apply inj_lt, Nat.mod_upper_bound.n, m:nat
H:m <> 0%nat
Z.of_nat n =
Z.of_nat m * (Z.of_nat n / Z.of_nat m) +
Z.of_nat (n mod m)
 rewrite <- div_Zdiv, <- Nat2Z.inj_mul, <- Nat2Z.inj_add by trivial.n, m:nat
H:m <> 0%nat
Z.of_nat n = Z.of_nat (m * (n / m) + n mod m)
 now apply inj_eq, Nat.div_mod.
Qed.