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 ZAxioms ZMulOrder ZSgnAbs NZDiv.

Euclidean Division for integers (Floor convention)

We use here the convention known as Floor, or Round-Toward-Bottom, where a/b is the closest integer below the exact fraction. It can be summarized by:

a = bq+r ∧ 0 ≤ |r| < |b| ∧ Sign(r) = Sign(b)

This is the convention followed historically by Z.div in Coq, and corresponds to convention "F" in the following paper:

R. Boute, "The Euclidean definition of the functions div and mod", ACM Transactions on Programming Languages and Systems, Vol. 14, No.2, pp. 127-144, April 1992.

See files ZDivTrunc and ZDivEucl for others conventions.

Module Type ZDivProp
 (Import A : ZAxiomsSig')
 (Import B : ZMulOrderProp A)
 (Import C : ZSgnAbsProp A B).

We benefit from what already exists for NZ

Module Import Private_NZDiv := Nop <+ NZDivProp A A B.

Another formulation of the main equation

Lemma mod_eq :
 forall a b, b~=0 -> a mod b == a - b*(a/b).forall a b : t, b ~= 0 -> a mod b == a - b * (a / b)
Proof.forall a b : t, b ~= 0 -> a mod b == a - b * (a / b)
intros.a, b:t
H:b ~= 0
a mod b == a - b * (a / b)
rewrite <- add_move_l.a, b:t
H:b ~= 0
b * (a / b) + a mod b == a
symmetry.a, b:t
H:b ~= 0
a == b * (a / b) + a mod b now apply div_mod.
Qed.

We have a general bound for absolute values

Lemma mod_bound_abs :
 forall a b, b~=0 -> abs (a mod b) < abs b.forall a b : t, b ~= 0 -> abs (a mod b) < abs b
Proof.forall a b : t, b ~= 0 -> abs (a mod b) < abs b
intros.a, b:t
H:b ~= 0
abs (a mod b) < abs b
destruct (abs_spec b) as [(LE,EQ)|(LE,EQ)]; rewrite EQ.a, b:t
H:b ~= 0
LE:0 <= b
EQ:abs b == b
abs (a mod b) < b
a, b:t
H:b ~= 0
LE:b < 0
EQ:abs b == - b
abs (a mod b) < - b
destruct (mod_pos_bound a b).a, b:t
H:b ~= 0
LE:0 <= b
EQ:abs b == b
0 < b
a, b:t
H:b ~= 0
LE:0 <= b
EQ:abs b == b
H0:0 <= a mod b
H1:a mod b < b
abs (a mod b) < b
a, b:t
H:b ~= 0
LE:b < 0
EQ:abs b == - b
abs (a mod b) < - b order.a, b:t
H:b ~= 0
LE:0 <= b
EQ:abs b == b
H0:0 <= a mod b
H1:a mod b < b
abs (a mod b) < b
a, b:t
H:b ~= 0
LE:b < 0
EQ:abs b == - b
abs (a mod b) < - b now rewrite abs_eq.a, b:t
H:b ~= 0
LE:b < 0
EQ:abs b == - b
abs (a mod b) < - b
destruct (mod_neg_bound a b).a, b:t
H:b ~= 0
LE:b < 0
EQ:abs b == - b
b < 0
a, b:t
H:b ~= 0
LE:b < 0
EQ:abs b == - b
H0:b < a mod b
H1:a mod b <= 0
abs (a mod b) < - b order.a, b:t
H:b ~= 0
LE:b < 0
EQ:abs b == - b
H0:b < a mod b
H1:a mod b <= 0
abs (a mod b) < - b rewrite abs_neq; trivial.a, b:t
H:b ~= 0
LE:b < 0
EQ:abs b == - b
H0:b < a mod b
H1:a mod b <= 0
- (a mod b) < - b
now rewrite <- opp_lt_mono.
Qed.

Uniqueness theorems

Theorem div_mod_unique : forall b q1 q2 r1 r2 : t,
  (0<=r1<b \/ b<r1<=0) -> (0<=r2<b \/ b<r2<=0) ->
  b*q1+r1 == b*q2+r2 -> q1 == q2 /\ r1 == r2.forall b q1 q2 r1 r2 : t,
0 <= r1 < b \/ b < r1 <= 0 ->
0 <= r2 < b \/ b < r2 <= 0 ->
b * q1 + r1 == b * q2 + r2 -> q1 == q2 /\ r1 == r2
Proof.forall b q1 q2 r1 r2 : t,
0 <= r1 < b \/ b < r1 <= 0 ->
0 <= r2 < b \/ b < r2 <= 0 ->
b * q1 + r1 == b * q2 + r2 -> q1 == q2 /\ r1 == r2
intros b q1 q2 r1 r2 Hr1 Hr2 EQ.b, q1, q2, r1, r2:t
Hr1:0 <= r1 < b \/ b < r1 <= 0
Hr2:0 <= r2 < b \/ b < r2 <= 0
EQ:b * q1 + r1 == b * q2 + r2
q1 == q2 /\ r1 == r2
destruct Hr1; destruct Hr2; try (intuition; order).b, q1, q2, r1, r2:t
H:0 <= r1 < b
H0:0 <= r2 < b
EQ:b * q1 + r1 == b * q2 + r2
q1 == q2 /\ r1 == r2
b, q1, q2, r1, r2:t
H:b < r1 <= 0
H0:b < r2 <= 0
EQ:b * q1 + r1 == b * q2 + r2
q1 == q2 /\ r1 == r2
apply div_mod_unique with b; trivial.b, q1, q2, r1, r2:t
H:b < r1 <= 0
H0:b < r2 <= 0
EQ:b * q1 + r1 == b * q2 + r2
q1 == q2 /\ r1 == r2
rewrite <- (opp_inj_wd r1 r2).b, q1, q2, r1, r2:t
H:b < r1 <= 0
H0:b < r2 <= 0
EQ:b * q1 + r1 == b * q2 + r2
q1 == q2 /\ - r1 == - r2
apply div_mod_unique with (-b); trivial.b, q1, q2, r1, r2:t
H:b < r1 <= 0
H0:b < r2 <= 0
EQ:b * q1 + r1 == b * q2 + r2
0 <= - r1 < - b
b, q1, q2, r1, r2:t
H:b < r1 <= 0
H0:b < r2 <= 0
EQ:b * q1 + r1 == b * q2 + r2
0 <= - r2 < - b
b, q1, q2, r1, r2:t
H:b < r1 <= 0
H0:b < r2 <= 0
EQ:b * q1 + r1 == b * q2 + r2
- b * q1 + - r1 == - b * q2 + - r2
rewrite <- opp_lt_mono, opp_nonneg_nonpos; tauto.b, q1, q2, r1, r2:t
H:b < r1 <= 0
H0:b < r2 <= 0
EQ:b * q1 + r1 == b * q2 + r2
0 <= - r2 < - b
b, q1, q2, r1, r2:t
H:b < r1 <= 0
H0:b < r2 <= 0
EQ:b * q1 + r1 == b * q2 + r2
- b * q1 + - r1 == - b * q2 + - r2
rewrite <- opp_lt_mono, opp_nonneg_nonpos; tauto.b, q1, q2, r1, r2:t
H:b < r1 <= 0
H0:b < r2 <= 0
EQ:b * q1 + r1 == b * q2 + r2
- b * q1 + - r1 == - b * q2 + - r2
now rewrite 2 mul_opp_l, <- 2 opp_add_distr, opp_inj_wd.
Qed.

Theorem div_unique:
 forall a b q r, (0<=r<b \/ b<r<=0) -> a == b*q + r -> q == a/b.forall a b q r : t,
0 <= r < b \/ b < r <= 0 ->
a == b * q + r -> q == a / b
Proof.forall a b q r : t,
0 <= r < b \/ b < r <= 0 ->
a == b * q + r -> q == a / b
intros a b q r Hr EQ.a, b, q, r:t
Hr:0 <= r < b \/ b < r <= 0
EQ:a == b * q + r
q == a / b
assert (Hb : b~=0) by (destruct Hr; intuition; order).a, b, q, r:t
Hr:0 <= r < b \/ b < r <= 0
EQ:a == b * q + r
Hb:b ~= 0
q == a / b
destruct (div_mod_unique b q (a/b) r (a mod b)); trivial.a, b, q, r:t
Hr:0 <= r < b \/ b < r <= 0
EQ:a == b * q + r
Hb:b ~= 0
0 <= a mod b < b \/ b < a mod b <= 0
a, b, q, r:t
Hr:0 <= r < b \/ b < r <= 0
EQ:a == b * q + r
Hb:b ~= 0
b * q + r == b * (a / b) + a mod b
destruct Hr; [left; apply mod_pos_bound|right; apply mod_neg_bound];
 intuition order.a, b, q, r:t
Hr:0 <= r < b \/ b < r <= 0
EQ:a == b * q + r
Hb:b ~= 0
b * q + r == b * (a / b) + a mod b
now rewrite <- div_mod.
Qed.

Theorem div_unique_pos:
 forall a b q r, 0<=r<b -> a == b*q + r -> q == a/b.forall a b q r : t,
0 <= r < b -> a == b * q + r -> q == a / b
Proof.forall a b q r : t,
0 <= r < b -> a == b * q + r -> q == a / b intros; apply div_unique with r; auto. Qed.

Theorem div_unique_neg:
 forall a b q r, b<r<=0 -> a == b*q + r -> q == a/b.forall a b q r : t,
b < r <= 0 -> a == b * q + r -> q == a / b
Proof.forall a b q r : t,
b < r <= 0 -> a == b * q + r -> q == a / b intros; apply div_unique with r; auto. Qed.

Theorem mod_unique:
 forall a b q r, (0<=r<b \/ b<r<=0) -> a == b*q + r -> r == a mod b.forall a b q r : t,
0 <= r < b \/ b < r <= 0 ->
a == b * q + r -> r == a mod b
Proof.forall a b q r : t,
0 <= r < b \/ b < r <= 0 ->
a == b * q + r -> r == a mod b
intros a b q r Hr EQ.a, b, q, r:t
Hr:0 <= r < b \/ b < r <= 0
EQ:a == b * q + r
r == a mod b
assert (Hb : b~=0) by (destruct Hr; intuition; order).a, b, q, r:t
Hr:0 <= r < b \/ b < r <= 0
EQ:a == b * q + r
Hb:b ~= 0
r == a mod b
destruct (div_mod_unique b q (a/b) r (a mod b)); trivial.a, b, q, r:t
Hr:0 <= r < b \/ b < r <= 0
EQ:a == b * q + r
Hb:b ~= 0
0 <= a mod b < b \/ b < a mod b <= 0
a, b, q, r:t
Hr:0 <= r < b \/ b < r <= 0
EQ:a == b * q + r
Hb:b ~= 0
b * q + r == b * (a / b) + a mod b
destruct Hr; [left; apply mod_pos_bound|right; apply mod_neg_bound];
 intuition order.a, b, q, r:t
Hr:0 <= r < b \/ b < r <= 0
EQ:a == b * q + r
Hb:b ~= 0
b * q + r == b * (a / b) + a mod b
now rewrite <- div_mod.
Qed.

Theorem mod_unique_pos:
 forall a b q r, 0<=r<b -> a == b*q + r -> r == a mod b.forall a b q r : t,
0 <= r < b -> a == b * q + r -> r == a mod b
Proof.forall a b q r : t,
0 <= r < b -> a == b * q + r -> r == a mod b intros; apply mod_unique with q; auto. Qed.

Theorem mod_unique_neg:
 forall a b q r, b<r<=0 -> a == b*q + r -> r == a mod b.forall a b q r : t,
b < r <= 0 -> a == b * q + r -> r == a mod b
Proof.forall a b q r : t,
b < r <= 0 -> a == b * q + r -> r == a mod b intros; apply mod_unique with q; auto. Qed.

Sign rules

Ltac pos_or_neg a :=
 let LT := fresh "LT" in
 let LE := fresh "LE" in
 destruct (le_gt_cases 0 a) as [LE|LT]; [|rewrite <- opp_pos_neg in LT].

Fact mod_bound_or : forall a b, b~=0 -> 0<=a mod b<b \/ b<a mod b<=0.forall a b : t,
b ~= 0 -> 0 <= a mod b < b \/ b < a mod b <= 0
Proof.forall a b : t,
b ~= 0 -> 0 <= a mod b < b \/ b < a mod b <= 0
intros.a, b:t
H:b ~= 0
0 <= a mod b < b \/ b < a mod b <= 0
destruct (lt_ge_cases 0 b); [left|right].a, b:t
H:b ~= 0
H0:0 < b
0 <= a mod b < b
a, b:t
H:b ~= 0
H0:b <= 0
b < a mod b <= 0
 apply mod_pos_bound; trivial.a, b:t
H:b ~= 0
H0:b <= 0
b < a mod b <= 0 apply mod_neg_bound; order.
Qed.

Fact opp_mod_bound_or : forall a b, b~=0 ->
 0 <= -(a mod b) < -b \/ -b < -(a mod b) <= 0.forall a b : t,
b ~= 0 ->
0 <= - (a mod b) < - b \/ - b < - (a mod b) <= 0
Proof.forall a b : t,
b ~= 0 ->
0 <= - (a mod b) < - b \/ - b < - (a mod b) <= 0
intros.a, b:t
H:b ~= 0
0 <= - (a mod b) < - b \/ - b < - (a mod b) <= 0
destruct (lt_ge_cases 0 b); [right|left].a, b:t
H:b ~= 0
H0:0 < b
- b < - (a mod b) <= 0
a, b:t
H:b ~= 0
H0:b <= 0
0 <= - (a mod b) < - b
rewrite <- opp_lt_mono, opp_nonpos_nonneg.a, b:t
H:b ~= 0
H0:0 < b
a mod b < b /\ 0 <= a mod b
a, b:t
H:b ~= 0
H0:b <= 0
0 <= - (a mod b) < - b
 destruct (mod_pos_bound a b); intuition; order.a, b:t
H:b ~= 0
H0:b <= 0
0 <= - (a mod b) < - b
rewrite <- opp_lt_mono, opp_nonneg_nonpos.a, b:t
H:b ~= 0
H0:b <= 0
a mod b <= 0 /\ b < a mod b
 destruct (mod_neg_bound a b); intuition; order.
Qed.

Lemma div_opp_opp : forall a b, b~=0 -> -a/-b == a/b.forall a b : t, b ~= 0 -> - a / - b == a / b
Proof.forall a b : t, b ~= 0 -> - a / - b == a / b
intros.a, b:t
H:b ~= 0
- a / - b == a / b symmetry.a, b:t
H:b ~= 0
a / b == - a / - b apply div_unique with (- (a mod b)).a, b:t
H:b ~= 0
0 <= - (a mod b) < - b \/ - b < - (a mod b) <= 0
a, b:t
H:b ~= 0
- a == - b * (a / b) + - (a mod b)
now apply opp_mod_bound_or.a, b:t
H:b ~= 0
- a == - b * (a / b) + - (a mod b)
rewrite mul_opp_l, <- opp_add_distr, <- div_mod; order.
Qed.

Lemma mod_opp_opp : forall a b, b~=0 -> (-a) mod (-b) == - (a mod b).forall a b : t, b ~= 0 -> - a mod - b == - (a mod b)
Proof.forall a b : t, b ~= 0 -> - a mod - b == - (a mod b)
intros.a, b:t
H:b ~= 0
- a mod - b == - (a mod b) symmetry.a, b:t
H:b ~= 0
- (a mod b) == - a mod - b apply mod_unique with (a/b).a, b:t
H:b ~= 0
0 <= - (a mod b) < - b \/ - b < - (a mod b) <= 0
a, b:t
H:b ~= 0
- a == - b * (a / b) + - (a mod b)
now apply opp_mod_bound_or.a, b:t
H:b ~= 0
- a == - b * (a / b) + - (a mod b)
rewrite mul_opp_l, <- opp_add_distr, <- div_mod; order.
Qed.

With the current conventions, the other sign rules are rather complex.

Lemma div_opp_l_z :
 forall a b, b~=0 -> a mod b == 0 -> (-a)/b == -(a/b).forall a b : t,
b ~= 0 -> a mod b == 0 -> - a / b == - (a / b)
Proof.forall a b : t,
b ~= 0 -> a mod b == 0 -> - a / b == - (a / b)
intros a b Hb H.a, b:t
Hb:b ~= 0
H:a mod b == 0
- a / b == - (a / b) symmetry.a, b:t
Hb:b ~= 0
H:a mod b == 0
- (a / b) == - a / b apply div_unique with 0.a, b:t
Hb:b ~= 0
H:a mod b == 0
0 <= 0 < b \/ b < 0 <= 0
a, b:t
Hb:b ~= 0
H:a mod b == 0
- a == b * - (a / b) + 0
destruct (lt_ge_cases 0 b); [left|right]; intuition; order.a, b:t
Hb:b ~= 0
H:a mod b == 0
- a == b * - (a / b) + 0
rewrite <- opp_0, <- H.a, b:t
Hb:b ~= 0
H:a mod b == 0
- a == b * - (a / b) + - (a mod b)
rewrite mul_opp_r, <- opp_add_distr, <- div_mod; order.
Qed.

Lemma div_opp_l_nz :
 forall a b, b~=0 -> a mod b ~= 0 -> (-a)/b == -(a/b)-1.forall a b : t,
b ~= 0 -> a mod b ~= 0 -> - a / b == - (a / b) - 1
Proof.forall a b : t,
b ~= 0 -> a mod b ~= 0 -> - a / b == - (a / b) - 1
intros a b Hb H.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a / b == - (a / b) - 1 symmetry.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- (a / b) - 1 == - a / b apply div_unique with (b - a mod b).a, b:t
Hb:b ~= 0
H:a mod b ~= 0
0 <= b - a mod b < b \/ b < b - a mod b <= 0
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b)
destruct (lt_ge_cases 0 b); [left|right].a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:0 < b
0 <= b - a mod b < b
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:b <= 0
b < b - a mod b <= 0
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b)
rewrite le_0_sub.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:0 < b
a mod b <= b /\ b - a mod b < b
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:b <= 0
b < b - a mod b <= 0
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b) rewrite <- (sub_0_r b) at 5.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:0 < b
a mod b <= b /\ b - a mod b < b - 0
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:b <= 0
b < b - a mod b <= 0
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b) rewrite <- sub_lt_mono_l.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:0 < b
a mod b <= b /\ 0 < a mod b
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:b <= 0
b < b - a mod b <= 0
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b)
destruct (mod_pos_bound a b); intuition; order.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:b <= 0
b < b - a mod b <= 0
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b)
rewrite le_sub_0.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:b <= 0
b < b - a mod b /\ b <= a mod b
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b) rewrite <- (sub_0_r b) at 1.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:b <= 0
b - 0 < b - a mod b /\ b <= a mod b
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b) rewrite <- sub_lt_mono_l.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:b <= 0
a mod b < 0 /\ b <= a mod b
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b)
destruct (mod_neg_bound a b); intuition; order.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b)
rewrite <- (add_opp_r b), mul_sub_distr_l, mul_1_r, sub_add_simpl_r_l.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * - (a / b) + - (a mod b)
rewrite mul_opp_r, <-opp_add_distr, <-div_mod; order.
Qed.

