theorem :: GROUP_24:80

for n, k being non zero Nat
for g being Element of (INT.Group n) st g = k holds
g " = (n - k) mod n