theorem Th12: :: EULER_2:12
for a, m, n being natural Number st a <> 0 & m > 1 & (a * n) mod m = n mod m & m,n are_coprime holds
a mod m = 1