theorem :: NAT_2:25

for k, n being Nat st k <= 2 * n holds
(k + 1) div 2 <= n