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.

(************************************************************************)
(*         *   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)         *)
(************************************************************************)

Require Import Nnat ZArith_base Lia ZArithRing Zdiv Morphisms.

Local Open Scope Z_scope.

This file provides results about the Round-Toward-Zero Euclidean division Z.quotrem, whose projections are Z.quot (noted ÷) and Z.rem.

This division and Z.div agree only on positive numbers. Otherwise, Z.div performs Round-Toward-Bottom (a.k.a Floor).

This Z.quot is compatible with the division of usual programming languages such as Ocaml. In addition, it has nicer properties with respect to opposite and other usual operations.

The definition of this division is now in file BinIntDef, while most of the results about here are now in the main module BinInt.Z, thanks to the generic "Numbers" layer. Remain here:

some compatibility notation for old names.
some extra results with less preconditions (in particular exploiting the arbitrary value of division by 0).

Notation Ndiv_Zquot := N2Z.inj_quot (only parsing).
Notation Nmod_Zrem := N2Z.inj_rem (only parsing).
Notation Z_quot_rem_eq := Z.quot_rem' (only parsing).
Notation Zrem_lt := Z.rem_bound_abs (only parsing).
Notation Z_quot_mult := Z.quot_mul (only parsing).

Particular values taken for a÷0 and (Z.rem a 0). We avise to not rely on these arbitrary values.

Lemma Zquot_0_r a : a ÷ 0 = 0.a:Z
a ÷ 0 = 0
Proof.a:Z
a ÷ 0 = 0 now destruct a. Qed.

Lemma Zrem_0_r a : Z.rem a 0 = a.a:Z
Z.rem a 0 = a
Proof.a:Z
Z.rem a 0 = a now destruct a. Qed.

The following results are expressed without the b<>0 condition whenever possible.

Lemma Zrem_0_l a : Z.rem 0 a = 0.a:Z
Z.rem 0 a = 0
Proof.a:Z
Z.rem 0 a = 0 now destruct a. Qed.

Lemma Zquot_0_l a : 0÷a = 0.a:Z
0 ÷ a = 0
Proof.a:Z
0 ÷ a = 0 now destruct a. Qed.

Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Z.quot_1_r Z.rem_1_r
 : zarith.

Ltac zero_or_not a :=
  destruct (Z.eq_decidable a 0) as [->|?];
  [rewrite ?Zquot_0_l, ?Zrem_0_l, ?Zquot_0_r, ?Zrem_0_r;
   auto with zarith|].

Lemma Z_rem_same a : Z.rem a a = 0.a:Z
Z.rem a a = 0
Proof.a:Z
Z.rem a a = 0 zero_or_not a.a:Z
H:a <> 0
Z.rem a a = 0 now apply Z.rem_same. Qed.

Lemma Z_rem_mult a b : Z.rem (a*b) b = 0.a, b:Z
Z.rem (a * b) b = 0
Proof.a, b:Z
Z.rem (a * b) b = 0 zero_or_not b.a, b:Z
H:b <> 0
Z.rem (a * b) b = 0 now apply Z.rem_mul. Qed.

Division and Opposite

(* The precise equalities that are invalid with "historic" Zdiv. *)

Theorem Zquot_opp_l a b : (-a)÷b = -(a÷b).a, b:Z
- a ÷ b = - (a ÷ b)
Proof.a, b:Z
- a ÷ b = - (a ÷ b) zero_or_not b.a, b:Z
H:b <> 0
- a ÷ b = - (a ÷ b) now apply Z.quot_opp_l. Qed.

Theorem Zquot_opp_r a b : a÷(-b) = -(a÷b).a, b:Z
a ÷ - b = - (a ÷ b)
Proof.a, b:Z
a ÷ - b = - (a ÷ b) zero_or_not b.a, b:Z
H:b <> 0
a ÷ - b = - (a ÷ b) now apply Z.quot_opp_r. Qed.

Theorem Zrem_opp_l a b : Z.rem (-a) b = -(Z.rem a b).a, b:Z
Z.rem (- a) b = - Z.rem a b
Proof.a, b:Z
Z.rem (- a) b = - Z.rem a b zero_or_not b.a, b:Z
H:b <> 0
Z.rem (- a) b = - Z.rem a b now apply Z.rem_opp_l. Qed.

Theorem Zrem_opp_r a b : Z.rem a (-b) = Z.rem a b.a, b:Z
Z.rem a (- b) = Z.rem a b
Proof.a, b:Z
Z.rem a (- b) = Z.rem a b zero_or_not b.a, b:Z
H:b <> 0
Z.rem a (- b) = Z.rem a b now apply Z.rem_opp_r. Qed.

Theorem Zquot_opp_opp a b : (-a)÷(-b) = a÷b.a, b:Z
- a ÷ - b = a ÷ b
Proof.a, b:Z
- a ÷ - b = a ÷ b zero_or_not b.a, b:Z
H:b <> 0
- a ÷ - b = a ÷ b now apply Z.quot_opp_opp. Qed.

Theorem Zrem_opp_opp a b : Z.rem (-a) (-b) = -(Z.rem a b).a, b:Z
Z.rem (- a) (- b) = - Z.rem a b
Proof.a, b:Z
Z.rem (- a) (- b) = - Z.rem a b zero_or_not b.a, b:Z
H:b <> 0
Z.rem (- a) (- b) = - Z.rem a b now apply Z.rem_opp_opp. Qed.

