mathlib

10216790 - feat(algebra/ordered_monoid): a few more `order_dual` instances (#8519)

feat(algebra/ordered_monoid): a few more `order_dual` instances (#8519) * add `covariant.flip` and `contravariant.flip`; * add `[to_additive]` to `group.covariant_iff_contravariant` and `covconv` (renamed to `group.covconv`); * use `group.covconv` in `group.covariant_class_le.to_contravariant_class_le`; * add some `order_dual` instances for `covariant_class` and `contravariant_class`; * golf `order_dual.ordered_comm_monoid`.