let m, n be Nat; :: thesis: ( m < n & m > 4 implies (Fib n) - (Fib m) > 2 )
assume A1: ( m < n & m > 4 ) ; :: thesis: (Fib n) - (Fib m) > 2
then m + 1 <= n by NAT_1:13;
then A3: (Fib (m + 1)) - (Fib m) <= (Fib n) - (Fib m) by XREAL_1:9, FIB_NUM2:45;
reconsider m1 = m - 1 as Element of NAT by INT_1:5, A1, XXREAL_0:2;
A2: Fib ((m1 + 1) + 1) = (Fib (m1 + 1)) + (Fib m1) by PRE_FF:1;
m - 1 > 4 - 1 by A1, XREAL_1:14;
then Fib m1 >= 3 by FibGe3;
then (Fib n) - (Fib m) >= 3 by A3, XXREAL_0:2, A2;
hence (Fib n) - (Fib m) > 2 by XXREAL_0:2; :: thesis: verum