let i, j be Integer; :: thesis: ( i >= 0 & j >= 0 implies ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j ) )
assume that
A1: i >= 0 and
A2: j >= 0 ; :: thesis: ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j )

per cases ( j > 0 or j = 0 ) by A2, XXREAL_0:1;

suppose j > 0 ; :: thesis: ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j )

then ( i = abs i & j = abs j ) by A1, ABSVALUE:def 1;
hence ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j ) ; :: thesis: verum

end;

suppose A5: j = 0 ; :: thesis: ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j )

abs 0 = 0 by ABSVALUE:def 1;
then ( (abs i) mod (abs 0 ) = 0 & (abs i) div (abs 0 ) = 0 ) by INT_1:75, INT_1:def 8;
hence ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j ) by A5, INT_1:75, INT_1:def 8; :: thesis: verum

end;

end;