Library Coq.FSets.OrderedTypeEx
Examples of Ordered Type structures.
First, a particular case of OrderedType where
the equality is the usual one of Coq.
a UsualOrderedType is in particular an OrderedType.
nat is an ordered type with respect to the usual order on natural numbers.
Z is an ordered type with respect to the usual order on integers.
positive is an ordered type with respect to the usual order on natural numbers.
N is an ordered type with respect to the usual order on natural numbers.
From two ordered types, we can build a new OrderedType
over their cartesian product, using the lexicographic order.