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