The sign of the remainder is the one of a. Due to the possible nullity of a, a general result is to be stated in the following form:

Theorem Zrem_sgn a b : 0 <= Z.sgn (Z.rem a b) * Z.sgn a.a, b:Z
0 <= Z.sgn (Z.rem a b) * Z.sgn a
Proof.a, b:Z
0 <= Z.sgn (Z.rem a b) * Z.sgn a
  zero_or_not b.a:Z
0 <= Z.sgn a * Z.sgn a
a, b:Z
H:b <> 0
0 <= Z.sgn (Z.rem a b) * Z.sgn a
  -a:Z
0 <= Z.sgn a * Z.sgn a apply Z.square_nonneg.
  -a, b:Z
H:b <> 0
0 <= Z.sgn (Z.rem a b) * Z.sgn a zero_or_not (Z.rem a b).a, b:Z
H:b <> 0
H0:Z.rem a b <> 0
0 <= Z.sgn (Z.rem a b) * Z.sgn a
    rewrite Z.rem_sign_nz; trivial.a, b:Z
H:b <> 0
H0:Z.rem a b <> 0
0 <= Z.sgn a * Z.sgn a apply Z.square_nonneg.
Qed.

This can also be said in a simpler way:

Theorem Zrem_sgn2 a b : 0 <= (Z.rem a b) * a.a, b:Z
0 <= Z.rem a b * a
Proof.a, b:Z
0 <= Z.rem a b * a
  zero_or_not b.a:Z
0 <= a * a
a, b:Z
H:b <> 0
0 <= Z.rem a b * a
  -a:Z
0 <= a * a apply Z.square_nonneg.
  -a, b:Z
H:b <> 0
0 <= Z.rem a b * a now apply Z.rem_sign_mul.
Qed.

Reformulation of Z.rem_bound_abs in 2 then 4 particular cases.

Theorem Zrem_lt_pos a b : 0<=a -> b<>0 -> 0 <= Z.rem a b < Z.abs b.a, b:Z
0 <= a -> b <> 0 -> 0 <= Z.rem a b < Z.abs b
Proof.a, b:Z
0 <= a -> b <> 0 -> 0 <= Z.rem a b < Z.abs b
  intros; generalize (Z.rem_nonneg a b) (Z.rem_bound_abs a b);
    lia.
Qed.

Theorem Zrem_lt_neg a b : a<=0 -> b<>0 -> -Z.abs b < Z.rem a b <= 0.a, b:Z
a <= 0 -> b <> 0 -> - Z.abs b < Z.rem a b <= 0
Proof.a, b:Z
a <= 0 -> b <> 0 -> - Z.abs b < Z.rem a b <= 0
  intros; generalize (Z.rem_nonpos a b) (Z.rem_bound_abs a b);
   lia.
Qed.

Theorem Zrem_lt_pos_pos a b : 0<=a -> 0<b -> 0 <= Z.rem a b < b.a, b:Z
0 <= a -> 0 < b -> 0 <= Z.rem a b < b
Proof.a, b:Z
0 <= a -> 0 < b -> 0 <= Z.rem a b < b
  intros; generalize (Zrem_lt_pos a b); lia.
Qed.

Theorem Zrem_lt_pos_neg a b : 0<=a -> b<0 -> 0 <= Z.rem a b < -b.a, b:Z
0 <= a -> b < 0 -> 0 <= Z.rem a b < - b
Proof.a, b:Z
0 <= a -> b < 0 -> 0 <= Z.rem a b < - b
  intros; generalize (Zrem_lt_pos a b); lia.
Qed.

Theorem Zrem_lt_neg_pos a b : a<=0 -> 0<b -> -b < Z.rem a b <= 0.a, b:Z
a <= 0 -> 0 < b -> - b < Z.rem a b <= 0
Proof.a, b:Z
a <= 0 -> 0 < b -> - b < Z.rem a b <= 0
  intros; generalize (Zrem_lt_neg a b); lia.
Qed.

Theorem Zrem_lt_neg_neg a b : a<=0 -> b<0 -> b < Z.rem a b <= 0.a, b:Z
a <= 0 -> b < 0 -> b < Z.rem a b <= 0
Proof.a, b:Z
a <= 0 -> b < 0 -> b < Z.rem a b <= 0
  intros; generalize (Zrem_lt_neg a b); lia.
Qed.

Unicity results

Definition Remainder a b r :=
  (0 <= a /\ 0 <= r < Z.abs b) \/ (a <= 0 /\ -Z.abs b < r <= 0).

Definition Remainder_alt a b r :=
  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.forall a b r : Z,
Remainder a b r <-> Remainder_alt a b r
Proof.forall a b r : Z,
Remainder a b r <-> Remainder_alt a b r
  unfold Remainder, Remainder_alt; intuition.a, b, r:Z
H:0 <= a
H0:0 <= r
H2:r < Z.abs b
Z.abs r < Z.abs b
a, b, r:Z
H:a <= 0
H0:- Z.abs b < r
H2:r <= 0
Z.abs r < Z.abs b
a, b, r:Z
H:a <= 0
H0:- Z.abs b < r
H2:r <= 0
0 <= r * a
a, b, r:Z
H0:Z.abs r < Z.abs b
H1:0 <= r * a
0 <= a /\ 0 <= r < Z.abs b \/
a <= 0 /\ - Z.abs b < r <= 0
  -a, b, r:Z
H:0 <= a
H0:0 <= r
H2:r < Z.abs b
Z.abs r < Z.abs b lia.
  -a, b, r:Z
