sqrt 5 > 1 by SQUARE_1:18, SQUARE_1:27;
then - (sqrt 5) < - 1 by XREAL_1:24;
then A1: (- (sqrt 5)) + 1 < (- 1) + 1 by XREAL_1:6;
tau_bar / tau = ((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 - (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 2
.= (6 - (2 * (sqrt 5))) / ((1 ^2) - 5) by SQUARE_1:def 2
.= (2 * (3 - (sqrt 5))) / ((- 2) * 2) ;
hence tau_bar / tau = ((sqrt 5) - 3) / 2 ; :: thesis: verum