theorem :: RING_3:12

for m, n being Nat st 0 < m & m * n divides m holds
n = 1