H:a <= 0
H0:- Z.abs b < r
H2:r <= 0
Z.abs r < Z.abs b lia.
  -a, b, r:Z
H:a <= 0
H0:- Z.abs b < r
H2:r <= 0
0 <= r * a rewrite <-(Z.mul_opp_opp).a, b, r:Z
H:a <= 0
H0:- Z.abs b < r
H2:r <= 0
0 <= - r * - a apply Z.mul_nonneg_nonneg; lia.
  -a, b, r:Z
H0:Z.abs r < Z.abs b
H1:0 <= r * a
0 <= a /\ 0 <= r < Z.abs b \/
a <= 0 /\ - Z.abs b < r <= 0 assert (0 <= Z.sgn r * Z.sgn a).a, b, r:Z
H0:Z.abs r < Z.abs b
H1:0 <= r * a
0 <= Z.sgn r * Z.sgn a
a, b, r:Z
H0:Z.abs r < Z.abs b
H1:0 <= r * a
H:0 <= Z.sgn r * Z.sgn a
0 <= a /\ 0 <= r < Z.abs b \/
a <= 0 /\ - Z.abs b < r <= 0
    {a, b, r:Z
H0:Z.abs r < Z.abs b
H1:0 <= r * a
0 <= Z.sgn r * Z.sgn a rewrite <-Z.sgn_mul, Z.sgn_nonneg; auto. }a, b, r:Z
H0:Z.abs r < Z.abs b
H1:0 <= r * a
H:0 <= Z.sgn r * Z.sgn a
0 <= a /\ 0 <= r < Z.abs b \/
a <= 0 /\ - Z.abs b < r <= 0
    destruct r; simpl Z.sgn in *; lia.
Qed.

Theorem Zquot_mod_unique_full a b q r :
  Remainder a b r -> a = b*q + r -> q = a÷b /\ r = Z.rem a b.a, b, q, r:Z
Remainder a b r ->
a = b * q + r -> q = a ÷ b /\ r = Z.rem a b
Proof.a, b, q, r:Z
Remainder a b r ->
a = b * q + r -> q = a ÷ b /\ r = Z.rem a b
  destruct 1 as [(H,H0)|(H,H0)]; intros.a, b, q, r:Z
H:0 <= a
H0:0 <= r < Z.abs b
H1:a = b * q + r
q = a ÷ b /\ r = Z.rem a b
a, b, q, r:Z
H:a <= 0
H0:- Z.abs b < r <= 0
H1:a = b * q + r
q = a ÷ b /\ r = Z.rem a b
  apply Zdiv_mod_unique with b; auto.a, b, q, r:Z
H:0 <= a
H0:0 <= r < Z.abs b
H1:a = b * q + r
0 <= Z.rem a b < Z.abs b
a, b, q, r:Z
H:0 <= a
H0:0 <= r < Z.abs b
H1:a = b * q + r
b * q + r = b * (a ÷ b) + Z.rem a b
a, b, q, r:Z
H:a <= 0
H0:- Z.abs b < r <= 0
H1:a = b * q + r
q = a ÷ b /\ r = Z.rem a b
  apply Zrem_lt_pos; auto.a, b, q, r:Z
H:0 <= a
H0:0 <= r < Z.abs b
H1:a = b * q + r
b <> 0
a, b, q, r:Z
H:0 <= a
H0:0 <= r < Z.abs b
H1:a = b * q + r
b * q + r = b * (a ÷ b) + Z.rem a b
a, b, q, r:Z
H:a <= 0
H0:- Z.abs b < r <= 0
H1:a = b * q + r
q = a ÷ b /\ r = Z.rem a b
  lia.a, b, q, r:Z
H:0 <= a
H0:0 <= r < Z.abs b
H1:a = b * q + r
b * q + r = b * (a ÷ b) + Z.rem a b
a, b, q, r:Z
H:a <= 0
H0:- Z.abs b < r <= 0
H1:a = b * q + r
q = a ÷ b /\ r = Z.rem a b
  rewrite <- H1; apply Z.quot_rem'.a, b, q, r:Z
H:a <= 0
H0:- Z.abs b < r <= 0
H1:a = b * q + r
q = a ÷ b /\ r = Z.rem a b

  rewrite <- (Z.opp_involutive a).a, b, q, r:Z
H:a <= 0
H0:- Z.abs b < r <= 0
H1:a = b * q + r
q = - - a ÷ b /\ r = Z.rem (- - a) b
  rewrite Zquot_opp_l, Zrem_opp_l.a, b, q, r:Z
H:a <= 0
H0:- Z.abs b < r <= 0
H1:a = b * q + r
q = - (- a ÷ b) /\ r = - Z.rem (- a) b
  generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Z.rem (-a) b)).a, b, q, r:Z
H:a <= 0
H0:- Z.abs b < r <= 0
H1:a = b * q + r
(0 <= - r < Z.abs b ->
 0 <= Z.rem (- a) b < Z.abs b ->
 b * - q + - r = b * (- a ÷ b) + Z.rem (- a) b ->
 - q = - a ÷ b /\ - r = Z.rem (- a) b) ->
q = - (- a ÷ b) /\ r = - Z.rem (- a) b
  generalize (Zrem_lt_pos (-a) b).a, b, q, r:Z
