for a, b being Integer
for m being Nat st (a * b) mod m = 1 & a mod m = 1 holds
b mod m = 1