theorem Th8: :: RING_3:8

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