Library Coq.Numbers.Natural.Abstract.NDiv
Euclidean Division
We benefit from what already exists for NZ
Let's now state again theorems, but without useless hypothesis.
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 previous inequality is exact iff the modulo is zero.
Some additionnal inequalities about div.
A division respects opposite monotonicity for the divisor
Relations between usual operations and mod and div
Cancellations.
Operations modulo.
A last inequality:
mod is related to divisibility