# Library Coq.ZArith.ZOrderedType

Require Import BinInt Zcompare Zorder Zbool ZArith_dec
Equalities Orders OrdersTac.
Local Open Scope Z_scope.

# DecidableType structure for binary integers

Module Z_as_UBE <: UsualBoolEq.
Definition t := Z.
Definition eq := @eq Z.
Definition eqb := Zeq_bool.
Definition eqb_eq x y := iff_sym (Zeq_is_eq_bool x y).
End Z_as_UBE.
Module Z_as_DT <: UsualDecidableTypeFull := Make_UDTF Z_as_UBE.
Note that the last module fulfills by subtyping many other interfaces, such as DecidableType or EqualityType.

# OrderedType structure for binary integers

Module Z_as_OT <: OrderedTypeFull.
Include Z_as_DT.
Definition lt := Zlt.
Definition le := Zle.
Definition compare := Zcompare.
Instance lt_strorder : StrictOrder Zlt.
Instance lt_compat : Proper (Logic.eq ==> Logic.eq ==> iff) Zlt.
Definition le_lteq := Zle_lt_or_eq_iff.
Definition compare_spec := Zcompare_spec.
End Z_as_OT.
Note that Z_as_OT can also be seen as a UsualOrderedType and a OrderedType (and also as a DecidableType).

# An order tactic for integers

Module ZOrder := OTF_to_OrderTac Z_as_OT.
Ltac z_order := ZOrder.order.
Note that z_order is domain-agnostic: it will not prove 1<=2 or x<=x+x, but rather things like x<=y -> y<=x -> x=y.