theorem :: COMPLEX3:68

for k being positive Real
for n being positive light Real holds (k + 1) to_power n < (k to_power n) + 1