Library Coq.Numbers.Integer.Binary.ZBinary


Require Import ZAxioms ZProperties BinInt.

Local Open Scope Z_scope.

BinInt.Z is already implementing ZAxiomsMiniSig

Module Z
 <: ZAxiomsSig <: UsualOrderedTypeFull <: TotalOrder
 <: UsualDecidableTypeFull
 := BinInt.Z.

An order tactic for integers


Ltac z_order := Z.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.

Section TestOrder.
 Let test : forall x y, x<=y -> y<=x -> x=y.
End TestOrder.

Z forms a ring