(k + 1) to_power n > (k to_power n) + (1 to_power n) by APB;
then ((k + 1) to_power n) - (k to_power n) > ((k to_power n) + 1) - (k to_power n) by XREAL_1:9;
hence ( ((k + 1) to_power n) - (k to_power n) is heavy & ((k + 1) to_power n) - (k to_power n) is positive ) by TA1; :: thesis: verum