H:a <= 0
H0:- Z.abs b < r <= 0
H1:a = b * q + r
(0 <= - a -> b <> 0 -> 0 <= Z.rem (- a) b < Z.abs b) ->
(0 <= - r < Z.abs b ->
 0 <= Z.rem (- a) b < Z.abs b ->
 b * - q + - r = b * (- a ÷ b) + Z.rem (- a) b ->
 - q = - a ÷ b /\ - r = Z.rem (- a) b) ->
q = - (- a ÷ b) /\ r = - Z.rem (- a) b
  rewrite <-Z.quot_rem', Z.mul_opp_r, <-Z.opp_add_distr, <-H1.a, b, q, r:Z
H:a <= 0
H0:- Z.abs b < r <= 0
H1:a = b * q + r
(0 <= - a -> b <> 0 -> 0 <= Z.rem (- a) b < Z.abs b) ->
(0 <= - r < Z.abs b ->
 0 <= Z.rem (- a) b < Z.abs b ->
 - a = - a -> - q = - a ÷ b /\ - r = Z.rem (- a) b) ->
q = - (- a ÷ b) /\ r = - Z.rem (- a) b
  lia.
Qed.

Theorem Zquot_unique_full a b q r :
  Remainder a b r -> a = b*q + r -> q = a÷b.a, b, q, r:Z
Remainder a b r -> a = b * q + r -> q = a ÷ b
Proof.a, b, q, r:Z
Remainder a b r -> a = b * q + r -> q = a ÷ b
 intros; destruct (Zquot_mod_unique_full a b q r); auto.
Qed.

Theorem Zrem_unique_full a b q r :
  Remainder a b r -> a = b*q + r -> r = Z.rem a b.a, b, q, r:Z
Remainder a b r -> a = b * q + r -> r = Z.rem a b
Proof.a, b, q, r:Z
Remainder a b r -> a = b * q + r -> r = Z.rem a b
 intros; destruct (Zquot_mod_unique_full a b q r); auto.
Qed.

Order results about Zrem and Zquot

(* Division of positive numbers is positive. *)

Lemma Z_quot_pos a b : 0 <= a -> 0 <= b -> 0 <= a÷b.a, b:Z
0 <= a -> 0 <= b -> 0 <= a ÷ b
Proof.a, b:Z
0 <= a -> 0 <= b -> 0 <= a ÷ b intros.a, b:Z
H:0 <= a
H0:0 <= b
0 <= a ÷ b zero_or_not b.a, b:Z
H:0 <= a
H0:0 <= b
H1:b <> 0
0 <= a ÷ b apply Z.quot_pos; auto with zarith. Qed.

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

Lemma Z_quot_lt a b : 0 < a -> 2 <= b -> a÷b < a.a, b:Z
0 < a -> 2 <= b -> a ÷ b < a
Proof.a, b:Z
0 < a -> 2 <= b -> a ÷ b < a intros.a, b:Z
H:0 < a
H0:2 <= b
a ÷ b < a apply Z.quot_lt; auto with zarith. Qed.

≤ is compatible with a positive division.

Lemma Z_quot_monotone a b c : 0<=c -> a<=b -> a÷c <= b÷c.a, b, c:Z
0 <= c -> a <= b -> a ÷ c <= b ÷ c
Proof.a, b, c:Z
0 <= c -> a <= b -> a ÷ c <= b ÷ c intros.a, b, c:Z
H:0 <= c
H0:a <= b
a ÷ c <= b ÷ c zero_or_not c.a, b, c:Z
H:0 <= c
H0:a <= b
H1:c <> 0
a ÷ c <= b ÷ c apply Z.quot_le_mono; auto with zarith. Qed.

With our choice of division, rounding of (a÷b) is always done toward 0:

Lemma Z_mult_quot_le a b : 0 <= a -> 0 <= b*(a÷b) <= a.a, b:Z
0 <= a -> 0 <= b * (a ÷ b) <= a
Proof.a, b:Z
0 <= a -> 0 <= b * (a ÷ b) <= a intros.a, b:Z
H:0 <= a
0 <= b * (a ÷ b) <= a zero_or_not b.a, b:Z
H:0 <= a
H0:b <> 0
0 <= b * (a ÷ b) <= a apply Z.mul_quot_le; auto with zarith. Qed.

Lemma Z_mult_quot_ge a b : a <= 0 -> a <= b*(a÷b) <= 0.a, b:Z
a <= 0 -> a <= b * (a ÷ b) <= 0
Proof.a, b:Z
a <= 0 -> a <= b * (a ÷ b) <= 0 intros.a, b:Z
H:a <= 0
a <= b * (a ÷ b) <= 0 zero_or_not b.a, b:Z
H:a <= 0
H0:b <> 0
a <= b * (a ÷ b) <= 0 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 a b : a = b*(a÷b) <-> Z.rem a b = 0.a, b:Z
a = b * (a ÷ b) <-> Z.rem a b = 0
Proof.a, b:Z
a = b * (a ÷ b) <-> Z.rem a b = 0 intros.a, b:Z
a = b * (a ÷ b) <-> Z.rem a b = 0 zero_or_not b.a:Z
a = 0 * 0 <-> a = 0
a, b:Z
H:b <> 0
a = b * (a ÷ b) <-> Z.rem a b = 0 intuition.a, b:Z
H:b <> 0
a = b * (a ÷ b) <-> Z.rem a b = 0 apply Z.quot_exact; auto. Qed.

A modulo cannot grow beyond its starting point.

