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