theorem :: NAT_2:13

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