A1: sqrt 5 > 0 by SQUARE_1:25;
tau / tau_bar = ((1 + (sqrt 5)) * 2) / ((1 - (sqrt 5)) * 2) by FIB_NUM:def 1, FIB_NUM:def 2, XCMPLX_1:84
.= (1 + (sqrt 5)) / (1 - (sqrt 5)) by XCMPLX_1:91
.= ((1 + (sqrt 5)) * (1 + (sqrt 5))) / ((1 - (sqrt 5)) * (1 + (sqrt 5))) by A1, XCMPLX_1:91
.= ((1 + (sqrt 5)) * (1 + (sqrt 5))) / (1 - ((sqrt 5) ^2))
.= ((1 + (sqrt 5)) * (1 + (sqrt 5))) / (1 - 5) by SQUARE_1:def 2
.= ((1 + (2 * (sqrt 5))) + ((sqrt 5) ^2)) / (- 4)
.= ((1 + (2 * (sqrt 5))) + 5) / (- 4) by SQUARE_1:def 2 ;
hence tau / tau_bar = ((- 3) - (sqrt 5)) / 2 ; :: thesis: verum