let a, b be complex number ; :: thesis: (- a) / b = a / (- b)
thus (- a) / b = - (a / b) by Lm17
.= a / (- b) by Th189 ; :: thesis: verum