theorem :: INT_1:55

for m, n being Nat holds 0 <= m div n by Th52;