let n be Nat; :: thesis: ( n >= 1 implies (2 to_power (n + 1)) - (2 to_power n) > 1 )
assume n >= 1 ; :: thesis: (2 to_power (n + 1)) - (2 to_power n) > 1
then 2 to_power n >= 2 to_power 1 by PRE_FF:8;
then (2 to_power n) * 1 >= 2 by POWER:25;
then ((2 to_power n) * 2) - ((2 to_power n) * 1) > 1 by XXREAL_0:2;
then ((2 to_power n) * (2 to_power 1)) - (2 to_power n) > 1 by POWER:25;
hence (2 to_power (n + 1)) - (2 to_power n) > 1 by POWER:27; :: thesis: verum