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