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

[Freek Wiedijk <freek@cs.ru.nl>]

Andrzej:

>and always   0 <= abs(i mod j) <= abs j

So John apparently prefers to have

	0 <= i mod j < abs j

for negative j, although he didn't explain why.

Also, can you tell us what was the reason for taking

	i mod 0 = 0

instead of

	i mod 0 = i

?

Freek