Theorem Zrem_le a b : 0 <= a -> 0 <= b -> Z.rem a b <= a.a, b:Z
0 <= a -> 0 <= b -> Z.rem a b <= a
Proof.a, b:Z
0 <= a -> 0 <= b -> Z.rem a b <= a intros.a, b:Z
H:0 <= a
H0:0 <= b
Z.rem a b <= a zero_or_not b.a, b:Z
H:0 <= a
H0:0 <= b
H1:b <> 0
Z.rem a b <= a apply Z.rem_le; auto with zarith. Qed.

Some additional inequalities about Zdiv.

Theorem Zquot_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.quot_le_upper_bound. Qed.

Theorem Zquot_lt_upper_bound:
  forall a b q, 0 <= a -> 0 < b -> a < q*b -> a÷b < q.forall a b q : Z,
0 <= a -> 0 < b -> a < q * b -> a ÷ b < q
Proof.forall a b q : Z,
0 <= a -> 0 < b -> a < q * b -> a ÷ b < q intros a b q; rewrite Z.mul_comm; apply Z.quot_lt_upper_bound. Qed.

Theorem Zquot_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.quot_le_lower_bound. Qed.

Theorem Zquot_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;
  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

First, a result that used to be always valid with Zdiv, but must be restricted here. For instance, now (9+(-5)*2) rem 2 = -1 <> 1 = 9 rem 2

Lemma Z_rem_plus : forall a b c:Z,
 0 <= (a+b*c) * a ->
 Z.rem (a + b * c) c = Z.rem a c.forall a b c : Z,
0 <= (a + b * c) * a ->
Z.rem (a + b * c) c = Z.rem a c
Proof.forall a b c : Z,
0 <= (a + b * c) * a ->
Z.rem (a + b * c) c = Z.rem a c intros.a, b, c:Z
H:0 <= (a + b * c) * a
Z.rem (a + b * c) c = Z.rem a c zero_or_not c.a, b, c:Z
H:0 <= (a + b * c) * a
H0:c <> 0
Z.rem (a + b * c) c = Z.rem a c apply Z.rem_add; auto with zarith. Qed.

Lemma Z_quot_plus : forall a b c:Z,
 0 <= (a+b*c) * a -> c<>0 ->
 (a + b * c) ÷ c = a ÷ c + b.forall a b c : Z,
0 <= (a + b * c) * a ->
c <> 0 -> (a + b * c) ÷ c = a ÷ c + b
Proof.forall a b c : Z,
0 <= (a + b * c) * a ->
c <> 0 -> (a + b * c) ÷ c = a ÷ c + b intros.a, b, c:Z
H:0 <= (a + b * c) * a
H0:c <> 0
(a + b * c) ÷ c = a ÷ c + b apply Z.quot_add; auto with zarith. Qed.

Theorem Z_quot_plus_l: forall a b c : Z,
 0 <= (a*b+c)*c -> b<>0 ->
 b<>0 -> (a * b + c) ÷ b = a + c ÷ b.forall a b c : Z,
0 <= (a * b + c) * c ->
b <> 0 -> b <> 0 -> (a * b + c) ÷ b = a + c ÷ b
Proof.forall a b c : Z,
0 <= (a * b + c) * c ->
b <> 0 -> b <> 0 -> (a * b + c) ÷ b = a + c ÷ b intros.a, b, c:Z
H:0 <= (a * b + c) * c
H0, H1:b <> 0
(a * b + c) ÷ b = a + c ÷ b apply Z.quot_add_l; auto with zarith. Qed.

Cancellations.

Lemma Zquot_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
H0:b <> 0
a * c ÷ (b * c) = a ÷ b apply Z.quot_mul_cancel_r; auto. Qed.

Lemma Zquot_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).a, b, c:Z
H:c <> 0
c * a ÷ (b * c) = a ÷ b zero_or_not b.a, b, c:Z
H:c <> 0
H0:b <> 0
c * a ÷ (b * c) = a ÷ b
 rewrite (Z.mul_comm b c).a, b, c:Z
H:c <> 0
H0:b <> 0
c * a ÷ (c * b) = a ÷ b apply Z.quot_mul_cancel_l; auto.
Qed.

Lemma Zmult_rem_distr_l: forall a b c,
  Z.rem (c*a) (c*b) = c * (Z.rem a b).forall a b c : Z,
Z.rem (c * a) (c * b) = c * Z.rem a b
Proof.forall a b c : Z,
Z.rem (c * a) (c * b) = c * Z.rem a b
 intros.a, b, c:Z
Z.rem (c * a) (c * b) = c * Z.rem a b zero_or_not c.a, b, c:Z
H:c <> 0
Z.rem (c * a) (c * b) = c * Z.rem a b rewrite (Z.mul_comm c b).a, b, c:Z
H:c <> 0
Z.rem (c * a) (b * c) = c * Z.rem a b zero_or_not b.a, b, c:Z
H:c <> 0
H0:b <> 0
Z.rem (c * a) (b * c) = c * Z.rem a b
 rewrite (Z.mul_comm b c).a, b, c:Z
H:c <> 0
H0:b <> 0
Z.rem (c * a) (c * b) = c * Z.rem a b apply Z.mul_rem_distr_l; auto.
Qed.

Lemma Zmult_rem_distr_r: forall a b c,
  Z.rem (a*c) (b*c) = (Z.rem a b) * c.forall a b c : Z,
Z.rem (a * c) (b * c) = Z.rem a b * c
Proof.forall a b c : Z,
Z.rem (a * c) (b * c) = Z.rem a b * c
 intros.a, b, c:Z
