for a, b, m being Integer st m > 0 & a,m are_coprime holds
ex n being Nat st ((a * n) - b) mod m = 0