mathlib

af8a38fd - feat(algebra/{covariant_and_contravariant + ordered_monoid): add instance, golf, docs (#8067)

feat(algebra/{covariant_and_contravariant + ordered_monoid): add instance, golf, docs (#8067) Introduce a missing instance for `comm_semigroup`s. Also, golf a couple of proofs and add a relevant, explicit PR to a comment.