Re: [mizar] Integer division and modulus/remainder in Mizar

[John Harrison <John.Harrison@cl.cam.ac.uk>]

Hi Andrzej,

| So, 0 <= i mod 0 < |0| ?

Ahem :-) When I wrote:

| Boute distinguishes three main possibilities, all of which satisfy
| that law for nonzero divisor. (Like Freek, I support i div 0 = 0 and i
| mod 0 = i so it holds even for zero divisors, and I've recently
| changed HOL Light's definitions accordingly.)

by "that law" I just meant the division law i = (i div j)*j + i mod j.
The characterizing properties of the three approaches to division
were just intended for nonzero divisors, and my introduction of the
case of zero was meant to be a separate question. It was probably
unwise of me to fold these together.

John.