Lemma mod_opp_l_z :
 forall a b, b~=0 -> a mod b == 0 -> (-a) mod b == 0.forall a b : t,
b ~= 0 -> a mod b == 0 -> - a mod b == 0
Proof.forall a b : t,
b ~= 0 -> a mod b == 0 -> - a mod b == 0
intros a b Hb H.a, b:t
Hb:b ~= 0
H:a mod b == 0
- a mod b == 0 symmetry.a, b:t
Hb:b ~= 0
H:a mod b == 0
0 == - a mod b apply mod_unique with (-(a/b)).a, b:t
Hb:b ~= 0
H:a mod b == 0
0 <= 0 < b \/ b < 0 <= 0
a, b:t
Hb:b ~= 0
H:a mod b == 0
- a == b * - (a / b) + 0
destruct (lt_ge_cases 0 b); [left|right]; intuition; order.a, b:t
Hb:b ~= 0
H:a mod b == 0
- a == b * - (a / b) + 0
rewrite <- opp_0, <- H.a, b:t
Hb:b ~= 0
H:a mod b == 0
- a == b * - (a / b) + - (a mod b)
rewrite mul_opp_r, <- opp_add_distr, <- div_mod; order.
Qed.

Lemma mod_opp_l_nz :
 forall a b, b~=0 -> a mod b ~= 0 -> (-a) mod b == b - a mod b.forall a b : t,
