for k being Nat holds Lucas k >= k