let i, j, n be Nat; :: thesis: for a being non trivial Nat st 0 < i & i <= n & 0 <= j & j < 4 * n & Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & not j = i holds
j + i = 4 * n
let a be non trivial Nat; :: thesis: ( 0 < i & i <= n & 0 <= j & j < 4 * n & Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & not j = i implies j + i = 4 * n )
set P = Px (a,n);
assume A1: ( 0 < i & i <= n & 0 <= j & j < 4 * n & Px (a,i), Px (a,j) are_congruent_mod Px (a,n) ) ; :: thesis: ( j = i or j + i = 4 * n )
then A2: Px (a,j), Px (a,i) are_congruent_mod Px (a,n) by INT_1:14;
reconsider j4n = (4 * n) - j as Nat by A1, NAT_1:21;
Px (a,|.((4 * n) + (- j4n)).|), Px (a,|.(- j4n).|) are_congruent_mod Px (a,|.n.|) by Th18;
then A3: Px (a,i), Px (a,j4n) are_congruent_mod Px (a,n) by A1, INT_1:15;
then A4: Px (a,j4n), Px (a,i) are_congruent_mod Px (a,n) by INT_1:14;
n <= n + n by NAT_1:11;
then A5: i <= n + n by A1, XXREAL_0:2;

per cases ( j <= 2 * n or j > 2 * n ) ;

suppose A6: j <= 2 * n ; :: thesis: ( j = i or j + i = 4 * n )

per cases ( i <= j or j < i ) ;

suppose i <= j ; :: thesis: ( j = i or j + i = 4 * n )

hence ( j = i or j + i = 4 * n ) by A6, Th21, A1; :: thesis: verum

end;

suppose j < i ; :: thesis: ( j = i or j + i = 4 * n )

then ( ( j = 0 & i = 2 & a = 2 & n = 1 ) or j = i ) by A6, Th21, A5, A2;
hence ( j = i or j + i = 4 * n ) by A1; :: thesis: verum

end;

end;

end;

suppose A7: j > 2 * n ; :: thesis: ( j = i or j + i = 4 * n )

then A8: j4n < (4 * n) - (2 * n) by XREAL_1:10;

per cases ( i <= j4n or j4n < i ) ;

suppose i <= j4n ; :: thesis: ( j = i or j + i = 4 * n )

then i = j4n by A3, A8, Th21, A1;
hence ( j = i or j + i = 4 * n ) ; :: thesis: verum

end;

suppose j4n < i ; :: thesis: ( j = i or j + i = 4 * n )

then ( ( j4n = 0 & i = 2 & a = 2 & n = 1 ) or j4n = i ) by A4, A7, Th21, A5;
hence ( j = i or j + i = 4 * n ) by A1; :: thesis: verum

end;

end;

end;

end;