let i, j be natural number ; :: thesis: ( j > 0 & i mod j = 0 implies i div j = i / j )
assume A1: j > 0 ; :: thesis: ( not i mod j = 0 or i div j = i / j )
assume i mod j = 0 ; :: thesis: i div j = i / j
then consider t being Nat such that
A2: i = (j * t) + 0 and
A3: 0 < j by A1, NAT_D:def 2;
thus i div j = t by A2, A3, NAT_D:def 1
.= i / j by A1, A2, XCMPLX_1:89 ; :: thesis: verum