b ~= 0 -> a mod b ~= 0 -> - a mod b == b - a mod b
Proof.forall a b : t,
b ~= 0 -> a mod b ~= 0 -> - a mod b == b - a mod b
intros a b Hb H.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a mod b == b - a mod b symmetry.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
b - a mod b == - a mod b apply mod_unique with (-(a/b)-1).a, b:t
Hb:b ~= 0
H:a mod b ~= 0
0 <= b - a mod b < b \/ b < b - a mod b <= 0
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b)
destruct (lt_ge_cases 0 b); [left|right].a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:0 < b
0 <= b - a mod b < b
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:b <= 0
b < b - a mod b <= 0
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b)
rewrite le_0_sub.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:0 < b
a mod b <= b /\ b - a mod b < b
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:b <= 0
b < b - a mod b <= 0
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b) rewrite <- (sub_0_r b) at 5.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:0 < b
a mod b <= b /\ b - a mod b < b - 0
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:b <= 0
b < b - a mod b <= 0
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b) rewrite <- sub_lt_mono_l.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:0 < b
a mod b <= b /\ 0 < a mod b
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:b <= 0
b < b - a mod b <= 0
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b)
destruct (mod_pos_bound a b); intuition; order.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:b <= 0
b < b - a mod b <= 0
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b)
rewrite le_sub_0.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:b <= 0
b < b - a mod b /\ b <= a mod b
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b) rewrite <- (sub_0_r b) at 1.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:b <= 0
b - 0 < b - a mod b /\ b <= a mod b
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b) rewrite <- sub_lt_mono_l.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
H0:b <= 0
a mod b < 0 /\ b <= a mod b
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b)
destruct (mod_neg_bound a b); intuition; order.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * (- (a / b) - 1) + (b - a mod b)
rewrite <- (add_opp_r b), mul_sub_distr_l, mul_1_r, sub_add_simpl_r_l.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
- a == b * - (a / b) + - (a mod b)
rewrite mul_opp_r, <-opp_add_distr, <-div_mod; order.
Qed.

Lemma div_opp_r_z :
 forall a b, b~=0 -> a mod b == 0 -> a/(-b) == -(a/b).forall a b : t,
b ~= 0 -> a mod b == 0 -> a / - b == - (a / b)
Proof.forall a b : t,
b ~= 0 -> a mod b == 0 -> a / - b == - (a / b)
intros.a, b:t
H:b ~= 0
H0:a mod b == 0
a / - b == - (a / b) rewrite <- (opp_involutive a) at 1.a, b:t
H:b ~= 0
H0:a mod b == 0
- - a / - b == - (a / b)
rewrite div_opp_opp; auto using div_opp_l_z.
Qed.

Lemma div_opp_r_nz :
 forall a b, b~=0 -> a mod b ~= 0 -> a/(-b) == -(a/b)-1.forall a b : t,
b ~= 0 -> a mod b ~= 0 -> a / - b == - (a / b) - 1
Proof.forall a b : t,
b ~= 0 -> a mod b ~= 0 -> a / - b == - (a / b) - 1
intros.a, b:t
H:b ~= 0
H0:a mod b ~= 0
a / - b == - (a / b) - 1 rewrite <- (opp_involutive a) at 1.a, b:t
H:b ~= 0
H0:a mod b ~= 0
- - a / - b == - (a / b) - 1
rewrite div_opp_opp; auto using div_opp_l_nz.
Qed.

Lemma mod_opp_r_z :
 forall a b, b~=0 -> a mod b == 0 -> a mod (-b) == 0.forall a b : t,
b ~= 0 -> a mod b == 0 -> a mod - b == 0
Proof.forall a b : t,
b ~= 0 -> a mod b == 0 -> a mod - b == 0
intros.a, b:t
H:b ~= 0
H0:a mod b == 0
a mod - b == 0 rewrite <- (opp_involutive a) at 1.a, b:t
H:b ~= 0
H0:a mod b == 0
- - a mod - b == 0
now rewrite mod_opp_opp, mod_opp_l_z, opp_0.
Qed.

Lemma mod_opp_r_nz :
 forall a b, b~=0 -> a mod b ~= 0 -> a mod (-b) == (a mod b) - b.forall a b : t,
b ~= 0 -> a mod b ~= 0 -> a mod - b == a mod b - b
Proof.forall a b : t,
b ~= 0 -> a mod b ~= 0 -> a mod - b == a mod b - b
intros.a, b:t
H:b ~= 0
H0:a mod b ~= 0
a mod - b == a mod b - b rewrite <- (opp_involutive a) at 1.a, b:t
H:b ~= 0
H0:a mod b ~= 0
- - a mod - b == a mod b - b
rewrite mod_opp_opp, mod_opp_l_nz by trivial.a, b:t
H:b ~= 0
H0:a mod b ~= 0
- (b - a mod b) == a mod b - b
now rewrite opp_sub_distr, add_comm, add_opp_r.
Qed.

