theorem :: NAT_2:11

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