for a, b, n being Nat st n > 0 & a <> b holds
(2 * (a |^ n)) * (b |^ n) < (a |^ (2 * n)) + (b |^ (2 * n))