for a, b being positive Real holds ((a / b) + (b / a)) / 2 >= 1