let n be Integer; :: thesis: ( - 1,1 are_congruent_mod n iff ( n = 2 or n = 1 or n = - 2 or n = - 1 ) )

hereby :: thesis: ( ( n = 2 or n = 1 or n = - 2 or n = - 1 ) implies - 1,1 are_congruent_mod n )

assume A1: - 1,1 are_congruent_mod n ; :: thesis: ( n = 2 or n = 1 or n = - 2 or n = - 1 )
then consider k being Integer such that
A2: n * k = - 2 ;

now :: thesis: ( ( n >= 0 & ( n = 2 or n = 1 or n = - 2 or n = - 1 ) ) or ( n < 0 & ( n = 2 or n = 1 or n = - 2 or n = - 1 ) ) )

per cases ( n >= 0 or n < 0 ) ;

case n >= 0 ; :: thesis: ( n = 2 or n = 1 or n = - 2 or n = - 1 )

then n in NAT by INT_1:3;
then reconsider m = n as Nat ;
( m = 1 or m = 2 ) by A1, Th19;
hence ( n = 2 or n = 1 or n = - 2 or n = - 1 ) ; :: thesis: verum

end;

case A3: n < 0 ; :: thesis: ( n = 2 or n = 1 or n = - 2 or n = - 1 )

then A4: k > 0 by A2;
then A5: k >= 0 + 1 by INT_1:7;

now :: thesis: ( n <> - 2 implies n = - 1 )

assume A6: n <> - 2 ; :: thesis: n = - 1

now :: thesis: not n <> - 1

assume A7: n <> - 1 ; :: thesis: contradiction
n <= - 1 by A3, INT_1:8;
then n < - 1 by A7, XXREAL_0:1;
then n + 1 <= - 1 by INT_1:7;
then (n + 1) - 1 <= (- 1) - 1 by XREAL_1:9;
then n < - 2 by A6, XXREAL_0:1;
then n + 1 <= - 2 by INT_1:7;
then (n + 1) - 1 <= (- 2) - 1 by XREAL_1:9;
then A8: n * k <= (- 3) * k by A4, XREAL_1:64;
(- 3) * k <= (- 3) * 1 by A5, XREAL_1:65;
hence contradiction by A2, A8, XXREAL_0:2; :: thesis: verum

end;

hence n = - 1 ; :: thesis: verum

end;

hence ( n = 2 or n = 1 or n = - 2 or n = - 1 ) ; :: thesis: verum

end;

end;

end;

hence ( n = 2 or n = 1 or n = - 2 or n = - 1 ) ; :: thesis: verum

end;

assume A9: ( n = 2 or n = 1 or n = - 2 or n = - 1 ) ; :: thesis: - 1,1 are_congruent_mod n

per cases ( n = 2 or n = 1 or n = - 2 or n = - 1 ) by A9;

suppose n = 2 ; :: thesis: - 1,1 are_congruent_mod n

then n * (- 1) = - 2 ;
hence - 1,1 are_congruent_mod n ; :: thesis: verum

end;

suppose n = 1 ; :: thesis: - 1,1 are_congruent_mod n

hence - 1,1 are_congruent_mod n by INT_1:13; :: thesis: verum

end;

suppose n = - 2 ; :: thesis: - 1,1 are_congruent_mod n

hence - 1,1 are_congruent_mod n ; :: thesis: verum

end;

suppose n = - 1 ; :: thesis: - 1,1 are_congruent_mod n

then n * (- 1) = 1 ;
hence - 1,1 are_congruent_mod n by INT_1:20, INT_1:13; :: thesis: verum

end;

end;