tau * tau_bar = ((1 ^2) - ((sqrt 5) ^2)) / 4 by FIB_NUM:def 1, FIB_NUM:def 2
.= (1 - 5) / 4 by SQUARE_1:def 2 ;
hence tau * tau_bar = - 1 ; :: thesis: verum