Commit 2022-04-21 15:19 e8b581a7

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.