theorem :: XCMPLX_1:97
for a, b, c being Complex st c <> 0 holds
a / b = c * ((a / c) / b)