theorem NN1: :: COMPLEX3:20

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