let a, b be complex number ; :: thesis: ( (a ^2 ) - (b ^2 ) <> 0 implies 1 / (a + b) = (a - b) / ((a ^2 ) - (b ^2 )) )
assume (a ^2 ) - (b ^2 ) <> 0 ; :: thesis: 1 / (a + b) = (a - b) / ((a ^2 ) - (b ^2 ))
then a - b <> 0 ;
hence 1 / (a + b) = (1 * (a - b)) / ((a + b) * (a - b)) by XCMPLX_1:92
.= (a - b) / ((a ^2 ) - (b ^2 )) ;
:: thesis: verum