for i, j, n being Nat
for a being non trivial Nat st 0 < i & i <= n & Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & not j,i are_congruent_mod 4 * n holds
j, - i are_congruent_mod 4 * n