The sign of a mod b is the one of b (when it isn't null)

Lemma mod_sign_nz : forall a b, b~=0 -> a mod b ~= 0 ->
 sgn (a mod b) == sgn b.forall a b : t,
b ~= 0 -> a mod b ~= 0 -> sgn (a mod b) == sgn b
Proof.forall a b : t,
b ~= 0 -> a mod b ~= 0 -> sgn (a mod b) == sgn b
intros a b Hb H.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
sgn (a mod b) == sgn b destruct (lt_ge_cases 0 b) as [Hb'|Hb'].a, b:t
Hb:b ~= 0
H:a mod b ~= 0
Hb':0 < b
sgn (a mod b) == sgn b
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
Hb':b <= 0
sgn (a mod b) == sgn b
destruct (mod_pos_bound a b Hb').a, b:t
Hb:b ~= 0
H:a mod b ~= 0
Hb':0 < b
H0:0 <= a mod b
H1:a mod b < b
sgn (a mod b) == sgn b
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
Hb':b <= 0
sgn (a mod b) == sgn b rewrite 2 sgn_pos; order.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
Hb':b <= 0
sgn (a mod b) == sgn b
destruct (mod_neg_bound a b).a, b:t
Hb:b ~= 0
H:a mod b ~= 0
Hb':b <= 0
b < 0
a, b:t
Hb:b ~= 0
H:a mod b ~= 0
Hb':b <= 0
H0:b < a mod b
H1:a mod b <= 0
sgn (a mod b) == sgn b order.a, b:t
Hb:b ~= 0
H:a mod b ~= 0
Hb':b <= 0
H0:b < a mod b
H1:a mod b <= 0
sgn (a mod b) == sgn b rewrite 2 sgn_neg; order.
Qed.

Lemma mod_sign : forall a b, b~=0 -> sgn (a mod b) ~= -sgn b.forall a b : t, b ~= 0 -> sgn (a mod b) ~= - sgn b
Proof.forall a b : t, b ~= 0 -> sgn (a mod b) ~= - sgn b
intros a b Hb H.a, b:t
Hb:b ~= 0
H:sgn (a mod b) == - sgn b
False
destruct (eq_decidable (a mod b) 0) as [EQ|NEQ].a, b:t
Hb:b ~= 0
H:sgn (a mod b) == - sgn b
EQ:a mod b == 0
False
a, b:t
Hb:b ~= 0
H:sgn (a mod b) == - sgn b
NEQ:a mod b ~= 0
False
apply Hb, sgn_null_iff, opp_inj.a, b:t
Hb:b ~= 0
H:sgn (a mod b) == - sgn b
EQ:a mod b == 0
- sgn b == - 0
a, b:t
Hb:b ~= 0
H:sgn (a mod b) == - sgn b
NEQ:a mod b ~= 0
False now rewrite <- H, opp_0, EQ, sgn_0.a, b:t
Hb:b ~= 0
H:sgn (a mod b) == - sgn b
NEQ:a mod b ~= 0
False
apply Hb, sgn_null_iff.a, b:t
Hb:b ~= 0
H:sgn (a mod b) == - sgn b
NEQ:a mod b ~= 0
sgn b == 0 apply eq_mul_0_l with 2; try order'.a, b:t
Hb:b ~= 0
H:sgn (a mod b) == - sgn b
NEQ:a mod b ~= 0
sgn b * 2 == 0 nzsimpl'.a, b:t
Hb:b ~= 0
H:sgn (a mod b) == - sgn b
NEQ:a mod b ~= 0
sgn b + sgn b == 0
apply add_move_0_l.a, b:t
Hb:b ~= 0
H:sgn (a mod b) == - sgn b
NEQ:a mod b ~= 0
sgn b == - sgn b rewrite <- H.a, b:t
Hb:b ~= 0
H:sgn (a mod b) == - sgn b
NEQ:a mod b ~= 0
sgn b == sgn (a mod b) symmetry.a, b:t
Hb:b ~= 0
H:sgn (a mod b) == - sgn b
NEQ:a mod b ~= 0
sgn (a mod b) == sgn b now apply mod_sign_nz.
Qed.

Lemma mod_sign_mul : forall a b, b~=0 -> 0 <= (a mod b) * b.forall a b : t, b ~= 0 -> 0 <= a mod b * b
Proof.forall a b : t, b ~= 0 -> 0 <= a mod b * b
intros.a, b:t
H:b ~= 0
0 <= a mod b * b destruct (lt_ge_cases 0 b).a, b:t
H:b ~= 0
H0:0 < b
0 <= a mod b * b
a, b:t
H:b ~= 0
H0:b <= 0
0 <= a mod b * b
apply mul_nonneg_nonneg; destruct (mod_pos_bound a b); order.a, b:t
H:b ~= 0
H0:b <= 0
0 <= a mod b * b
apply mul_nonpos_nonpos; destruct (mod_neg_bound a b); order.
Qed.

A division by itself returns 1

Lemma div_same : forall a, a~=0 -> a/a == 1.forall a : t, a ~= 0 -> a / a == 1
Proof.forall a : t, a ~= 0 -> a / a == 1
intros.a:t
H:a ~= 0
a / a == 1 pos_or_neg a.a:t
H:a ~= 0
LE:0 <= a
a / a == 1
a:t
H:a ~= 0
LT:0 < - a
a / a == 1 apply div_same; order.a:t
H:a ~= 0
LT:0 < - a
a / a == 1
rewrite <- div_opp_opp by trivial.a:t
H:a ~= 0
LT:0 < - a
- a / - a == 1 now apply div_same.
Qed.

Lemma mod_same : forall a, a~=0 -> a mod a == 0.forall a : t, a ~= 0 -> a mod a == 0
Proof.forall a : t, a ~= 0 -> a mod a == 0
intros.a:t
H:a ~= 0
a mod a == 0 rewrite mod_eq, div_same by trivial.a:t
H:a ~= 0
a - a * 1 == 0 nzsimpl.a:t
H:a ~= 0
a - a == 0 apply sub_diag.
Qed.

A division of a small number by a bigger one yields zero.

Theorem div_small: forall a b, 0<=a<b -> a/b == 0.forall a b : t, 0 <= a < b -> a / b == 0
Proof.forall a b : t, 0 <= a < b -> a / b == 0 exact div_small. Qed.

Same situation, in term of modulo:

Theorem mod_small: forall a b, 0<=a<b -> a mod b == a.forall a b : t, 0 <= a < b -> a mod b == a
Proof.forall a b : t, 0 <= a < b -> a mod b == a exact mod_small. Qed.

Basic values of divisions and modulo.

Lemma div_0_l: forall a, a~=0 -> 0/a == 0.forall a : t, a ~= 0 -> 0 / a == 0
Proof.forall a : t, a ~= 0 -> 0 / a == 0
intros.a:t
H:a ~= 0
0 / a == 0 pos_or_neg a.a:t
H:a ~= 0
LE:0 <= a
0 / a == 0
a:t
H:a ~= 0
LT:0 < - a
0 / a == 0 apply div_0_l; order.a:t
H:a ~= 0
LT:0 < - a
0 / a == 0
rewrite <- div_opp_opp, opp_0 by trivial.a:t
H:a ~= 0
LT:0 < - a
0 / - a == 0 now apply div_0_l.
Qed.

Lemma mod_0_l: forall a, a~=0 -> 0 mod a == 0.forall a : t, a ~= 0 -> 0 mod a == 0
Proof.forall a : t, a ~= 0 -> 0 mod a == 0
intros; rewrite mod_eq, div_0_l; now nzsimpl.
Qed.

Lemma div_1_r: forall a, a/1 == a.forall a : t, a / 1 == a
Proof.forall a : t, a / 1 == a
intros.a:t
a / 1 == a symmetry.a:t
a == a / 1 apply div_unique with 0.a:t
0 <= 0 < 1 \/ 1 < 0 <= 0
a:t
a == 1 * a + 0 left.a:t
0 <= 0 < 1
a:t
a == 1 * a + 0 split; order || apply lt_0_1.a:t
a == 1 * a + 0
now nzsimpl.
Qed.

Lemma mod_1_r: forall a, a mod 1 == 0.forall a : t, a mod 1 == 0
Proof.forall a : t, a mod 1 == 0
intros.a:t
a mod 1 == 0 rewrite mod_eq, div_1_r; nzsimpl; auto using sub_diag.a:t
1 ~= 0
intro EQ; symmetry in EQ; revert EQ; apply lt_neq; apply lt_0_1.
Qed.

Lemma div_1_l: forall a, 1<a -> 1/a == 0.forall a : t, 1 < a -> 1 / a == 0
Proof.forall a : t, 1 < a -> 1 / a == 0 exact div_1_l. Qed.

Lemma mod_1_l: forall a, 1<a -> 1 mod a == 1.forall a : t, 1 < a -> 1 mod a == 1
Proof.forall a : t, 1 < a -> 1 mod a == 1 exact mod_1_l. Qed.

Lemma div_mul : forall a b, b~=0 -> (a*b)/b == a.forall a b : t, b ~= 0 -> a * b / b == a
Proof.forall a b : t, b ~= 0 -> a * b / b == a
intros.a, b:t
H:b ~= 0
a * b / b == a symmetry.a, b:t
H:b ~= 0
a == a * b / b apply div_unique with 0.a, b:t
H:b ~= 0
0 <= 0 < b \/ b < 0 <= 0
a, b:t
H:b ~= 0
a * b == b * a + 0
destruct (lt_ge_cases 0 b); [left|right]; split; order.a, b:t
H:b ~= 0
a * b == b * a + 0
nzsimpl; apply mul_comm.
Qed.

Lemma mod_mul : forall a b, b~=0 -> (a*b) mod b == 0.forall a b : t, b ~= 0 -> (a * b) mod b == 0
Proof.forall a b : t, b ~= 0 -> (a * b) mod b == 0
intros.a, b:t
H:b ~= 0
(a * b) mod b == 0 rewrite mod_eq, div_mul by trivial.a, b:t
H:b ~= 0
a * b - b * a == 0 rewrite mul_comm; apply sub_diag.
Qed.

Theorem div_unique_exact a b q: b~=0 -> a == b*q -> q == a/b.a, b, q:t
b ~= 0 -> a == b * q -> q == a / b
Proof.a, b, q:t
b ~= 0 -> a == b * q -> q == a / b
 intros Hb H.a, b, q:t
Hb:b ~= 0
H:a == b * q
q == a / b rewrite H, mul_comm.a, b, q:t
Hb:b ~= 0
H:a == b * q
q == q * b / b symmetry.a, b, q:t
Hb:b ~= 0
H:a == b * q
q * b / b == q now apply div_mul.
Qed.

Order results about mod and div

A modulo cannot grow beyond its starting point.

Theorem mod_le: forall a b, 0<=a -> 0<b -> a mod b <= a.forall a b : t, 0 <= a -> 0 < b -> a mod b <= a
Proof.forall a b : t, 0 <= a -> 0 < b -> a mod b <= a exact mod_le. Qed.

Theorem div_pos : forall a b, 0<=a -> 0<b -> 0<= a/b.forall a b : t, 0 <= a -> 0 < b -> 0 <= a / b
Proof.forall a b : t, 0 <= a -> 0 < b -> 0 <= a / b exact div_pos. Qed.

Lemma div_str_pos : forall a b, 0<b<=a -> 0 < a/b.forall a b : t, 0 < b <= a -> 0 < a / b
Proof.forall a b : t, 0 < b <= a -> 0 < a / b exact div_str_pos. Qed.

Lemma div_small_iff : forall a b, b~=0 -> (a/b==0 <-> 0<=a<b \/ b<a<=0).forall a b : t,
b ~= 0 -> a / b == 0 <-> 0 <= a < b \/ b < a <= 0
Proof.forall a b : t,
b ~= 0 -> a / b == 0 <-> 0 <= a < b \/ b < a <= 0
intros a b Hb.a, b:t
Hb:b ~= 0
a / b == 0 <-> 0 <= a < b \/ b < a <= 0
split.a, b:t
Hb:b ~= 0
a / b == 0 -> 0 <= a < b \/ b < a <= 0
a, b:t
Hb:b ~= 0
0 <= a < b \/ b < a <= 0 -> a / b == 0
intros EQ.a, b:t
Hb:b ~= 0
EQ:a / b == 0
0 <= a < b \/ b < a <= 0
a, b:t
Hb:b ~= 0
0 <= a < b \/ b < a <= 0 -> a / b == 0
rewrite (div_mod a b Hb), EQ; nzsimpl.a, b:t
Hb:b ~= 0
EQ:a / b == 0
0 <= a mod b < b \/ b < a mod b <= 0
a, b:t
Hb:b ~= 0
0 <= a < b \/ b < a <= 0 -> a / b == 0
now apply mod_bound_or.a, b:t
Hb:b ~= 0
0 <= a < b \/ b < a <= 0 -> a / b == 0
destruct 1.a, b:t
Hb:b ~= 0
H:0 <= a < b
a / b == 0
a, b:t
Hb:b ~= 0
H:b < a <= 0
a / b == 0 now apply div_small.a, b:t
Hb:b ~= 0
H:b < a <= 0
a / b == 0
rewrite <- div_opp_opp by trivial.a, b:t
Hb:b ~= 0
H:b < a <= 0
- a / - b == 0 apply div_small; trivial.a, b:t
Hb:b ~= 0
H:b < a <= 0
0 <= - a < - b
rewrite <- opp_lt_mono, opp_nonneg_nonpos; tauto.
Qed.

Lemma mod_small_iff : forall a b, b~=0 -> (a mod b == a <-> 0<=a<b \/ b<a<=0).forall a b : t,
b ~= 0 -> a mod b == a <-> 0 <= a < b \/ b < a <= 0
Proof.forall a b : t,
b ~= 0 -> a mod b == a <-> 0 <= a < b \/ b < a <= 0
intros.a, b:t
H:b ~= 0
a mod b == a <-> 0 <= a < b \/ b < a <= 0
rewrite <- div_small_iff, mod_eq by trivial.a, b:t
H:b ~= 0
a - b * (a / b) == a <-> a / b == 0
rewrite sub_move_r, <- (add_0_r a) at 1.a, b:t
H:b ~= 0
a + 0 == a + b * (a / b) <-> a / b == 0 rewrite add_cancel_l.a, b:t
H:b ~= 0
0 == b * (a / b) <-> a / b == 0
rewrite eq_sym_iff, eq_mul_0.a, b:t
H:b ~= 0
b == 0 \/ a / b == 0 <-> a / b == 0 tauto.
Qed.

As soon as the divisor is strictly greater than 1, the division is strictly decreasing.

Lemma div_lt : forall a b, 0<a -> 1<b -> a/b < a.forall a b : t, 0 < a -> 1 < b -> a / b < a
Proof.forall a b : t, 0 < a -> 1 < b -> a / b < a exact div_lt. Qed.

le is compatible with a positive division.

Lemma div_le_mono : forall a b c, 0<c -> a<=b -> a/c <= b/c.forall a b c : t, 0 < c -> a <= b -> a / c <= b / c
Proof.forall a b c : t, 0 < c -> a <= b -> a / c <= b / c
intros a b c Hc Hab.a, b, c:t
Hc:0 < c
Hab:a <= b
a / c <= b / c
rewrite lt_eq_cases in Hab.a, b, c:t
Hc:0 < c
Hab:a < b \/ a == b
a / c <= b / c destruct Hab as [LT|EQ];
 [|rewrite EQ; order].a, b, c:t
Hc:0 < c
LT:a < b
a / c <= b / c
rewrite <- lt_succ_r.a, b, c:t
Hc:0 < c
LT:a < b
a / c < S (b / c)
rewrite (mul_lt_mono_pos_l c) by order.a, b, c:t
Hc:0 < c
LT:a < b
c * (a / c) < c * S (b / c)
nzsimpl.a, b, c:t
Hc:0 < c
LT:a < b
c * (a / c) < c * (b / c) + c
rewrite (add_lt_mono_r _ _ (a mod c)).a, b, c:t
Hc:0 < c
LT:a < b
c * (a / c) + a mod c < c * (b / c) + c + a mod c
rewrite <- div_mod by order.a, b, c:t
Hc:0 < c
LT:a < b
a < c * (b / c) + c + a mod c
apply lt_le_trans with b; trivial.a, b, c:t
Hc:0 < c
LT:a < b
b <= c * (b / c) + c + a mod c
rewrite (div_mod b c) at 1 by order.a, b, c:t
Hc:0 < c
LT:a < b
c * (b / c) + b mod c <= c * (b / c) + c + a mod c
rewrite <- add_assoc, <- add_le_mono_l.a, b, c:t
Hc:0 < c
LT:a < b
b mod c <= c + a mod c
apply le_trans with (c+0).a, b, c:t
Hc:0 < c
LT:a < b
b mod c <= c + 0
a, b, c:t
Hc:0 < c
LT:a < b
c + 0 <= c + a mod c
nzsimpl; destruct (mod_pos_bound b c); order.a, b, c:t
Hc:0 < c
LT:a < b
c + 0 <= c + a mod c
rewrite <- add_le_mono_l.a, b, c:t
Hc:0 < c
LT:a < b
0 <= a mod c destruct (mod_pos_bound a c); order.
Qed.

In this convention, div performs Rounding-Toward-Bottom.

Since we cannot speak of rational values here, we express this fact by multiplying back by b, and this leads to separates statements according to the sign of b.

First, a/b is below the exact fraction ...

Lemma mul_div_le : forall a b, 0<b -> b*(a/b) <= a.forall a b : t, 0 < b -> b * (a / b) <= a
Proof.forall a b : t, 0 < b -> b * (a / b) <= a
intros.a, b:t
H:0 < b
b * (a / b) <= a
rewrite (div_mod a b) at 2; try order.a, b:t
H:0 < b
b * (a / b) <= b * (a / b) + a mod b
rewrite <- (add_0_r (b*(a/b))) at 1.a, b:t
H:0 < b
b * (a / b) + 0 <= b * (a / b) + a mod b
rewrite <- add_le_mono_l.a, b:t
H:0 < b
0 <= a mod b
now destruct (mod_pos_bound a b).
Qed.

Lemma mul_div_ge : forall a b, b<0 -> a <= b*(a/b).forall a b : t, b < 0 -> a <= b * (a / b)
Proof.forall a b : t, b < 0 -> a <= b * (a / b)
intros.a, b:t
H:b < 0
a <= b * (a / b) rewrite <- div_opp_opp, opp_le_mono, <-mul_opp_l by order.a, b:t
H:b < 0
- b * (- a / - b) <= - a
apply mul_div_le.a, b:t
H:b < 0
0 < - b now rewrite opp_pos_neg.
Qed.

... and moreover it is the larger such integer, since S(a/b) is strictly above the exact fraction.

Lemma mul_succ_div_gt: forall a b, 0<b -> a < b*(S (a/b)).forall a b : t, 0 < b -> a < b * S (a / b)
Proof.forall a b : t, 0 < b -> a < b * S (a / b)
intros.a, b:t
H:0 < b
a < b * S (a / b)
nzsimpl.a, b:t
H:0 < b
a < b * (a / b) + b
rewrite (div_mod a b) at 1; try order.a, b:t
H:0 < b
b * (a / b) + a mod b < b * (a / b) + b
rewrite <- add_lt_mono_l.a, b:t
H:0 < b
a mod b < b
destruct (mod_pos_bound a b); order.
Qed.

Lemma mul_succ_div_lt: forall a b, b<0 -> b*(S (a/b)) < a.forall a b : t, b < 0 -> b * S (a / b) < a
Proof.forall a b : t, b < 0 -> b * S (a / b) < a
intros.a, b:t
H:b < 0
b * S (a / b) < a rewrite <- div_opp_opp, opp_lt_mono, <-mul_opp_l by order.a, b:t
H:b < 0
- a < - b * S (- a / - b)
apply mul_succ_div_gt.a, b:t
H:b < 0
0 < - b now rewrite opp_pos_neg.
Qed.

NB: The four previous properties could be used as specifications for div.

Inequality mul_div_le is exact iff the modulo is zero.

Lemma div_exact : forall a b, b~=0 -> (a == b*(a/b) <-> a mod b == 0).forall a b : t,
b ~= 0 -> a == b * (a / b) <-> a mod b == 0
Proof.forall a b : t,
b ~= 0 -> a == b * (a / b) <-> a mod b == 0
intros.a, b:t
H:b ~= 0
a == b * (a / b) <-> a mod b == 0
rewrite (div_mod a b) at 1; try order.a, b:t
H:b ~= 0
b * (a / b) + a mod b == b * (a / b) <-> a mod b == 0
rewrite <- (add_0_r (b*(a/b))) at 2.a, b:t
H:b ~= 0
b * (a / b) + a mod b == b * (a / b) + 0 <->
a mod b == 0
apply add_cancel_l.
Qed.

Some additional inequalities about div.

Theorem div_lt_upper_bound:
  forall a b q, 0<b -> a < b*q -> a/b < q.forall a b q : t, 0 < b -> a < b * q -> a / b < q
Proof.forall a b q : t, 0 < b -> a < b * q -> a / b < q
intros.a, b, q:t
H:0 < b
H0:a < b * q
a / b < q
rewrite (mul_lt_mono_pos_l b) by trivial.a, b, q:t
H:0 < b
H0:a < b * q
b * (a / b) < b * q
apply le_lt_trans with a; trivial.a, b, q:t
H:0 < b
H0:a < b * q
b * (a / b) <= a
now apply mul_div_le.
Qed.

Theorem div_le_upper_bound:
  forall a b q, 0<b -> a <= b*q -> a/b <= q.forall a b q : t, 0 < b -> a <= b * q -> a / b <= q
Proof.forall a b q : t, 0 < b -> a <= b * q -> a / b <= q
intros.a, b, q:t
H:0 < b
H0:a <= b * q
a / b <= q
rewrite <- (div_mul q b) by order.a, b, q:t
H:0 < b
H0:a <= b * q
a / b <= q * b / b
apply div_le_mono; trivial.a, b, q:t
H:0 < b
H0:a <= b * q
a <= q * b now rewrite mul_comm.
Qed.

Theorem div_le_lower_bound:
  forall a b q, 0<b -> b*q <= a -> q <= a/b.forall a b q : t, 0 < b -> b * q <= a -> q <= a / b
Proof.forall a b q : t, 0 < b -> b * q <= a -> q <= a / b
intros.a, b, q:t
H:0 < b
H0:b * q <= a
q <= a / b
rewrite <- (div_mul q b) by order.a, b, q:t
H:0 < b
H0:b * q <= a
q * b / b <= a / b
apply div_le_mono; trivial.a, b, q:t
H:0 < b
H0:b * q <= a
q * b <= a now rewrite mul_comm.
Qed.

A division respects opposite monotonicity for the divisor

Lemma div_le_compat_l: forall p q r, 0<=p -> 0<q<=r -> p/r <= p/q.forall p q r : t,
0 <= p -> 0 < q <= r -> p / r <= p / q
Proof.forall p q r : t,
0 <= p -> 0 < q <= r -> p / r <= p / q exact div_le_compat_l. Qed.

Relations between usual operations and mod and div

Lemma mod_add : forall a b c, c~=0 ->
 (a + b * c) mod c == a mod c.forall a b c : t,
c ~= 0 -> (a + b * c) mod c == a mod c
Proof.forall a b c : t,
c ~= 0 -> (a + b * c) mod c == a mod c
intros.a, b, c:t
H:c ~= 0
(a + b * c) mod c == a mod c
symmetry.a, b, c:t
H:c ~= 0
a mod c == (a + b * c) mod c
apply mod_unique with (a/c+b); trivial.a, b, c:t
H:c ~= 0
0 <= a mod c < c \/ c < a mod c <= 0
a, b, c:t
H:c ~= 0
a + b * c == c * (a / c + b) + a mod c
now apply mod_bound_or.a, b, c:t
H:c ~= 0
a + b * c == c * (a / c + b) + a mod c
rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order.a, b, c:t
H:c ~= 0
a + b * c == a + c * b
now rewrite mul_comm.
Qed.

Lemma div_add : forall a b c, c~=0 ->
 (a + b * c) / c == a / c + b.forall a b c : t,
c ~= 0 -> (a + b * c) / c == a / c + b
Proof.forall a b c : t,
c ~= 0 -> (a + b * c) / c == a / c + b
intros.a, b, c:t
H:c ~= 0
(a + b * c) / c == a / c + b
apply (mul_cancel_l _ _ c); try order.a, b, c:t
H:c ~= 0
c * ((a + b * c) / c) == c * (a / c + b)
apply (add_cancel_r _ _ ((a+b*c) mod c)).a, b, c:t
H:c ~= 0
c * ((a + b * c) / c) + (a + b * c) mod c ==
c * (a / c + b) + (a + b * c) mod c
rewrite <- div_mod, mod_add by order.a, b, c:t
H:c ~= 0
a + b * c == c * (a / c + b) + a mod c
rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order.a, b, c:t
H:c ~= 0
a + b * c == a + c * b
now rewrite mul_comm.
Qed.

Lemma div_add_l: forall a b c, b~=0 ->
 (a * b + c) / b == a + c / b.forall a b c : t,
b ~= 0 -> (a * b + c) / b == a + c / b
Proof.forall a b c : t,
b ~= 0 -> (a * b + c) / b == a + c / b
 intros a b c.a, b, c:t
b ~= 0 -> (a * b + c) / b == a + c / b rewrite (add_comm _ c), (add_comm a).a, b, c:t
b ~= 0 -> (c + a * b) / b == c / b + a
 now apply div_add.
Qed.

Cancellations.

Lemma div_mul_cancel_r : forall a b c, b~=0 -> c~=0 ->
 (a*c)/(b*c) == a/b.forall a b c : t,
b ~= 0 -> c ~= 0 -> a * c / (b * c) == a / b
Proof.forall a b c : t,
b ~= 0 -> c ~= 0 -> a * c / (b * c) == a / b
intros.a, b, c:t
H:b ~= 0
H0:c ~= 0
a * c / (b * c) == a / b
symmetry.a, b, c:t
H:b ~= 0
H0:c ~= 0
a / b == a * c / (b * c)
apply div_unique with ((a mod b)*c).a, b, c:t
H:b ~= 0
H0:c ~= 0
0 <= a mod b * c < b * c \/ b * c < a mod b * c <= 0
a, b, c:t
H:b ~= 0
H0:c ~= 0
a * c == b * c * (a / b) + a mod b * c
(* ineqs *)
destruct (lt_ge_cases 0 c).a, b, c:t
H:b ~= 0
H0:c ~= 0
H1:0 < c
0 <= a mod b * c < b * c \/ b * c < a mod b * c <= 0
a, b, c:t
H:b ~= 0
H0:c ~= 0
H1:c <= 0
0 <= a mod b * c < b * c \/ b * c < a mod b * c <= 0
a, b, c:t
H:b ~= 0
H0:c ~= 0
a * c == b * c * (a / b) + a mod b * c
rewrite <-(mul_0_l c), <-2mul_lt_mono_pos_r, <-2mul_le_mono_pos_r by trivial.a, b, c:t
H:b ~= 0
H0:c ~= 0
H1:0 < c
0 <= a mod b < b \/ b < a mod b <= 0
a, b, c:t
H:b ~= 0
H0:c ~= 0
H1:c <= 0
0 <= a mod b * c < b * c \/ b * c < a mod b * c <= 0
a, b, c:t
H:b ~= 0
H0:c ~= 0
a * c == b * c * (a / b) + a mod b * c
now apply mod_bound_or.a, b, c:t
H:b ~= 0
H0:c ~= 0
H1:c <= 0
0 <= a mod b * c < b * c \/ b * c < a mod b * c <= 0
a, b, c:t
H:b ~= 0
H0:c ~= 0
a * c == b * c * (a / b) + a mod b * c
rewrite <-(mul_0_l c), <-2mul_lt_mono_neg_r, <-2mul_le_mono_neg_r by order.a, b, c:t
H:b ~= 0
H0:c ~= 0
H1:c <= 0
a mod b <= 0 /\ b < a mod b \/
a mod b < b /\ 0 <= a mod b
a, b, c:t
H:b ~= 0
H0:c ~= 0
a * c == b * c * (a / b) + a mod b * c
destruct (mod_bound_or a b); tauto.a, b, c:t
H:b ~= 0
H0:c ~= 0
a * c == b * c * (a / b) + a mod b * c
(* equation *)
rewrite (div_mod a b) at 1 by order.a, b, c:t
H:b ~= 0
H0:c ~= 0
(b * (a / b) + a mod b) * c ==
b * c * (a / b) + a mod b * c
rewrite mul_add_distr_r.a, b, c:t
H:b ~= 0
H0:c ~= 0
b * (a / b) * c + a mod b * c ==
b * c * (a / b) + a mod b * c
rewrite add_cancel_r.a, b, c:t
H:b ~= 0
H0:c ~= 0
b * (a / b) * c == b * c * (a / b)
rewrite <- 2 mul_assoc.a, b, c:t
H:b ~= 0
H0:c ~= 0
b * (a / b * c) == b * (c * (a / b)) now rewrite (mul_comm c).
Qed.

Lemma div_mul_cancel_l : forall a b c, b~=0 -> c~=0 ->
 (c*a)/(c*b) == a/b.forall a b c : t,
b ~= 0 -> c ~= 0 -> c * a / (c * b) == a / b
Proof.forall a b c : t,
b ~= 0 -> c ~= 0 -> c * a / (c * b) == a / b
intros.a, b, c:t
H:b ~= 0
H0:c ~= 0
c * a / (c * b) == a / b rewrite !(mul_comm c); now apply div_mul_cancel_r.
Qed.

Lemma mul_mod_distr_l: forall a b c, b~=0 -> c~=0 ->
  (c*a) mod (c*b) == c * (a mod b).forall a b c : t,
b ~= 0 ->
c ~= 0 -> (c * a) mod (c * b) == c * (a mod b)
Proof.forall a b c : t,
b ~= 0 ->
c ~= 0 -> (c * a) mod (c * b) == c * (a mod b)
intros.a, b, c:t
H:b ~= 0
H0:c ~= 0
(c * a) mod (c * b) == c * (a mod b)
rewrite <- (add_cancel_l _ _ ((c*b)* ((c*a)/(c*b)))).a, b, c:t
H:b ~= 0
H0:c ~= 0
c * b * (c * a / (c * b)) + (c * a) mod (c * b) ==
c * b * (c * a / (c * b)) + c * (a mod b)
rewrite <- div_mod.a, b, c:t
H:b ~= 0
H0:c ~= 0
c * a == c * b * (c * a / (c * b)) + c * (a mod b)
a, b, c:t
H:b ~= 0
H0:c ~= 0
c * b ~= 0
rewrite div_mul_cancel_l by trivial.a, b, c:t
H:b ~= 0
H0:c ~= 0
c * a == c * b * (a / b) + c * (a mod b)
a, b, c:t
H:b ~= 0
H0:c ~= 0
c * b ~= 0
rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order.a, b, c:t
H:b ~= 0
H0:c ~= 0
a == b * (a / b) + a mod b
a, b, c:t
H:b ~= 0
H0:c ~= 0
c * b ~= 0
apply div_mod; order.a, b, c:t
H:b ~= 0
H0:c ~= 0
c * b ~= 0
rewrite <- neq_mul_0; auto.
Qed.

Lemma mul_mod_distr_r: forall a b c, b~=0 -> c~=0 ->
  (a*c) mod (b*c) == (a mod b) * c.forall a b c : t,
b ~= 0 -> c ~= 0 -> (a * c) mod (b * c) == a mod b * c
Proof.forall a b c : t,
b ~= 0 -> c ~= 0 -> (a * c) mod (b * c) == a mod b * c
 intros.a, b, c:t
H:b ~= 0
H0:c ~= 0
(a * c) mod (b * c) == a mod b * c rewrite !(mul_comm _ c); now rewrite mul_mod_distr_l.
Qed.

Operations modulo.

Theorem mod_mod: forall a n, n~=0 ->
 (a mod n) mod n == a mod n.forall a n : t, n ~= 0 -> (a mod n) mod n == a mod n
Proof.forall a n : t, n ~= 0 -> (a mod n) mod n == a mod n
intros.a, n:t
H:n ~= 0
(a mod n) mod n == a mod n rewrite mod_small_iff by trivial.a, n:t
H:n ~= 0
0 <= a mod n < n \/ n < a mod n <= 0
now apply mod_bound_or.
Qed.

Lemma mul_mod_idemp_l : forall a b n, n~=0 ->
 ((a mod n)*b) mod n == (a*b) mod n.forall a b n : t,
n ~= 0 -> (a mod n * b) mod n == (a * b) mod n
Proof.forall a b n : t,
n ~= 0 -> (a mod n * b) mod n == (a * b) mod n
 intros a b n Hn.a, b, n:t
Hn:n ~= 0
(a mod n * b) mod n == (a * b) mod n symmetry.a, b, n:t
Hn:n ~= 0
(a * b) mod n == (a mod n * b) mod n
 rewrite (div_mod a n) at 1 by order.a, b, n:t
Hn:n ~= 0
((n * (a / n) + a mod n) * b) mod n ==
(a mod n * b) mod n
 rewrite add_comm, (mul_comm n), (mul_comm _ b).a, b, n:t
Hn:n ~= 0
(b * (a mod n + a / n * n)) mod n ==
(a mod n * b) mod n
 rewrite mul_add_distr_l, mul_assoc.a, b, n:t
Hn:n ~= 0
(b * (a mod n) + b * (a / n) * n) mod n ==
(a mod n * b) mod n
 intros.a, b, n:t
Hn:n ~= 0
(b * (a mod n) + b * (a / n) * n) mod n ==
(a mod n * b) mod n rewrite mod_add by trivial.a, b, n:t
Hn:n ~= 0
(b * (a mod n)) mod n == (a mod n * b) mod n
 now rewrite mul_comm.
Qed.

Lemma mul_mod_idemp_r : forall a b n, n~=0 ->
 (a*(b mod n)) mod n == (a*b) mod n.forall a b n : t,
n ~= 0 -> (a * (b mod n)) mod n == (a * b) mod n
Proof.forall a b n : t,
n ~= 0 -> (a * (b mod n)) mod n == (a * b) mod n
 intros.a, b, n:t
H:n ~= 0
(a * (b mod n)) mod n == (a * b) mod n rewrite !(mul_comm a).a, b, n:t
H:n ~= 0
(b mod n * a) mod n == (b * a) mod n now apply mul_mod_idemp_l.
Qed.

Theorem mul_mod: forall a b n, n~=0 ->
 (a * b) mod n == ((a mod n) * (b mod n)) mod n.forall a b n : t,
n ~= 0 -> (a * b) mod n == (a mod n * (b mod n)) mod n
Proof.forall a b n : t,
n ~= 0 -> (a * b) mod n == (a mod n * (b mod n)) mod n
 intros.a, b, n:t
H:n ~= 0
(a * b) mod n == (a mod n * (b mod n)) mod n now rewrite mul_mod_idemp_l, mul_mod_idemp_r.
Qed.

Lemma add_mod_idemp_l : forall a b n, n~=0 ->
 ((a mod n)+b) mod n == (a+b) mod n.forall a b n : t,
n ~= 0 -> (a mod n + b) mod n == (a + b) mod n
Proof.forall a b n : t,
n ~= 0 -> (a mod n + b) mod n == (a + b) mod n
 intros a b n Hn.a, b, n:t
Hn:n ~= 0
(a mod n + b) mod n == (a + b) mod n symmetry.a, b, n:t
Hn:n ~= 0
(a + b) mod n == (a mod n + b) mod n
 rewrite (div_mod a n) at 1 by order.a, b, n:t
Hn:n ~= 0
(n * (a / n) + a mod n + b) mod n ==
(a mod n + b) mod n
 rewrite <- add_assoc, add_comm, mul_comm.a, b, n:t
Hn:n ~= 0
(a mod n + b + a / n * n) mod n == (a mod n + b) mod n
 intros.a, b, n:t
Hn:n ~= 0
(a mod n + b + a / n * n) mod n == (a mod n + b) mod n now rewrite mod_add.
Qed.

Lemma add_mod_idemp_r : forall a b n, n~=0 ->
 (a+(b mod n)) mod n == (a+b) mod n.forall a b n : t,
n ~= 0 -> (a + b mod n) mod n == (a + b) mod n
Proof.forall a b n : t,
n ~= 0 -> (a + b mod n) mod n == (a + b) mod n
 intros.a, b, n:t
H:n ~= 0
(a + b mod n) mod n == (a + b) mod n rewrite !(add_comm a).a, b, n:t
H:n ~= 0
(b mod n + a) mod n == (b + a) mod n now apply add_mod_idemp_l.
Qed.

Theorem add_mod: forall a b n, n~=0 ->
 (a+b) mod n == (a mod n + b mod n) mod n.forall a b n : t,
n ~= 0 -> (a + b) mod n == (a mod n + b mod n) mod n
Proof.forall a b n : t,
n ~= 0 -> (a + b) mod n == (a mod n + b mod n) mod n
 intros.a, b, n:t
H:n ~= 0
(a + b) mod n == (a mod n + b mod n) mod n now rewrite add_mod_idemp_l, add_mod_idemp_r.
Qed.

With the current convention, the following result isn't always true with a negative last divisor. For instance 3/(-2)/(-2) = 1 ≠ 0 = 3 / (-2*-2) , or 5/2/(-2) = -1 ≠ -2 = 5 / (2*-2) .

Lemma div_div : forall a b c, b~=0 -> 0<c ->
 (a/b)/c == a/(b*c).forall a b c : t,
b ~= 0 -> 0 < c -> a / b / c == a / (b * c)
Proof.forall a b c : t,
b ~= 0 -> 0 < c -> a / b / c == a / (b * c)
 intros a b c Hb Hc.a, b, c:t
Hb:b ~= 0
Hc:0 < c
a / b / c == a / (b * c)
 apply div_unique with (b*((a/b) mod c) + a mod b).a, b, c:t
Hb:b ~= 0
Hc:0 < c
0 <= b * ((a / b) mod c) + a mod b < b * c \/
b * c < b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 (* begin 0<= ... <b*c \/ ... *)
 apply neg_pos_cases in Hb.a, b, c:t
Hb:b < 0 \/ 0 < b
Hc:0 < c
0 <= b * ((a / b) mod c) + a mod b < b * c \/
b * c < b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b) destruct Hb as [Hb|Hb].a, b, c:t
Hb:b < 0
Hc:0 < c
0 <= b * ((a / b) mod c) + a mod b < b * c \/
b * c < b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:0 < b
Hc:0 < c
0 <= b * ((a / b) mod c) + a mod b < b * c \/
b * c < b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 right.a, b, c:t
Hb:b < 0
Hc:0 < c
b * c < b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:0 < b
Hc:0 < c
0 <= b * ((a / b) mod c) + a mod b < b * c \/
b * c < b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 destruct (mod_pos_bound (a/b) c), (mod_neg_bound a b); trivial.a, b, c:t
Hb:b < 0
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:b < a mod b
H2:a mod b <= 0
b * c < b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:0 < b
Hc:0 < c
0 <= b * ((a / b) mod c) + a mod b < b * c \/
b * c < b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 split.a, b, c:t
Hb:b < 0
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:b < a mod b
H2:a mod b <= 0
b * c < b * ((a / b) mod c) + a mod b
a, b, c:t
Hb:b < 0
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:b < a mod b
H2:a mod b <= 0
b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:0 < b
Hc:0 < c
0 <= b * ((a / b) mod c) + a mod b < b * c \/
b * c < b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 apply le_lt_trans with (b*((a/b) mod c) + b).a, b, c:t
Hb:b < 0
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:b < a mod b
H2:a mod b <= 0
b * c <= b * ((a / b) mod c) + b
a, b, c:t
Hb:b < 0
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:b < a mod b
H2:a mod b <= 0
b * ((a / b) mod c) + b <
b * ((a / b) mod c) + a mod b
a, b, c:t
Hb:b < 0
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:b < a mod b
H2:a mod b <= 0
b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:0 < b
Hc:0 < c
0 <= b * ((a / b) mod c) + a mod b < b * c \/
b * c < b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 now rewrite <- mul_succ_r, <- mul_le_mono_neg_l, le_succ_l.a, b, c:t
Hb:b < 0
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:b < a mod b
H2:a mod b <= 0
b * ((a / b) mod c) + b <
b * ((a / b) mod c) + a mod b
a, b, c:t
Hb:b < 0
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:b < a mod b
H2:a mod b <= 0
b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:0 < b
Hc:0 < c
0 <= b * ((a / b) mod c) + a mod b < b * c \/
b * c < b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 now rewrite <- add_lt_mono_l.a, b, c:t
Hb:b < 0
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:b < a mod b
H2:a mod b <= 0
b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:0 < b
Hc:0 < c
0 <= b * ((a / b) mod c) + a mod b < b * c \/
b * c < b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 apply add_nonpos_nonpos; trivial.a, b, c:t
Hb:b < 0
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:b < a mod b
H2:a mod b <= 0
b * ((a / b) mod c) <= 0
a, b, c:t
Hb:0 < b
Hc:0 < c
0 <= b * ((a / b) mod c) + a mod b < b * c \/
b * c < b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 apply mul_nonpos_nonneg; order.a, b, c:t
Hb:0 < b
Hc:0 < c
0 <= b * ((a / b) mod c) + a mod b < b * c \/
b * c < b * ((a / b) mod c) + a mod b <= 0
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 left.a, b, c:t
Hb:0 < b
Hc:0 < c
0 <= b * ((a / b) mod c) + a mod b < b * c
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 destruct (mod_pos_bound (a/b) c), (mod_pos_bound a b); trivial.a, b, c:t
Hb:0 < b
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:0 <= a mod b
H2:a mod b < b
0 <= b * ((a / b) mod c) + a mod b < b * c
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 split.a, b, c:t
Hb:0 < b
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:0 <= a mod b
H2:a mod b < b
0 <= b * ((a / b) mod c) + a mod b
a, b, c:t
Hb:0 < b
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:0 <= a mod b
H2:a mod b < b
b * ((a / b) mod c) + a mod b < b * c
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 apply add_nonneg_nonneg; trivial.a, b, c:t
Hb:0 < b
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:0 <= a mod b
H2:a mod b < b
0 <= b * ((a / b) mod c)
a, b, c:t
Hb:0 < b
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:0 <= a mod b
H2:a mod b < b
b * ((a / b) mod c) + a mod b < b * c
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 apply mul_nonneg_nonneg; order.a, b, c:t
Hb:0 < b
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:0 <= a mod b
H2:a mod b < b
b * ((a / b) mod c) + a mod b < b * c
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 apply lt_le_trans with (b*((a/b) mod c) + b).a, b, c:t
Hb:0 < b
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:0 <= a mod b
H2:a mod b < b
b * ((a / b) mod c) + a mod b <
b * ((a / b) mod c) + b
a, b, c:t
Hb:0 < b
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:0 <= a mod b
H2:a mod b < b
b * ((a / b) mod c) + b <= b * c
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 now rewrite <- add_lt_mono_l.a, b, c:t
Hb:0 < b
Hc:0 < c
H:0 <= (a / b) mod c
H0:(a / b) mod c < c
H1:0 <= a mod b
H2:a mod b < b
b * ((a / b) mod c) + b <= b * c
a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 now rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l.a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 (* end 0<= ... < b*c \/ ... *)
 rewrite (div_mod a b) at 1 by order.a, b, c:t
Hb:b ~= 0
Hc:0 < c
b * (a / b) + a mod b ==
b * c * (a / b / c) + (b * ((a / b) mod c) + a mod b)
 rewrite add_assoc, add_cancel_r.a, b, c:t
Hb:b ~= 0
Hc:0 < c
b * (a / b) ==
b * c * (a / b / c) + b * ((a / b) mod c)
 rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order.a, b, c:t
Hb:b ~= 0
Hc:0 < c
a / b == c * (a / b / c) + (a / b) mod c
 apply div_mod; order.
Qed.

Similarly, the following result doesn't always hold when c<0. For instance 3 mod (-2*-2)) = 3 while 3 mod (-2) + (-2)*((3/-2) mod -2) = -1.

Lemma rem_mul_r : forall a b c, b~=0 -> 0<c ->
 a mod (b*c) == a mod b + b*((a/b) mod c).forall a b c : t,
b ~= 0 ->
0 < c ->
a mod (b * c) == a mod b + b * ((a / b) mod c)
Proof.forall a b c : t,
b ~= 0 ->
0 < c ->
a mod (b * c) == a mod b + b * ((a / b) mod c)
 intros a b c Hb Hc.a, b, c:t
Hb:b ~= 0
Hc:0 < c
a mod (b * c) == a mod b + b * ((a / b) mod c)
 apply add_cancel_l with (b*c*(a/(b*c))).a, b, c:t
Hb:b ~= 0
Hc:0 < c
b * c * (a / (b * c)) + a mod (b * c) ==
b * c * (a / (b * c)) +
(a mod b + b * ((a / b) mod c))
 rewrite <- div_mod by (apply neq_mul_0; split; order).a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / (b * c)) +
