theorem LMC31D: :: ASYMPT_2:4

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