mathlib

d249e533 - feat(algebra/ordered_group): add instances mixing `group` and `co(ntra)variant` (#8072)

feat(algebra/ordered_group): add instances mixing `group` and `co(ntra)variant` (#8072) In an attempt to break off small parts of PR #8060, I extracted some of the instances proven there to this PR. This is part of the `order` refactor. ~~I tried to get rid of the `@`, but failed. If you have a trick to avoid them, I would be very happy to learn it!~~ `@`s removed!