for n, p being Nat
for a being non trivial Nat holds Px (a,n),(p |^ n) + ((Py (a,n)) * (a - p)) are_congruent_mod (((2 * a) * p) - (p ^2)) - 1