theorem :: FIB_NUM4:39

for n, k being Nat st n >= 4 & k >= 1 & n > k & n is odd holds
Lucas (n + k) = [\(((tau to_power k) * (Lucas n)) + 1)/]