theorem Th4: :: REAL_3:4

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