theorem LMC31E: :: ASYMPT_2:5

for k, n being Nat st k <= n holds
n + k <= 2 to_power n