theorem :: XCMPLX_1:184

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