feat(algebra/order/monoid): Co/contravariant classes for with_bot/with_top (#13369)

Add the `covariant_class (with_bot α) (with_bot α) (+) (≤)` and `contravariant_class (with_bot α) (with_bot α) (+) (<)` instances, as well as the lemmas that `covariant_class (with_bot α) (with_bot α) (+) (<)` and `contravariant_class (with_bot α) (with_bot α) (+) (≤)` almost hold.

On the way, match the APIs for `with_bot`/`with_top` by adding missing lemmas.

Co-authored-by: Wrenna Robson <wren.robson@gmail.com>

Author: YaelDillies