Countable strict weak orders embed in the rationals

[UPSTREAM] candidate for Mathlib/Order/CountableDenseLinearOrder.lean. A countable strict weak order is the pullback of < on ℚ along some map. Its quotient by incomparability is a countable linear order, which embeds in ℚ by Cantor's theorem Order.embedding_from_countable_to_dense.

theorem Order.exists_rat_rel_iff_lt {β : Type u_1} [Countable β] (r : β → β → Prop) [IsStrictWeakOrder β r] : ∃ (f : β → ℚ), ∀ (x y : β), r x y ↔ f x < f y

A countable strict weak order is the pullback of < on ℚ along some map.