theorem Th10: :: RING_3:10

for m being Nat
for i being Integer holds i / m = (i div (i gcd m)) / (m div (i gcd m))