Z.rem (a * c) (b * c) = Z.rem a b * c zero_or_not b.a, b, c:Z
H:b <> 0
Z.rem (a * c) (b * c) = Z.rem a b * c rewrite (Z.mul_comm b c).a, b, c:Z
H:b <> 0
Z.rem (a * c) (c * b) = Z.rem a b * c zero_or_not c.a, b, c:Z
H:b <> 0
H0:c <> 0
Z.rem (a * c) (c * b) = Z.rem a b * c
 rewrite (Z.mul_comm c b).a, b, c:Z
H:b <> 0
H0:c <> 0
Z.rem (a * c) (b * c) = Z.rem a b * c apply Z.mul_rem_distr_r; auto.
Qed.

Operations modulo.

Theorem Zrem_rem: forall a n, Z.rem (Z.rem a n) n = Z.rem a n.forall a n : Z, Z.rem (Z.rem a n) n = Z.rem a n
Proof.forall a n : Z, Z.rem (Z.rem a n) n = Z.rem a n intros.a, n:Z
Z.rem (Z.rem a n) n = Z.rem a n zero_or_not n.a, n:Z
H:n <> 0
Z.rem (Z.rem a n) n = Z.rem a n apply Z.rem_rem; auto. Qed.

Theorem Zmult_rem: forall a b n,
 Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n.forall a b n : Z,
Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n
Proof.forall a b n : Z,
Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n intros.a, b, n:Z
Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n zero_or_not n.a, b, n:Z
H:n <> 0
Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n apply Z.mul_rem; auto. Qed.

addition and modulo

Generally speaking, unlike with Zdiv, we don't have (a+b) rem n = (a rem n + b rem n) rem n for any a and b. For instance, take (8 + (-10)) rem 3 = -2 whereas (8 rem 3 + (-10 rem 3)) rem 3 = 1.

Theorem Zplus_rem: forall a b n,
 0 <= a * b ->
 Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) n.forall a b n : Z,
0 <= a * b ->
Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) n
Proof.forall a b n : Z,
0 <= a * b ->
Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) n intros.a, b, n:Z
H:0 <= a * b
Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) n zero_or_not n.a, b, n:Z
H:0 <= a * b
H0:n <> 0
Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) n apply Z.add_rem; auto. Qed.

Lemma Zplus_rem_idemp_l: forall a b n,
 0 <= a * b ->
 Z.rem (Z.rem a n + b) n = Z.rem (a + b) n.forall a b n : Z,
0 <= a * b ->
Z.rem (Z.rem a n + b) n = Z.rem (a + b) n
Proof.forall a b n : Z,
0 <= a * b ->
Z.rem (Z.rem a n + b) n = Z.rem (a + b) n intros.a, b, n:Z
H:0 <= a * b
Z.rem (Z.rem a n + b) n = Z.rem (a + b) n zero_or_not n.a, b, n:Z
H:0 <= a * b
H0:n <> 0
Z.rem (Z.rem a n + b) n = Z.rem (a + b) n apply Z.add_rem_idemp_l; auto. Qed.

Lemma Zplus_rem_idemp_r: forall a b n,
 0 <= a*b ->
 Z.rem (b + Z.rem a n) n = Z.rem (b + a) n.forall a b n : Z,
0 <= a * b ->
Z.rem (b + Z.rem a n) n = Z.rem (b + a) n
Proof.forall a b n : Z,
0 <= a * b ->
Z.rem (b + Z.rem a n) n = Z.rem (b + a) n
 intros.a, b, n:Z
H:0 <= a * b
Z.rem (b + Z.rem a n) n = Z.rem (b + a) n zero_or_not n.a, b, n:Z
H:0 <= a * b
H0:n <> 0
Z.rem (b + Z.rem a n) n = Z.rem (b + a) n apply Z.add_rem_idemp_r; auto.a, b, n:Z
H:0 <= a * b
H0:n <> 0
0 <= b * a
 rewrite Z.mul_comm; auto.
Qed.

Lemma Zmult_rem_idemp_l: forall a b n, Z.rem (Z.rem a n * b) n = Z.rem (a * b) n.forall a b n : Z,
Z.rem (Z.rem a n * b) n = Z.rem (a * b) n
Proof.forall a b n : Z,
Z.rem (Z.rem a n * b) n = Z.rem (a * b) n intros.a, b, n:Z
Z.rem (Z.rem a n * b) n = Z.rem (a * b) n zero_or_not n.a, b, n:Z
H:n <> 0
Z.rem (Z.rem a n * b) n = Z.rem (a * b) n apply Z.mul_rem_idemp_l; auto. Qed.

Lemma Zmult_rem_idemp_r: forall a b n, Z.rem (b * Z.rem a n) n = Z.rem (b * a) n.forall a b n : Z,
Z.rem (b * Z.rem a n) n = Z.rem (b * a) n
Proof.forall a b n : Z,
Z.rem (b * Z.rem a n) n = Z.rem (b * a) n intros.a, b, n:Z
Z.rem (b * Z.rem a n) n = Z.rem (b * a) n zero_or_not n.a, b, n:Z
H:n <> 0
Z.rem (b * Z.rem a n) n = Z.rem (b * a) n apply Z.mul_rem_idemp_r; auto. Qed.

Unlike with Zdiv, the following result is true without restrictions.

