let n be Nat; :: thesis: ( 3 <= n implies tau to_power (n - 2) < Fib n )
defpred S1[ Nat] means tau to_power ($1 - 2) < Fib $1;
A1: for k being Nat st k >= 3 & ( for i being Nat st i >= 3 & i < k holds
S1[i] ) holds
S1[k]
proof
let k be Nat; :: thesis: ( k >= 3 & ( for i being Nat st i >= 3 & i < k holds
S1[i] ) implies S1[k] )
assume A2: k >= 3 ; :: thesis: ( ex i being Nat st
( i >= 3 & i < k & not S1[i] ) or S1[k] )
assume A3: for i being Nat st i >= 3 & i < k holds
S1[i] ; :: thesis: S1[k]
LL: ( ( 3 <= k & k <= 3 + 1 ) or 4 < k ) by A2;
now :: thesis: ( ( k = 3 & S1[3] ) or ( k = 4 & S1[4] ) or ( 4 < k & S1[k] ) )
per cases ( k = 3 or k = 4 or 4 < k ) by LL, NAT_1:9;
case LC4A: 4 < k ; :: thesis: S1[k]
then k - 4 in NAT by INT_1:5;
then reconsider z = k - 4 as Nat ;
4 - 3 < k - 0 by XREAL_1:14, LC4A;
then k - 1 in NAT by INT_1:5;
then reconsider x = k - 1 as Nat ;
4 - 2 < k - 0 by XREAL_1:14, LC4A;
then k - 2 in NAT by INT_1:5;
then reconsider y = k - 2 as Nat ;
4 + 1 <= k by INT_1:7, LC4A;
then ( 5 - 2 <= k - 2 & 5 - 2 <= k - 1 ) by XREAL_1:13;
then ( 3 <= x & 3 <= y & x < k & y < k ) by XREAL_1:44;
then ( tau to_power (x - 2) < Fib x & tau to_power (y - 2) < Fib y ) by A3;
then (tau to_power z) + (tau to_power (z + 1)) < (Fib x) + (Fib y) by XREAL_1:8;
then tau to_power (z + 2) < (Fib x) + (Fib y) by FIB_NUM3:9;
then tau to_power (k - 2) < Fib ((y + 1) + 1) by PRE_FF:1;
hence S1[k] ; :: thesis: verum
end;
end;
end;
hence S1[k] ; :: thesis: verum
end;
for k being Nat st k >= 3 holds
S1[k] from NAT_1:sch 9(A1);
 hence ( 3 <= n implies tau to_power (n - 2) < Fib n ) ; :: thesis: verum