let k, n be Nat; :: thesis: ( k <= n implies 2 to_power k divides 2 to_power n )
assume k <= n ; :: thesis: 2 to_power k divides 2 to_power n
then 2 to_power n = (2 to_power k) * (2 to_power (n -' k)) by Th10;
hence 2 to_power k divides 2 to_power n by NAT_D:def 3; :: thesis: verum