for k being Nat holds 2 * k <= 2 to_power k