let a, b be Complex; :: thesis: (- a) / b = a / (- b)
thus (- a) / b = - (a / b) by Lm17
.= a / (- b) by Th188 ; :: thesis: verum