let a, b, n be Nat; :: thesis: ( a > b & a + b >= 2 |^ (n + 1) implies a > 2 |^ n )
assume A1: ( a > b & a + b >= 2 |^ (n + 1) ) ; :: thesis: a > 2 |^ n
then a + a > a + b by XREAL_1:6;
then 2 * a > 2 |^ (n + 1) by A1, XXREAL_0:2;
then 2 * a > 2 * (2 |^ n) by NEWTON:6;
hence a > 2 |^ n by XREAL_1:66; :: thesis: verum