theorem LC5aa: :: ASYMPT_2:8

for n being Nat
for a being Real st 1 < a holds
a to_power n < a to_power (n + 1)