theorem Th12: :: FIB_NUM4:12

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