theorem :: COMPLEX3:28

for a, b being negative Real holds
( 1 / a > 1 / b iff - a > - b ) by ABN, XREAL_1:24;