Library Coq.Numbers.NatInt.NZDiv
Euclidean Division
The first signatures will be common to all divisions over NZ, N and Z
The different divisions will only differ in the conditions
they impose on modulo. For NZ, we have only described the
behavior on positive numbers.
Uniqueness theorems
A division by itself returns 1
A division of a small number by a bigger one yields zero.
Same situation, in term of modulo:
Basic values of divisions and modulo.
Order results about mod and div
A modulo cannot grow beyond its starting point.
As soon as the divisor is strictly greater than 1,
the division is strictly decreasing.
le is compatible with a positive division.
The following two properties could be used as specification of div
The previous inequality is exact iff the modulo is zero.
Some additional inequalities about div.
A division respects opposite monotonicity for the divisor
Relations between usual operations and mod and div
Cancellations.
Operations modulo.
Theorem mod_mod:
forall a n, 0
<=a -> 0
<n ->
(a mod n) mod n == a mod n.
Lemma mul_mod_idemp_l :
forall a b n, 0
<=a -> 0
<=b -> 0
<n ->
((a mod n)*b) mod n == (a*b) mod n.
Lemma mul_mod_idemp_r :
forall a b n, 0
<=a -> 0
<=b -> 0
<n ->
(a*(b mod n)) mod n == (a*b) mod n.
Theorem mul_mod:
forall a b n, 0
<=a -> 0
<=b -> 0
<n ->
(a * b) mod n == ((a mod n) * (b mod n)) mod n.
Lemma add_mod_idemp_l :
forall a b n, 0
<=a -> 0
<=b -> 0
<n ->
((a mod n)+b) mod n == (a+b) mod n.
Lemma add_mod_idemp_r :
forall a b n, 0
<=a -> 0
<=b -> 0
<n ->
(a+(b mod n)) mod n == (a+b) mod n.
Theorem add_mod:
forall a b n, 0
<=a -> 0
<=b -> 0
<n ->
(a+b) mod n == (a mod n + b mod n) mod n.
Lemma div_div :
forall a b c, 0
<=a -> 0
<b -> 0
<c ->
(a/b)/c == a/(b*c).
Lemma mod_mul_r :
forall a b c, 0
<=a -> 0
<b -> 0
<c ->
a mod (b*c) == a mod b + b*((a/b) mod c).
Lemma add_mul_mod_distr_l:
forall a b c d, 0
<=a -> 0
<b -> 0
<=d<c ->
(c*a+d) mod (c*b) == c*(a mod b)+d.
Lemma add_mul_mod_distr_r:
forall a b c d, 0
<=a -> 0
<b -> 0
<=d<c ->
(a*c+d) mod (b*c) == (a mod b)*c+d.
Lemma mul_mod_distr_l:
forall a b c, 0
<=a -> 0
<b -> 0
<c ->
(c*a) mod (c*b) == c * (a mod b).
Lemma mul_mod_distr_r:
forall a b c, 0
<=a -> 0
<b -> 0
<c ->
(a*c) mod (b*c) == (a mod b) * c.
A last inequality:
mod is related to divisibility