theorem SRL: :: COMPLEX3:46
for a, b, c, d being positive Real st a + b >= c + d & a * b < c * d holds
(1 / a) + (1 / b) > (1 / c) + (1 / d)