tau to_power 2 = ((1 + (sqrt 5)) / 2) ^2 by FIB_NUM:def 1, 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 to_power 2 = (3 + (sqrt 5)) / 2 ; :: thesis: verum