for n, m being Nat st m mod n = 0 holds
m / n = m div n