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

[trybulec <trybulec@math.uwb.edu.pl>]

Freek Wiedijk wrote:

Andrzej:

  

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

So John apparently prefers to have

	0 <= i mod j < abs j
  

I would like it. Actually, I was certain that it is the case in Mizar. Well, Mizar has a different opinion. But I would like
to have
     i = (i div j)*j + i mod j,
too. We can't probably have both?

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

It was a simultaneous job. I have sent a message with an explanation seconds before I get this one.

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

	i mod 0 = 0

instead of

	i mod 0 = i

?

Freek