theorem :: RING_3:18

for m being Nat
for i being Integer st m <> 0 holds
( denominator (- (i / m)) = m / ((- i) gcd m) & numerator (- (i / m)) = (- i) / ((- i) gcd m) )