theorem :: XCMPLX_1:185

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