for a, b, c, d being positive Real holds
( not a * b >= c * d or a + b > c + d or (1 / a) + (1 / b) <= (1 / c) + (1 / d) ) by SRI;