theorem Th6: :: RING_3:6

for n being Nat
for i being Integer st n divides i holds
i div n = i / n