Library Coq.Structures.OrdersEx
Examples of Ordered Type structures.
Ordered Type for
nat,
Positive,
N,
Z with the usual order.
An OrderedType can now directly be seen as a DecidableType
(Usual) Decidable Type for nat, positive, N, Z
From two ordered types, we can build a new OrderedType
over their cartesian product, using the lexicographic order.