let i, j be Integer; :: thesis: ( i mod j = 0 implies i div j = i / j )
assume A2: i mod j = 0 ; :: thesis: i div j = i / j

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

suppose A1: j <> 0 ; :: thesis: i div j = i / j

i = ((i div j) * j) + (i mod j) by A1, INT_1:59
.= (i div j) * j by A2 ;
hence i div j = i / j by A1, XCMPLX_1:89; :: thesis: verum

end;

suppose j = 0 ; :: thesis: i div j = i / j

hence i div j = i / j by XCMPLX_1:49; :: thesis: verum

end;

end;