for m, n being non zero Nat st m >= n holds
Lucas m >= Lucas n