for a, m being Nat st a <> 0 & m > 1 & a,m are_coprime holds
(a |^ (Euler m)) mod m = 1