theorem Th9: :: RING_3:9

for g, m being Nat
for i being Integer st g divides i & g divides m holds
i / m = (i div g) / (m div g)