let n be Nat; :: thesis: ( n >= 2 implies tau_bar to_power n <= 1 / (sqrt 5) )
assume A1: n >= 2 ; :: thesis: tau_bar to_power n <= 1 / (sqrt 5)

per cases ( n is even or n is odd ) ;

suppose A2: n is even ; :: thesis: tau_bar to_power n <= 1 / (sqrt 5)

A3: sqrt 5 > 0 by SQUARE_1:25;
A4: tau_bar to_power n <= (3 - (sqrt 5)) / 2 by Lm7, A1, A2, Th11, POLYFORM:5;
sqrt 5 <= sqrt ((7 / 3) ^2) by SQUARE_1:26;
then sqrt 5 <= 7 / 3 by SQUARE_1:def 2;
then 3 * (sqrt 5) <= (7 / 3) * 3 by XREAL_1:64;
then (3 * (sqrt 5)) - 5 <= 7 - 5 by XREAL_1:9;
then (3 * (sqrt 5)) - ((sqrt 5) ^2) <= 2 by SQUARE_1:def 2;
then ((3 * (sqrt 5)) - ((sqrt 5) * (sqrt 5))) / 2 <= 2 / 2 by XREAL_1:72;
then (((3 - (sqrt 5)) / 2) * (sqrt 5)) / (sqrt 5) <= 1 / (sqrt 5) by A3, XREAL_1:72;
then (3 - (sqrt 5)) / 2 <= 1 / (sqrt 5) by A3, XCMPLX_1:89;
hence tau_bar to_power n <= 1 / (sqrt 5) by A4, XXREAL_0:2; :: thesis: verum

end;

suppose n is odd ; :: thesis: tau_bar to_power n <= 1 / (sqrt 5)

then A5: tau_bar to_power n < 0 by Th7;
sqrt 5 >= sqrt 0 by SQUARE_1:26;
hence tau_bar to_power n <= 1 / (sqrt 5) by A5; :: thesis: verum

end;

end;