theorem :: XCMPLX_1:80

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