theorem NP1: :: COMPLEX3:21

for a being negative Real
for b being positive Real holds ((a / b) + (b / a)) / 2 <= - 1