let i, j be Integer; :: thesis: ( i >= 0 & j >= 0 implies ( |.i.| mod |.j.| = i mod j & |.i.| div |.j.| = i div j ) )
assume ( i >= 0 & j >= 0 ) ; :: thesis: ( |.i.| mod |.j.| = i mod j & |.i.| div |.j.| = i div j )
then ( |.i.| = i & |.j.| = j ) by ABSVALUE:def 1;
hence ( |.i.| mod |.j.| = i mod j & |.i.| div |.j.| = i div j ) ; :: thesis: verum