theorem :: XCMPLX_1:175

for a, b being Complex holds (- a) * b = a * (- b) ;