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 A1: tau_bar to_power n >= tau_bar to_power 3 by Th10, POLYFORM:6;
A2: 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 A2, 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 A2, XCMPLX_1:90;
hence tau_bar to_power n >= - (1 / (sqrt 5)) by A1, Lm8, XXREAL_0:2; :: thesis: verum