theorem Th5: :: REAL_3:5

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