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