An ordered (additive) commutative monoid is a commutative monoid with a partial order such that addition is an order embedding, i.e. a + b ≤ a + c ↔ b ≤ c. These monoids are automatically cancellative.

A canonically ordered monoid is an ordered commutative monoid in which the ordering coincides with the divisibility relation, which is to say, a ≤ b iff there exists c with b = a + c. This is satisfied by the natural numbers, for example, but not the integers or other ordered groups.

The add_lt_add_left field of ordered_comm_group is redundant, but it is in core so we can't remove it for now. This alternative constructor is the best we can do.

This is not so much a new structure as a construction mechanism for ordered groups, by specifying only the "positive cone" of the group.