sqrt 5 > 1 by SQUARE_1:83, SQUARE_1:95;
then - (sqrt 5) < - 1 by XREAL_1:26;
then a1: (- (sqrt 5)) + 1 < (- 1) + 1 by XREAL_1:8;
tau_bar / tau = ((1 - (sqrt 5)) * 2) / ((1 + (sqrt 5)) * 2) by FIB_NUM:def 1, FIB_NUM:def 2, XCMPLX_1:85
.= (1 - (sqrt 5)) / (1 + (sqrt 5)) by XCMPLX_1:92
.= ((1 - (sqrt 5)) * (1 - (sqrt 5))) / ((1 + (sqrt 5)) * (1 - (sqrt 5))) by a1, XCMPLX_1:92
.= ((1 - (2 * (sqrt 5))) + ((sqrt 5) ^2)) / ((1 ^2) - ((sqrt 5) ^2))
.= ((1 - (2 * (sqrt 5))) + 5) / ((1 ^2) - ((sqrt 5) ^2)) by SQUARE_1:def 4
.= (6 - (2 * (sqrt 5))) / ((1 ^2) - 5) by SQUARE_1:def 4
.= (2 * (3 - (sqrt 5))) / ((- 2) * 2) ;
hence tau_bar / tau = ((sqrt 5) - 3) / 2 ; :: thesis: verum