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