theorem Th24: :: NAT_2:24

for k, m, n being Nat st n <= m holds
n div k <= m div k