mathlib

e8b581a7 - feat(order/countable_dense_linear_order): Relax conditions of `embedding_from_countable_to_dense` (#12928)

feat(order/countable_dense_linear_order): Relax conditions of `embedding_from_countable_to_dense` (#12928) We prove that any countable order embeds in any nontrivial dense order. We also slightly golf the rest of the file.