mathlib

522ace49 - feat(order/antisymmetrization): (<) is well-founded for a preorder iff well-founded on its antisymmetrization (#16741)

feat(order/antisymmetrization): (<) is well-founded for a preorder iff well-founded on its antisymmetrization (#16741) + Show that the antisymmetrization of a well-founded preorder is a well-founded partial order. Useful for reducing well-foundedness of preorders to partial orders. + fix reference to renamed lemma `well_founded.prod_game_add` in docstring.