Commit 2025-03-17 17:38 d98a17da

feat: shortlex order on lists (#20310) Given a relation r on a type α, the shortlex order over r on lists (first compare by length; if equal, then compare by lexicographic order over r) is defined. We prove that this inherits properties from the underlying relation r such as trichotomous-icity, asymmetry, order-connectedness. Most importantly, Shortlex r is well-founded if r is well-founded, giving a well-founded order on lists. (Notably, List.Lex is not well-founded).