Lemma Zquot_Zquot : forall a b c, (a÷b)÷c = a÷(b*c).forall a b c : Z, a ÷ b ÷ c = a ÷ (b * c)
Proof.forall a b c : Z, a ÷ b ÷ c = a ÷ (b * c)
 intros.a, b, c:Z
a ÷ b ÷ c = a ÷ (b * c) zero_or_not b.a, b, c:Z
H:b <> 0
a ÷ b ÷ c = a ÷ (b * c) rewrite Z.mul_comm.a, b, c:Z
H:b <> 0
a ÷ b ÷ c = a ÷ (c * b) zero_or_not c.a, b, c:Z
H:b <> 0
H0:c <> 0
a ÷ b ÷ c = a ÷ (c * b)
 rewrite Z.mul_comm.a, b, c:Z
H:b <> 0
H0:c <> 0
a ÷ b ÷ c = a ÷ (b * c) apply Z.quot_quot; auto.
Qed.

A last inequality:

Theorem Zquot_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
H2:b <> 0
c * (a ÷ b) <= c * a ÷ b apply Z.quot_mul_le; auto with zarith. Qed.

Z.rem is related to divisibility (see more in Znumtheory)

Lemma Zrem_divides : forall a b,
 Z.rem a b = 0 <-> exists c, a = b*c.forall a b : Z,
Z.rem a b = 0 <-> (exists c : Z, a = b * c)
Proof.forall a b : Z,
Z.rem a b = 0 <-> (exists c : Z, a = b * c)
 intros.a, b:Z
Z.rem a b = 0 <-> (exists c : Z, a = b * c) zero_or_not b.a:Z
a = 0 <-> (exists c : Z, a = 0 * c)
a, b:Z
H:b <> 0
Z.rem a b = 0 <-> (exists c : Z, a = b * c) firstorder.a, b:Z
H:b <> 0
Z.rem a b = 0 <-> (exists c : Z, a = b * c)
 rewrite Z.rem_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 Zquot2_odd_remainder : forall a,
 Remainder a 2 (if Z.odd a then Z.sgn a else 0).forall a : Z,
Remainder a 2 (if Z.odd a then Z.sgn a else 0)
Proof.forall a : Z,
Remainder a 2 (if Z.odd a then Z.sgn a else 0)
 intros [ |p|p].Remainder 0 2 (if Z.odd 0 then Z.sgn 0 else 0)
p:positive
Remainder (Z.pos p) 2
  (if Z.odd (Z.pos p) then Z.sgn (Z.pos p) else 0)
p:positive
Remainder (Z.neg p) 2
  (if Z.odd (Z.neg p) then Z.sgn (Z.neg p) else 0) simpl.Remainder 0 2 0
p:positive
Remainder (Z.pos p) 2
  (if Z.odd (Z.pos p) then Z.sgn (Z.pos p) else 0)
p:positive
Remainder (Z.neg p) 2
  (if Z.odd (Z.neg p) then Z.sgn (Z.neg p) else 0)
 left.0 <= 0 /\ 0 <= 0 < Z.abs 2
p:positive
Remainder (Z.pos p) 2
  (if Z.odd (Z.pos p) then Z.sgn (Z.pos p) else 0)
p:positive
Remainder (Z.neg p) 2
  (if Z.odd (Z.neg p) then Z.sgn (Z.neg p) else 0) simpl.0 <= 0 /\ 0 <= 0 < 2
p:positive
Remainder (Z.pos p) 2
  (if Z.odd (Z.pos p) then Z.sgn (Z.pos p) else 0)
p:positive
Remainder (Z.neg p) 2
  (if Z.odd (Z.neg p) then Z.sgn (Z.neg p) else 0) auto with zarith.p:positive
Remainder (Z.pos p) 2
  (if Z.odd (Z.pos p) then Z.sgn (Z.pos p) else 0)
p:positive
Remainder (Z.neg p) 2
  (if Z.odd (Z.neg p) then Z.sgn (Z.neg p) else 0)
 left.p:positive
0 <= Z.pos p /\
0 <=
(if Z.odd (Z.pos p) then Z.sgn (Z.pos p) else 0) <
Z.abs 2
p:positive
Remainder (Z.neg p) 2
  (if Z.odd (Z.neg p) then Z.sgn (Z.neg p) else 0) destruct p; simpl; auto with zarith.p:positive
Remainder (Z.neg p) 2
  (if Z.odd (Z.neg p) then Z.sgn (Z.neg p) else 0)
 right.p:positive
Z.neg p <= 0 /\
- Z.abs 2 <
(if Z.odd (Z.neg p) then Z.sgn (Z.neg p) else 0) <= 0 destruct p; simpl; split; now auto with zarith.
Qed.

Lemma Zrem_odd : forall a, Z.rem a 2 = if Z.odd a then Z.sgn a else 0.forall a : Z,
Z.rem a 2 = (if Z.odd a then Z.sgn a else 0)
Proof.forall a : Z,
Z.rem a 2 = (if Z.odd a then Z.sgn a else 0)
 intros.a:Z
Z.rem a 2 = (if Z.odd a then Z.sgn a else 0) symmetry.a:Z
(if Z.odd a then Z.sgn a else 0) = Z.rem a 2
 apply Zrem_unique_full with (Z.quot2 a).a:Z
Remainder a 2 (if Z.odd a then Z.sgn a else 0)
a:Z
a = 2 * Z.quot2 a + (if Z.odd a then Z.sgn a else 0)
 apply Zquot2_odd_remainder.a:Z
