let k, l, m be Nat; :: thesis: ( 0 < k & k < l & l < m & ( not k = 2 or not l = 3 or not m = 4 ) & ( not k = 1 or not l = 4 or not m = 5 ) & (Fib m) - (Fib l) = (Fib l) - (Fib k) & (Fib l) - (Fib k) > 0 implies ( l > 2 & k = l - 2 & m = l + 1 ) )
set uk = Fib k;
set ul = Fib l;
set um = Fib m;
assume A1: ( 0 < k & k < l & l < m & ( not k = 2 or not l = 3 or not m = 4 ) & ( not k = 1 or not l = 4 or not m = 5 ) & (Fib m) - (Fib l) = (Fib l) - (Fib k) & (Fib l) - (Fib k) > 0 ) ; :: thesis: ( l > 2 & k = l - 2 & m = l + 1 )
then k >= 1 + 0 by NAT_1:13;
then II: l > 1 by A1, XXREAL_0:2;
sO: Fib l > 1

proof

assume Fib l <= 1 ; :: thesis: contradiction
then Fib l < 1 + 1 by NAT_1:13;
then Ia: ( Fib l = 0 or Fib l = 1 ) by NAT_1:23;
((Fib l) - (Fib k)) + (Fib k) > 0 + (Fib k) by A1, XREAL_1:8;
then Fib k = 0 by Ia, NAT_1:14;
hence contradiction by A1, LemmaFib0; :: thesis: verum

end;

then SO: l > 2 by FibGe2;
then l >= 2 + 1 by NAT_1:13;
then Y1: m > 3 by A1, XXREAL_0:2;
h1: Fib l < Fib (l + 1) by II, FIB_NUM2:44;
Fib m = ((Fib l) + (Fib l)) - (Fib k) by A1;
then H1: Fib m < (Fib l) + (Fib l) by XREAL_1:44, A1, LemmaFib0;
(Fib l) + (Fib l) < (Fib l) + (Fib (l + 1)) by h1, XREAL_1:8;
then (Fib l) + (Fib l) < Fib ((l + 1) + 1) by PRE_FF:1;
then XX: Fib m < Fib ((l + 1) + 1) by H1, XXREAL_0:2;
l + 1 <= m by A1, NAT_1:13;
then S2: Fib m >= Fib (l + 1) by FIB_NUM2:45;
JK: m in NAT by ORDINAL1:def 12;
m > 1 by Y1, XXREAL_0:2;
then dd: Fib m <= Fib (l + 1) by XX, FiboLeq;
then dx: Fib m = Fib (l + 1) by S2, XXREAL_0:1;
reconsider l1 = l - 1 as Nat by A1;
reconsider l2 = l - 2 as Element of NAT by SO, INT_1:5;

per cases ( k = 1 or k <> 1 ) ;

suppose D1: k = 1 ; :: thesis: ( l > 2 & k = l - 2 & m = l + 1 )

K1: (Fib l2) + (Fib (l2 + 1)) = Fib ((l2 + 1) + 1) by PRE_FF:1;
x2: Fib ((l1 + 1) + 1) = (Fib (l1 + 1)) + (Fib l1) by PRE_FF:1;
(2 * (Fib l)) - (Fib m) = (Fib l) - ((Fib (l + 1)) - (Fib l)) by dx;
then ( l2 = 1 or l2 = 2 ) by FIB_NUM2:47, D1, PRE_FF:1, K1, A1, x2;

per cases then ( l = 3 or l = 4 ) ;

suppose l = 3 ; :: thesis: ( l > 2 & k = l - 2 & m = l + 1 )

hence ( l > 2 & k = l - 2 & m = l + 1 ) by dx, A1, JK, FIB_NUM2:48, D1; :: thesis: verum

end;

suppose l = 4 ; :: thesis: ( l > 2 & k = l - 2 & m = l + 1 )

hence ( l > 2 & k = l - 2 & m = l + 1 ) by A1, D1, dx, JK, FIB_NUM2:48; :: thesis: verum

end;

end;

end;

suppose JA: k <> 1 ; :: thesis: ( l > 2 & k = l - 2 & m = l + 1 )

per cases ( l2 = 1 or l2 <> 1 ) ;

suppose Ss: l2 = 1 ; :: thesis: ( l > 2 & k = l - 2 & m = l + 1 )

then 3 - (Fib 3) = (Fib 3) - (Fib k) by FIB_NUM2:23, dd, A1, S2, XXREAL_0:1;
hence ( l > 2 & k = l - 2 & m = l + 1 ) by dx, A1, Ss, FIB_NUM2:47, FIB_NUM2:48, FIB_NUM2:22, II, JK; :: thesis: verum

end;

suppose ja: l2 <> 1 ; :: thesis: ( l > 2 & k = l - 2 & m = l + 1 )

K1: (Fib l2) + (Fib (l2 + 1)) = Fib ((l2 + 1) + 1) by PRE_FF:1;
X2: Fib ((l1 + 1) + 1) = (Fib (l1 + 1)) + (Fib l1) by PRE_FF:1;
l <> 0 by sO, FibGe2;
then LL: ( m > 1 & l + 1 <> 1 ) by Y1, XXREAL_0:2;
(2 * (Fib l)) - (Fib m) = (Fib l) - ((Fib (l + 1)) - (Fib l)) by dx;
hence ( l > 2 & k = l - 2 & m = l + 1 ) by sO, LL, JA, ja, Th48, K1, A1, X2, FibGe2; :: thesis: verum

end;

end;

end;

end;