for n being Nat
for a being non trivial Nat holds Py (a,n),n are_congruent_mod a - 1