a = 2 * Z.quot2 a + (if Z.odd a then Z.sgn a else 0)
 apply Zquot2_odd_eqn.
Qed.

Lemma Zrem_even : forall a, Z.rem a 2 = if Z.even a then 0 else Z.sgn a.forall a : Z,
Z.rem a 2 = (if Z.even a then 0 else Z.sgn a)
Proof.forall a : Z,
Z.rem a 2 = (if Z.even a then 0 else Z.sgn a)
 intros a.a:Z
Z.rem a 2 = (if Z.even a then 0 else Z.sgn a) rewrite Zrem_odd, Zodd_even_bool.a:Z
(if negb (Z.even a) then Z.sgn a else 0) =
(if Z.even a then 0 else Z.sgn a) now destruct Z.even.
Qed.

Lemma Zeven_rem : forall a, Z.even a = Z.eqb (Z.rem a 2) 0.forall a : Z, Z.even a = (Z.rem a 2 =? 0)
Proof.forall a : Z, Z.even a = (Z.rem a 2 =? 0)
 intros a.a:Z
Z.even a = (Z.rem a 2 =? 0) rewrite Zrem_even.a:Z
Z.even a = ((if Z.even a then 0 else Z.sgn a) =? 0)
 destruct a as [ |p|p]; trivial; now destruct p.
Qed.

Lemma Zodd_rem : forall a, Z.odd a = negb (Z.eqb (Z.rem a 2) 0).forall a : Z, Z.odd a = negb (Z.rem a 2 =? 0)
Proof.forall a : Z, Z.odd a = negb (Z.rem a 2 =? 0)
 intros a.a:Z
Z.odd a = negb (Z.rem a 2 =? 0) rewrite Zrem_odd.a:Z
Z.odd a = negb ((if Z.odd a then Z.sgn a else 0) =? 0)
 destruct a as [ |p|p]; trivial; now destruct p.
Qed.

Interaction with "historic" Zdiv

They agree at least on positive numbers:

Theorem Zquotrem_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b ->
  a÷b = a/b /\ Z.rem a b = a mod b.forall a b : Z,
0 <= a ->
0 < b -> a ÷ b = a / b /\ Z.rem a b = a mod b
Proof.forall a b : Z,
0 <= a ->
0 < b -> a ÷ b = a / b /\ Z.rem a b = a mod b
  intros.a, b:Z
H:0 <= a
H0:0 < b
a ÷ b = a / b /\ Z.rem a b = a mod b
  apply Zdiv_mod_unique with b.a, b:Z
H:0 <= a
H0:0 < b
0 <= Z.rem a b < Z.abs b
a, b:Z
H:0 <= a
H0:0 < b
0 <= a mod b < Z.abs b
a, b:Z
H:0 <= a
H0:0 < b
b * (a ÷ b) + Z.rem a b = b * (a / b) + a mod b
  apply Zrem_lt_pos; auto with zarith.a, b:Z
H:0 <= a
H0:0 < b
0 <= a mod b < Z.abs b
a, b:Z
H:0 <= a
H0:0 < b
b * (a ÷ b) + Z.rem a b = b * (a / b) + a mod b
  rewrite Z.abs_eq; auto with *; apply Z_mod_lt; auto with *.a, b:Z
H:0 <= a
H0:0 < b
b * (a ÷ b) + Z.rem a b = b * (a / b) + a mod b
  rewrite <- Z_div_mod_eq; auto with *.a, b:Z
H:0 <= a
H0:0 < b
b * (a ÷ b) + Z.rem a b = a
  symmetry; apply Z.quot_rem; auto with *.
Qed.

Theorem Zquot_Zdiv_pos : forall a b, 0 <= a -> 0 <= b ->
  a÷b = a/b.forall a b : Z, 0 <= a -> 0 <= b -> a ÷ b = a / b
Proof.forall a b : Z, 0 <= a -> 0 <= b -> a ÷ b = a / b
 intros a b Ha Hb.a, b:Z
Ha:0 <= a
Hb:0 <= b
a ÷ b = a / b Z.le_elim Hb.a, b:Z
Ha:0 <= a
Hb:0 < b
a ÷ b = a / b
a, b:Z
Ha:0 <= a
Hb:0 = b
a ÷ b = a / b
 -a, b:Z
Ha:0 <= a
Hb:0 < b
a ÷ b = a / b generalize (Zquotrem_Zdiv_eucl_pos a b Ha Hb); intuition.
 -a, b:Z
Ha:0 <= a
Hb:0 = b
a ÷ b = a / b subst; now rewrite Zquot_0_r, Zdiv_0_r.
Qed.

Theorem Zrem_Zmod_pos : forall a b, 0 <= a -> 0 < b ->
  Z.rem a b = a mod b.forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b = a mod b
Proof.forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b = a mod b
 intros a b Ha Hb; generalize (Zquotrem_Zdiv_eucl_pos a b Ha Hb);
 intuition.
Qed.

Modulos are null at the same places

Theorem Zrem_Zmod_zero : forall a b, b<>0 ->
 (Z.rem a b = 0 <-> a mod b = 0).forall a b : Z,
b <> 0 -> Z.rem a b = 0 <-> a mod b = 0
Proof.forall a b : Z,
b <> 0 -> Z.rem a b = 0 <-> a mod b = 0
 intros.a, b:Z
H:b <> 0
Z.rem a b = 0 <-> a mod b = 0
 rewrite Zrem_divides, Zmod_divides; intuition.
Qed.