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