mathlib3

bf83c301 - chore(algebra/{ordered_monoid_lemmas, ordered_monoid}): move two sections close together (#7921)

chore(algebra/{ordered_monoid_lemmas, ordered_monoid}): move two sections close together (#7921) This PR aims at shortening the diff between `master` and PR #7645 of the order refactor. I moved the `mono` section of `algebra/ordered_monoid_lemmas` to the end of the file and appended the `strict_mono` section of `algebra/ordered_monoid` after that. Note: the hypotheses are not optimal, but, with the current `instances` in this version, I did not know how to improve this. It will get better by the time PR #7645 is merged. In fact, the next PR in the sequence, #7876, already removes the unnecessary assumptions.