# Library Coq.ZArith.ZArith_dec

Require Import Sumbool.
Require Import BinInt.
Require Import Zorder.
Require Import Zcompare.
Local Open Scope Z_scope.
Lemma Zcompare_rect (P:Type) (n m:Z) :
(( n ?= m ) = Eq -> P) -> (( n ?= m ) = Lt -> P) -> (( n ?= m ) = Gt -> P) -> P.
Lemma Zcompare_rec (P:Set) (n m:Z) :
(( n ?= m ) = Eq -> P) -> (( n ?= m ) = Lt -> P) -> (( n ?= m ) = Gt -> P) -> P.
Notation Z_eq_dec := Z.eq_dec (compat "8.3").
Section decidability.
Variables x y : Z.

# Decidability of order on binary integers

Definition Z_lt_dec : { x < y } + { ~ x < y }.
Definition Z_le_dec : { x <= y } + { ~ x <= y }.
Definition Z_gt_dec : { x > y } + { ~ x > y }.
Definition Z_ge_dec : { x >= y } + { ~ x >= y }.
Definition Z_lt_ge_dec : { x < y } + { x >= y }.
Lemma Z_lt_le_dec : { x < y } + { y <= x }.
Definition Z_le_gt_dec : { x <= y } + { x > y }.
Definition Z_gt_le_dec : { x > y } + { x <= y }.
Definition Z_ge_lt_dec : { x >= y } + { x < y }.
Definition Z_le_lt_eq_dec : x <= y -> { x < y } + { x = y }.
End decidability.

# Cotransitivity of order on binary integers

Lemma Zlt_cotrans : forall n m:Z, n < m -> forall p:Z, { n < p } + { p < m }.
Lemma Zlt_cotrans_pos : forall n m:Z, 0 < n + m -> {0 < n } + {0 < m }.
Lemma Zlt_cotrans_neg : forall n m:Z, n + m < 0 -> { n < 0} + { m < 0}.
Lemma not_Zeq_inf : forall n m:Z, n <> m -> { n < m } + { m < n }.
Lemma Z_dec : forall n m:Z, { n < m } + { n > m } + { n = m }.
Lemma Z_dec' : forall n m:Z, { n < m } + { m < n } + { n = m }.