for i, j being Integer st i >= 0 & j >= 0 holds
( |.i.| mod |.j.| = i mod j & |.i.| div |.j.| = i div j )