theorem :: NEWTON01:29

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