let a, b be Real; :: thesis: ( a <> b implies 1 - (a / (a - b)) = - (b / (a - b)) )
assume a <> b ; :: thesis: 1 - (a / (a - b)) = - (b / (a - b))
then a - b <> 0 ;
then 1 - (a / (a - b)) = ((a - b) / (a - b)) - (a / (a - b)) by XCMPLX_1:60
.= ((a - b) - a) / (a - b) ;
hence 1 - (a / (a - b)) = - (b / (a - b)) ; :: thesis: verum