let i, j be Integer; :: thesis: for n being Nat st n < j & i,n are_congruent_mod j holds
i mod j = n
let n be Nat; :: thesis: ( n < j & i,n are_congruent_mod j implies i mod j = n )
assume A1: ( n < j & i,n are_congruent_mod j ) ; :: thesis: i mod j = n
then consider x being Integer such that
A2: j * x = i - n ;
A3: i = ((i div j) * j) + (i mod j) by A1, INT_1:59;

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

suppose n = 0 ; :: thesis: i mod j = n

hence i mod j = n by A1, INT_1:62; :: thesis: verum

end;

suppose A5: n <> 0 ; :: thesis: i mod j = n

A6: i / j = ((j * x) + n) * (j ") by A2, XCMPLX_0:def 9
.= (x * (j * (j "))) + (n * (j "))
.= (x * 1) + (n * (j ")) by A1, XCMPLX_0:def 7 ;
then A7: x <= i / j by A5, A1, XREAL_1:29;
A8: (i / j) - 1 = x + ((n * (j ")) - 1) by A6;
A9: n / j < j / j by A1, XREAL_1:74;
j / j = j * (j ") by XCMPLX_0:def 9
.= 1 by A1, XCMPLX_0:def 7 ;
then n * (j ") < 1 by A9, XCMPLX_0:def 9;
then (n * (j ")) - 1 < 1 - 1 by XREAL_1:9;
then (i / j) - 1 < x by A8, XREAL_1:30;
then i div j = x by A7, INT_1:def 6;
hence i mod j = n by A2, A3; :: thesis: verum

end;

end;