let n be natural number ; :: thesis: ( n > 0 implies for a being Integer holds
( a mod n >= 0 & a mod n < n ) )
assume A1: n > 0 ; :: thesis: for a being Integer holds
( a mod n >= 0 & a mod n < n )
let a be Integer; :: thesis: ( a mod n >= 0 & a mod n < n )

now

a div n = [\(a / n)/] by INT_1:def 7;
then a div n <= a / n by INT_1:def 4;
then (a div n) * n <= (a / n) * n by XREAL_1:66;
then (a div n) * n <= (a * (n " )) * n by XCMPLX_0:def 9;
then (a div n) * n <= a * ((n " ) * n) ;
then (a div n) * n <= a * 1 by A1, XCMPLX_0:def 7;
then ((a div n) * n) - ((a div n) * n) <= a - ((a div n) * n) by XREAL_1:11;
hence 0 <= a mod n by INT_1:def 8; :: thesis: not a mod n >= n
assume a mod n >= n ; :: thesis: contradiction
then a - ((a div n) * n) >= n by A1, INT_1:def 8;
then (a + (- ((a div n) * n))) + ((a div n) * n) >= n + ((a div n) * n) by XREAL_1:8;
then a - n >= (n + ((a div n) * n)) - n by XREAL_1:11;
then (a - n) * (n " ) >= ((a div n) * n) * (n " ) by XREAL_1:66;
then (a - n) * (n " ) >= (a div n) * (n * (n " )) ;
then (a * (n " )) - (n * (n " )) >= (a div n) * 1 by A1, XCMPLX_0:def 7;
then (a * (n " )) - 1 >= a div n by A1, XCMPLX_0:def 7;
then A2: (a / n) - 1 >= a div n by XCMPLX_0:def 9;
a div n = [\(a / n)/] by INT_1:def 7;
hence contradiction by A2, INT_1:def 4; :: thesis: verum

end;

hence ( a mod n >= 0 & a mod n < n ) ; :: thesis: verum