Commit 2021-06-15 06:03 bf83c301

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.