let i, j, n be Nat; :: thesis: for a being non trivial Nat st i <= j & j <= 2 * n & Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & not ( i = 0 & j = 2 & a = 2 & n = 1 ) holds
i = j
let a be non trivial Nat; :: thesis: ( i <= j & j <= 2 * n & Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & not ( i = 0 & j = 2 & a = 2 & n = 1 ) implies i = j )
set P = Px (a,n);
assume A1: ( i <= j & j <= 2 * n & Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & ( not i = 0 or not j = 2 or not a = 2 or not n = 1 ) & i <> j ) ; :: thesis: contradiction
reconsider j2n = (2 * n) - j as Nat by A1, NAT_1:21;
A2: 0 , Px (a,n) are_congruent_mod Px (a,n) by INT_1:12;
A3: i <= 2 * n by A1, XXREAL_0:2;
( i < n or i = n or n < i ) by XXREAL_0:1;

per cases then ( ( i < n & j < n ) or ( i < n & j = n ) or ( i < n & j > n ) or ( i = n & j > n ) or ( i > n & j > n ) ) by A1, XXREAL_0:1, XXREAL_0:2;

suppose ( i < n & j < n ) ; :: thesis: contradiction

hence contradiction by A1, Lm8; :: thesis: verum

end;

suppose A4: ( i < n & j = n ) ; :: thesis: contradiction

then Px (a,n), Px (a,i) are_congruent_mod Px (a,n) by A1, INT_1:14;
then A5: (Px (a,n)) - (Px (a,n)), Px (a,i) are_congruent_mod Px (a,n) by INT_1:22;
Px (a,i) < Px (a,n) by A4, Th19;
then 0 = Px (a,i) by A5, Lm7;
hence contradiction ; :: thesis: verum

end;

suppose A6: ( i < n & j > n ) ; :: thesis: contradiction

(2 * n) + (- j2n) = j ;
then Px (a,|.j.|), - (Px (a,|.(- j2n).|)) are_congruent_mod Px (a,|.n.|) by Th17;
then Px (a,|.i.|), - (Px (a,j2n)) are_congruent_mod Px (a,n) by A1, INT_1:15;
then A7: (Px (a,|.i.|)) + 0,(- (Px (a,j2n))) + (Px (a,n)) are_congruent_mod Px (a,n) by A2, INT_1:16;
A8: (2 * n) - j < (2 * n) - n by A6, XREAL_1:15;
then reconsider Pj = (Px (a,n)) - (Px (a,j2n)) as Nat by NAT_1:21, HILB10_1:10;
A9: Px (a,i) < Px (a,n) by A6, Th19;
Pj < (Px (a,n)) - 0 by XREAL_1:15;
then A10: Px (a,i) = Pj by A9, A7, Lm7;

per cases ( not a = 2 or not n = 1 or ( a = 2 & n = 1 ) ) ;

suppose ( not a = 2 or not n = 1 ) ; :: thesis: contradiction

then ( Px (a,i) < (Px (a,n)) / 2 & Px (a,j2n) < (Px (a,n)) / 2 ) by A6, A8, Lm9;
then ( (Px (a,i)) + (Px (a,j2n)) < ((Px (a,n)) / 2) + ((Px (a,n)) / 2) & ((Px (a,n)) / 2) + ((Px (a,n)) / 2) = Px (a,n) ) by XREAL_1:8;
hence contradiction by A10; :: thesis: verum

end;

suppose A11: ( a = 2 & n = 1 ) ; :: thesis: contradiction

then ( i = 0 & j >= 1 + 1 ) by A6, NAT_1:13, NAT_1:14;
hence contradiction by A1, A11, XXREAL_0:1; :: thesis: verum

end;

end;

end;

suppose A12: ( i = n & j > n ) ; :: thesis: contradiction

(2 * n) + (- j2n) = j ;
then Px (a,|.j.|), - (Px (a,|.(- j2n).|)) are_congruent_mod Px (a,|.n.|) by Th17;
then Px (a,n), - (Px (a,j2n)) are_congruent_mod Px (a,n) by A12, A1, INT_1:15;
then (Px (a,n)) + 0,(- (Px (a,j2n))) + (Px (a,n)) are_congruent_mod Px (a,n) by A2, INT_1:16;
then A13: (Px (a,n)) - (Px (a,n)),(- (Px (a,j2n))) + (Px (a,n)) are_congruent_mod Px (a,n) by INT_1:22;
(2 * n) - j <= (2 * n) - n by A12, XREAL_1:15;
then reconsider Pj = (Px (a,n)) - (Px (a,j2n)) as Nat by NAT_1:21, HILB10_1:10;
Pj < (Px (a,n)) - 0 by XREAL_1:15;
then 0 = Pj by A13, Lm7;
then (2 * n) - j = n by Th20;
hence contradiction by A12; :: thesis: verum

end;

suppose ( i > n & j > n ) ; :: thesis: contradiction

hence contradiction by A1, Lm10, A3; :: thesis: verum

end;

end;