for a, m being Element of NAT st a <> 0 & m > 1 & a,m are_coprime holds
for b, x being Integer st ((a * x) - b) mod m = 0 holds
[x,(b * (a |^ ((Euler m) -' 1)))] in Cong m