Library Coq.NArith.POrderedType
DecidableType structure for positive numbers
Note that the last module fulfills by subtyping many other
interfaces, such as DecidableType or EqualityType.
OrderedType structure for positive numbers
Note that Positive_as_OT can also be seen as a UsualOrderedType
and a OrderedType (and also as a DecidableType).
An order tactic for positive numbers
Note that p_order is domain-agnostic: it will not prove
1<=2 or x<=x+x, but rather things like x<=y -> y<=x -> x=y.