(a mod b + b * ((a / b) mod c))
 rewrite <- div_div by trivial.a, b, c:t
Hb:b ~= 0
Hc:0 < c
a ==
b * c * (a / b / c) + (a mod b + b * ((a / b) mod c))
 rewrite add_assoc, add_shuffle0, <- mul_assoc, <- mul_add_distr_l.a, b, c:t
Hb:b ~= 0
Hc:0 < c
a == b * (c * (a / b / c) + (a / b) mod c) + a mod b
 rewrite <- div_mod by order.a, b, c:t
Hb:b ~= 0
Hc:0 < c
a == b * (a / b) + a mod b
 apply div_mod; order.
Qed.

Lemma mod_div: forall a b, b~=0 ->
 a mod b / b == 0.forall a b : t, b ~= 0 -> a mod b / b == 0
Proof.forall a b : t, b ~= 0 -> a mod b / b == 0
 intros a b Hb.a, b:t
Hb:b ~= 0
a mod b / b == 0
 rewrite div_small_iff by assumption.a, b:t
Hb:b ~= 0
0 <= a mod b < b \/ b < a mod b <= 0
 auto using mod_bound_or.
Qed.

A last inequality:

Theorem div_mul_le:
 forall a b c, 0<=a -> 0<b -> 0<=c -> c*(a/b) <= (c*a)/b.forall a b c : t,
0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b
Proof.forall a b c : t,
0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b exact div_mul_le. Qed.

End ZDivProp.