for a being Real
for n being Nat st - 1 < a holds
(1 + a) to_power n >= 1 + (n * a) by PREPOWER:16;