let i, j, n be Nat; :: thesis: ( i <= j & j < n & i,j are_congruent_mod n implies i = j )

assume A1: ( i <= j & j < n & i,j are_congruent_mod n ) ; :: thesis: i = j

then consider x being Integer such that

A2: n * x = i - j by INT_1:def 5;

( i - j <= i - 0 & i < n ) by XREAL_1:10, A1, XXREAL_0:2;

then n * x < n * 1 by A2, XXREAL_0:2;

then A3: x < 0 + 1 by XREAL_1:64;

( i - j >= 0 - j & - j > - n ) by XREAL_1:9, XREAL_1:24, A1;

then n * x > n * (- 1) by A2, XXREAL_0:2;

then x > - 1 by XREAL_1:64;

then x >= (- 1) + 1 by INT_1:7;

then x = 0 by A3, INT_1:7;

hence i = j by A2; :: thesis: verum

assume A1: ( i <= j & j < n & i,j are_congruent_mod n ) ; :: thesis: i = j

then consider x being Integer such that

A2: n * x = i - j by INT_1:def 5;

( i - j <= i - 0 & i < n ) by XREAL_1:10, A1, XXREAL_0:2;

then n * x < n * 1 by A2, XXREAL_0:2;

then A3: x < 0 + 1 by XREAL_1:64;

( i - j >= 0 - j & - j > - n ) by XREAL_1:9, XREAL_1:24, A1;

then n * x > n * (- 1) by A2, XXREAL_0:2;

then x > - 1 by XREAL_1:64;

then x >= (- 1) + 1 by INT_1:7;

then x = 0 by A3, INT_1:7;

hence i = j by A2; :: thesis: verum