theorem :: FIB_NUM3:18

for m being non zero Element of NAT holds Lucas (m + 1) >= Lucas m