theorem :: XCMPLX_1:79

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