theorem Th31: :: SERIES_3:31
for n being Nat
for a, b being non negative Real holds (a + b) |^ (n + 2) >= (a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b)