chore: Move `CovariantClass` lemmas

[YaelDillies]

trafficstars

The files containing lemmas about the interaction of order in terms of CovariantClass/ContravariantClass and not the bundled compatibility typeclasses were all over the place. This PR puts them all in Algebra.Order.NameOfAlgebraicStructure.Unbundled.

---

In particular this addresses @semorrison's long time concern that Algebra.Order.Ring.Lemmas is more basic than Algebra.Order.Ring.Defs.

[github-actions[bot]]

No declarations were harmed in the making of this PR! 🐙

---

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[jcommelin]

Thanks :tada:

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style