theorem :: XCMPLX_1:219

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