for a, b being positive Real
for n being Nat holds ((a |^ n) + (b |^ n)) / 2 >= ((a + b) / 2) |^ n