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