mathlib
cdd1703c - feat(algebra/associates): add two instances and a lemma about the order on the monoid of associates of a monoid (#12863)
