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 A3: j > 0 ; :: thesis: ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j )

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

end;

suppose A4: 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:48, INT_1:def 10;
hence ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j ) by A4, INT_1:48, INT_1:def 10; :: thesis: verum

end;

end;