theorem Th3: :: EULER_2:3

for a, b, m being Nat st a <> 0 & b <> 0 & m <> 0 & a,m are_coprime & b,m are_coprime holds
m,(a * b) mod m are_coprime