theorem :: COMPLEX3:83
for a being positive heavy Real holds (1 / (a + 1)) + (1 / (a - 1)) > 2 / a