for a, b, m being Nat holds (a - b) * ((a |^ m) - (b |^ m)) >= 0