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 A2: 2 to_power n = (2 to_power k) * (2 to_power (n -' k)) by Th10;
reconsider a = 2 to_power (n -' k) as Nat by TARSKI:1;
take a ; :: according to NAT_D:def 3 :: thesis: 2 to_power n = (2 to_power k) * a
thus 2 to_power n = (2 to_power k) * a by A2; :: thesis: verum