Commit 2022-01-03 20:30 62d814a4

refactor(order/lexicographic): Change the lex synonym (#10926) At least five types have a natural lexicographic order, namely:

• α ⊕ β where everything on the left is smaller than everything on the right
• Σ i, α i where things are first ordered following ι, then following α i
• Σ' i, α i where things are first ordered following ι, then following α i
• α × β where things are first ordered following α, then following β
• finset α, which is in a specific sene the dual of finset.colex. And we could even add Π i, α i, ι →₀ α, Π₀ i, α i, etc... although those haven't come up yet in practice. Hence, we generalize the lex synonym away from prod to make it a general purpose synonym to equip a type with its lexicographical order. What was lex α β now is α ×ₗ β. Note that this PR doesn't add any of the aforementioned instances.