Locally finite linear orders embed in the integers

[UPSTREAM] candidate for Mathlib/Order/SuccPred/LinearLocallyFinite.lean. A locally finite linear order embeds in ℤ by numbering its elements from a base point, toZ, once it is given the successor and predecessor structure of a locally finite order.

theorem nonempty_orderEmbedding_int (ι : Type u_1) [LinearOrder ι] [LocallyFiniteOrder ι] : Nonempty (ι ↪o ℤ)

A locally finite linear order embeds in ℤ.