theorem Th76: :: NUMBER15:76

for m being Nat
for i being Integer st m <> 0 holds
i div (i gcd m),m div (i gcd m) are_coprime by RING_3:14;