for x, y being Integer
for a being non trivial Nat holds (sgn ((2 * x) + y)) * (Py (a,|.((2 * x) + y).|)), - ((sgn y) * (Py (a,|.y.|))) are_congruent_mod Px (a,|.x.|)