let k, n be Nat; :: thesis: ( k <= n implies (2 to_power n) div (2 to_power k) = 2 to_power (n -' k) )
assume k <= n ; :: thesis: (2 to_power n) div (2 to_power k) = 2 to_power (n -' k)
then ( 2 to_power k > 0 & 2 to_power n = (2 to_power k) * (2 to_power (n -' k)) ) by Th10, POWER:34;
hence (2 to_power n) div (2 to_power k) = 2 to_power (n -' k) by NAT_D:18; :: thesis: verum