for a being non trivial natural number
for n, m being natural number st n > m holds
a |^ n > a |^ m