theorem :: XCMPLX_1:131

for a, b being Complex st a <> 0 holds
a - b = a * (1 - (b / a))