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