theorem :: PRE_FF:16

for n being Nat st n <> 0 holds
n < 2 * n