let m, n be Nat; :: thesis: ( m < n & m > 3 implies (Fib n) - (Fib m) > 1 )
assume A1: ( m < n & m > 3 ) ; :: thesis: (Fib n) - (Fib m) > 1
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 > 3 - 1 by A1, XREAL_1:14;
then Fib m1 >= 2 by FibGe2a;
then (Fib n) - (Fib m) >= 2 by A3, a2, XXREAL_0:2;
hence (Fib n) - (Fib m) > 1 by XXREAL_0:2; :: thesis: verum