theorem Th4: :: EULER_2:4

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