chore(algebra/order/monoid): split into smaller files (#16861)

This, along later PRs for `algebra.order.group` and `algebra.order.ring`, will replace #16792.

- [x] depends on: #16172

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)


Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

counterexamples/canonically_ordered_comm_semiring_two_mul.lean

@@ -5,7 +5,7 @@ Authors: Damiano Testa
 -/
 import data.zmod.basic
 import ring_theory.subsemiring.basic
-import algebra.order.monoid
+import algebra.order.monoid.basic
 /-!
 
 A `canonically_ordered_comm_semiring` with two different elements `a` and `b` such that

counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean

@@ -4,7 +4,7 @@ All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Damiano Testa, Kevin Buzzard
 -/
-import algebra.order.monoid
+import algebra.order.monoid.basic
 
 /-!
 An example of a `linear_ordered_comm_monoid_with_zero` in which the product of two positive

src/algebra/order/group.lean

@@ -5,6 +5,10 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
 import algebra.abs
 import algebra.order.sub
+import algebra.order.monoid.min_max
+import algebra.order.monoid.prod
+import algebra.order.monoid.type_tags
+import algebra.order.monoid.units
 
 /-!
 # Ordered groups