# Library Coq.ZArith.Zcompare

Binary Integers : results about Z.compare Initial author: Pierre CrÃ©gut (CNET, Lannion, France
THIS FILE IS DEPRECATED. It is now almost entirely made of compatibility formulations for results already present in BinInt.Z.

Require Export BinPos BinInt.
Require Import Lt Gt Plus Mult.
Local Open Scope Z_scope.

# Comparison on integers

Lemma Zcompare_Gt_Lt_antisym : forall n m:Z, (n ?= m) = Gt <-> (m ?= n) = Lt.

Lemma Zcompare_antisym n m : CompOpp (n ?= m) = (m ?= n).

# Transitivity of comparison

Lemma Zcompare_Lt_trans :
forall n m p:Z, (n ?= m) = Lt -> (m ?= p) = Lt -> (n ?= p) = Lt.

Lemma Zcompare_Gt_trans :
forall n m p:Z, (n ?= m) = Gt -> (m ?= p) = Gt -> (n ?= p) = Gt.

# Relating x?=y to =, <=, <, >= or >

Lemma Zcompare_elim :
forall (c1 c2 c3:Prop) (n m:Z),
(n = m -> c1) ->
(n < m -> c2) ->
(n > m -> c3) -> match n ?= m with
| Eq => c1
| Lt => c2
| Gt => c3
end.

Lemma Zcompare_eq_case :
forall (c1 c2 c3:Prop) (n m:Z),
c1 -> n = m -> match n ?= m with
| Eq => c1
| Lt => c2
| Gt => c3
end.

Lemma Zle_compare :
forall n m:Z,
n <= m -> match n ?= m with
| Eq => True
| Lt => True
| Gt => False
end.

Lemma Zlt_compare :
forall n m:Z,
n < m -> match n ?= m with
| Eq => False
| Lt => True
| Gt => False
end.

Lemma Zge_compare :
forall n m:Z,
n >= m -> match n ?= m with
| Eq => True
| Lt => False
| Gt => True
end.

Lemma Zgt_compare :
forall n m:Z,
n > m -> match n ?= m with
| Eq => False
| Lt => False
| Gt => True
end.

Compatibility notations

Notation Zcompare_Eq_eq := Z.compare_eq (only parsing).
Notation Zcompare_Eq_iff_eq := Z.compare_eq_iff (only parsing).
Notation Zabs_non_eq := Z.abs_neq (only parsing).
Notation Zsgn_0 := Z.sgn_null (only parsing).
Notation Zsgn_1 := Z.sgn_pos (only parsing).
Notation Zsgn_m1 := Z.sgn_neg (only parsing).

Not kept: Zcompare_egal_dec