k to_power (n + 1) = (k to_power n) * (k to_power 1) by POWER:27
.= k * (k to_power n) ;
then (k to_power (n + 1)) - (k to_power n) = (k - 1) * (k to_power n) ;
hence (k to_power (n + 1)) - (k to_power n) is positive ; :: thesis: verum