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