let a, n be positive heavy Real; :: thesis: ((a + 1) to_power n) - ((a - 1) to_power n) > 2 to_power n
a + 1 = (a - 1) + 2 ;
then ((a + 1) to_power n) - ((a - 1) to_power n) > (((a - 1) to_power n) + (2 to_power n)) - ((a - 1) to_power n) by APB, XREAL_1:9;
hence ((a + 1) to_power n) - ((a - 1) to_power n) > 2 to_power n ; :: thesis: verum