mathlib3

ca1375a5 - refactor(algebra/order/monoid_lemmas): reorder the file (#13492)

refactor(algebra/order/monoid_lemmas): reorder the file (#13492) Just like in `algebra/order/monoid_lemmas_zero_lt`, sort by algebraic assumptions and order assumptions first, then put similar lemmas together. It would be simpler to find duplicates, missing lemmas, and inconsistencies. (There are so many!)