theorem :: EULER_2:21

for a, m being Nat st m is prime holds
a |^ m,a are_congruent_mod m