for a, b, c, m being Nat st a is odd & b is odd & m is even holds
(a |^ m) + (b |^ m) <> c |^ m