let a, b be Complex; :: 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:91
.= (a - b) / ((a ^2) - (b ^2)) ;
:: thesis: verum