let n be Nat; :: 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:25;
sqrt 5 >= 2 by SQUARE_1:20, SQUARE_1:26;
then 2 * (sqrt 5) >= 2 * 2 by XREAL_1:64;
then (2 * (sqrt 5)) - 5 >= 4 - 5 by XREAL_1:9;
then (2 * (sqrt 5)) - ((sqrt 5) ^2) >= - 1 by SQUARE_1:def 2;
then ((2 - (sqrt 5)) * (sqrt 5)) / (sqrt 5) >= (- 1) / (sqrt 5) by A2, XREAL_1:72;
then ((2 - (sqrt 5)) * (sqrt 5)) / (sqrt 5) >= - (1 / (sqrt 5)) by XCMPLX_1:187;
then 2 - (sqrt 5) >= - (1 / (sqrt 5)) by A2, XCMPLX_1:89;
hence tau_bar to_power n >= - (1 / (sqrt 5)) by A1, Lm8, XXREAL_0:2; :: thesis: verum