Library Coq.Structures.OrderedTypeAlt
An alternative (but equivalent) presentation for an Ordered Type
inferface.
NB: comparison, defined in Datatypes.v is Eq|Lt|Gt
whereas compare, defined in OrderedType.v is EQ _ | LT _ | GT _
From this new presentation to the original one.
From the original presentation to this alternative one.