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

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

assume - 1,1 are_congruent_mod n ; :: thesis: ( n = 2 or n = 1 )
then consider k being Integer such that
A1: n * k = - 2 ;
( k < 0 & n <> 0 ) by A1;
then A2: k <= - 1 by INT_1:8;

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

assume A3: n <> 2 ; :: thesis: n = 1

now :: thesis: not n <> 1

assume n <> 1 ; :: thesis: contradiction
then not n = 0 & ... & not n = 2 by A1, A3;
then not n <= 2 ;
then n >= 2 + 1 by NAT_1:13;
then ( n >= 3 & k < 0 ) by A1;
then A4: n * k <= 3 * k by XREAL_1:65;
3 * k <= 3 * (- 1) by A2, XREAL_1:64;
hence contradiction by A1, A4, XXREAL_0:2; :: thesis: verum

end;

hence n = 1 ; :: thesis: verum

end;

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

end;

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

per cases ( n = 2 or n = 1 ) by A5;

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;

end;