[mizar] Integer division and modulus/remainder in Mizar

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

I'm curious how Mizar defines division and modulus of integers where
one or both arguments are negative.

This is a well-known area where programming languages disagree or are
undefined, so I'm doing a little survey of some of the world's leading
theorem provers to see if there is a consensus there.

John.