theorem :: NEWTON01:11

for a, b, m being Nat holds (a |^ (m + 1)) + (b |^ (m + 1)) >= (((a |^ m) + (b |^ m)) * (a + b)) / 2