let n be natural number ; :: thesis: ( n > 2 implies tau_bar to_power n >= - (1 / (sqrt 5)) )
assume n > 2 ; :: thesis: tau_bar to_power n >= - (1 / (sqrt 5))
then n >= 2 + 1 by NAT_1:13;
then b2: tau_bar to_power n >= tau_bar to_power 3 by hopp9, POLYFORM:6;
B3: sqrt 5 > 0 by SQUARE_1:93;
sqrt 5 >= 2 by SQUARE_1:85, SQUARE_1:94;
then 2 * (sqrt 5) >= 2 * 2 by XREAL_1:66;
then (2 * (sqrt 5)) - 5 >= 4 - 5 by XREAL_1:11;
then (2 * (sqrt 5)) - ((sqrt 5) ^2 ) >= - 1 by SQUARE_1:def 4;
then ((2 - (sqrt 5)) * (sqrt 5)) / (sqrt 5) >= (- 1) / (sqrt 5) by B3, XREAL_1:74;
then ((2 - (sqrt 5)) * (sqrt 5)) / (sqrt 5) >= - (1 / (sqrt 5)) by XCMPLX_1:188;
then 2 - (sqrt 5) >= - (1 / (sqrt 5)) by B3, XCMPLX_1:90;
hence tau_bar to_power n >= - (1 / (sqrt 5)) by b2, beta3, XXREAL_0:2; :: thesis: verum