theorem :: FIB_NUM4:29

for n, k being Nat st ( ( n >= k & k > 1 ) or ( k = 1 & n > k ) ) holds
[\(((tau to_power k) * (Fib n)) + (1 / 2))/] = Fib (n + k)