for n being Nat st n >= 1 holds
(2 to_power (n + 1)) - (2 to_power n) > 1 by Lm48;