let i, j, n be Nat; :: thesis: 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
let a be non trivial Nat; :: thesis: ( 0 < i & i <= n & Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & not j,i are_congruent_mod 4 * n implies j, - i are_congruent_mod 4 * n )
set m = j mod (4 * n);
set d = j div (4 * n);
assume A1: ( 0 < i & i <= n & Px (a,i), Px (a,j) are_congruent_mod Px (a,n) ) ; :: thesis: ( j,i are_congruent_mod 4 * n or j, - i are_congruent_mod 4 * n )
then A2: j = ((j div (4 * n)) * (4 * n)) + (j mod (4 * n)) by INT_1:59;
then A3: Px (a,|.j.|), Px (a,|.(j mod (4 * n)).|) are_congruent_mod Px (a,|.n.|) by Th23;
j mod (4 * n) < 4 * n by A1, INT_1:58;

per cases then ( j mod (4 * n) = i or (j mod (4 * n)) + i = 4 * n ) by A3, Th22, A1, INT_1:15;

suppose j mod (4 * n) = i ; :: thesis: ( j,i are_congruent_mod 4 * n or j, - i are_congruent_mod 4 * n )

then 4 * n divides j - i by A1, PEPIN:8;
hence ( j,i are_congruent_mod 4 * n or j, - i are_congruent_mod 4 * n ) by INT_2:15; :: thesis: verum

end;

suppose (j mod (4 * n)) + i = 4 * n ; :: thesis: ( j,i are_congruent_mod 4 * n or j, - i are_congruent_mod 4 * n )

then 4 * n divides (j mod (4 * n)) - (- i) ;
then A4: j mod (4 * n), - i are_congruent_mod 4 * n by INT_2:15;
j - (j mod (4 * n)) = (j div (4 * n)) * (4 * n) by A2;
then j,j mod (4 * n) are_congruent_mod 4 * n by INT_1:def 5;
hence ( j,i are_congruent_mod 4 * n or j, - i are_congruent_mod 4 * n ) by A4, INT_1:15; :: thesis: verum

end;

end;