theorem :: NAT_2:16

for k, n being Nat st k <= n holds
(2 to_power n) div (2 to_power k) = 2 to_power (n -' k)