theorem :: NEWTON04:85
for a, b being non negative Real
for n being non zero Nat holds (a * ((a + (2 * b)) |^ n)) + (b |^ (n + 1)) >= (a + b) |^ (n + 1)