theorem Th17: :: FIB_NUM3:17

for k being Nat holds Lucas k >= k