let n, n1, n2 be Nat; for x, y being Integer
for a being non trivial Nat st n1 <= 4 * n & n2 <= 4 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) & not n1,n2 are_congruent_mod 2 * n holds
n1, - n2 are_congruent_mod 2 * n
let x, y be Integer; for a being non trivial Nat st n1 <= 4 * n & n2 <= 4 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) & not n1,n2 are_congruent_mod 2 * n holds
n1, - n2 are_congruent_mod 2 * n
let a be non trivial Nat; ( n1 <= 4 * n & n2 <= 4 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) & not n1,n2 are_congruent_mod 2 * n implies n1, - n2 are_congruent_mod 2 * n )
assume A1:
( n1 <= 4 * n & n2 <= 4 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) )
; ( n1,n2 are_congruent_mod 2 * n or n1, - n2 are_congruent_mod 2 * n )
then A2:
y,x are_congruent_mod Px (a,n)
by INT_1:14;
per cases
( ( n1 <= 2 * n & n2 <= 2 * n ) or ( n1 > 2 * n & n2 > 2 * n ) or ( n1 <= 2 * n & 2 * n < n2 ) or ( n2 <= 2 * n & 2 * n < n1 ) )
;
end;