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