theorem :: XCMPLX_1:187

for a, b being Complex holds - (a / b) = (- a) / b by Lm17;