theorem :: NEWTON04:86

for a, b being non negative Real
for n being non zero Nat holds (a * ((a + b) |^ n)) + ((a + b) * (b |^ n)) <= (a + b) |^ (n + 1)