theorem Th12: :: NAT_2:12

for k, n being Nat st k > 0 & n div k = 0 holds
n < k