let i, j be natural Number ; :: thesis: ( i < j implies i div j = 0 )
assume A1: i < j ; :: thesis: i div j = 0

per cases ( ex j1 being Nat st
( i = (j * (i div j)) + j1 & j1 < j ) or ( i div j = 0 & j = 0 ) ) by Def1;

suppose ex j1 being Nat st
( i = (j * (i div j)) + j1 & j1 < j ) ; :: thesis: i div j = 0

then consider j1 being Nat such that
A2: i = (j * (i div j)) + j1 and
j1 < j ;
assume i div j <> 0 ; :: thesis: contradiction
then consider k being Nat such that
A3: i div j = k + 1 by NAT_1:6;
i = j + ((j * k) + j1) by A2, A3;
hence contradiction by A1, NAT_1:11; :: thesis: verum

end;

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

hence i div j = 0 ; :: thesis: verum

end;

end;