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) * (a - b) <> 0 ;
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