let n be Nat; :: thesis: ( 3 <= n implies tau to_power (n - 2) < Fib n )
defpred S₁[ 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
S₁[i] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( k >= 3 & ( for i being Nat st i >= 3 & i < k holds
S₁[i] ) implies S₁[k] )
assume A2: k >= 3 ; :: thesis: ( ex i being Nat st
( i >= 3 & i < k & not S₁[i] ) or S₁[k] )
assume A3: for i being Nat st i >= 3 & i < k holds
S₁[i] ; :: thesis: S₁[k]
LL: ( ( 3 <= k & k <= 3 + 1 ) or 4 < k ) by A2;

now :: thesis: ( ( k = 3 & S₁[3] ) or ( k = 4 & S₁[4] ) or ( 4 < k & S₁[k] ) )

per cases ( k = 3 or k = 4 or 4 < k ) by LL, NAT_1:9;

case k = 3 ; :: thesis: S₁[3]

tau to_power 1 = tau ;
hence S₁[3] by FIB_NUM2:22, THTU2; :: thesis: verum

end;

case k = 4 ; :: thesis: S₁[4]

tau to_power (4 - 2) = tau to_power (0 + 2)
.= (tau to_power 0) + (tau to_power (0 + 1)) by FIB_NUM3:9
.= 1 + tau by POWER:24 ;
then tau to_power (4 - 2) < 1 + 2 by THTU2, XREAL_1:6;
hence S₁[4] by FIB_NUM2:23; :: thesis: verum

end;

case LC4A: 4 < k ; :: thesis: S₁[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 S₁[k] ; :: thesis: verum

end;

end;

end;

hence S₁[k] ; :: thesis: verum

end;

for k being Nat st k >= 3 holds
S₁[k] from NAT_1:sch 9(A1);
hence ( 3 <= n implies tau to_power (n - 2) < Fib n ) ; :: thesis: verum