for n, n1, n2 being Nat
for a being non trivial Nat st Py (a,n1), Py (a,n2) are_congruent_mod Px (a,n) & n > 0 & not n1,n2 are_congruent_mod 2 * n holds
n1, - n2 are_congruent_mod 2 * n