theorem Th7: :: RING_3:7

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