let a, b be complex number ; :: thesis: - (a / b) = (- a) / b
thus - (a / b) = - (a * (b " )) by XCMPLX_0:def 9
.= (- a) * (b " )
.= (- a) / b by XCMPLX_0:def 9 ; :: thesis: verum