for a being Nat
for b, n being non zero Nat st a mod b = 1 holds
(a |^ n) mod b = 1