Commit 2023-11-09 00:36 1dfce854

chore: Merge back ordered cancellative stuff (#8170) There really is no reason (mathematically nor import graphically) to have OrderedCancelCommMonoid be defined in a separate file from OrderedCommMonoid. Also take the opportunity to:

• make OrderedCancelCommMonoid extend OrderedCommMonoid
• fix capitalisation in instance names
• standardise to defining the additive of each structure version first, so that to_additive can be called directly on the multiplicative version
• inline at no cost a few auxiliary lemmas