r * (r " ) = r / r by XCMPLX_0:def 9;
hence not r * (r " ) is negative ; :: thesis: verum