mathlib

dd600354 - chore(algebra/{covariant_and_contravariant + ordered_monoid_lemmas}): new file covariant_and_contravariant (#7890)

chore(algebra/{covariant_and_contravariant + ordered_monoid_lemmas}): new file covariant_and_contravariant (#7890) This PR creates a new file `algebra/covariant_and_contravariant` and moves the part of `algebra/ordered_monoid_lemmas` dealing exclusively with `covariant` and `contravariant` into it. It also rearranges the documentation, with a view to the later PRs, building up to #7645. The discrepancy between the added and removed lines is entirely due to longer documentation: no actual Lean code has changed, except, of course, for the `import` in `algebra/ordered_monoid_lemmas` that now uses `covariant_and_contravariant`.