theorem :: NEWTON03:97

for n being Nat
for a being non trivial Nat holds (a |^ (n + 1)) + (a |^ n) < a |^ (n + 2)