theorem Problem64Part1:
for
k,
l,
m being
Nat st
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 holds
(
l > 2 &
k = l - 2 &
m = l + 1 )