# Library Coq.ZArith.Zorder

Binary Integers (Pierre Crégut, CNET, Lannion, France)
Require Import BinPos.
Require Import BinInt.
Require Import Arith_base.
Require Import Decidable.
Require Import Zcompare.
Open Local Scope Z_scope.
Implicit Types x y z : Z.
Properties of the order relations on binary integers

# Trichotomy

Theorem Ztrichotomy_inf : forall n m:Z, {n < m} + {n = m} + {n > m}.
Theorem Ztrichotomy : forall n m:Z, n < m \/ n = m \/ n > m.

# Decidability of equality and order on Z

Theorem dec_eq : forall n m:Z, decidable (n = m).
Theorem dec_Zne : forall n m:Z, decidable (Zne n m).
Theorem dec_Zle : forall n m:Z, decidable (n <= m).
Theorem dec_Zgt : forall n m:Z, decidable (n > m).
Theorem dec_Zge : forall n m:Z, decidable (n >= m).
Theorem dec_Zlt : forall n m:Z, decidable (n < m).
Theorem not_Zeq : forall n m:Z, n <> m -> n < m \/ m < n.

# Relating strict and large orders

Lemma Zgt_lt : forall n m:Z, n > m -> m < n.
Lemma Zlt_gt : forall n m:Z, n < m -> m > n.
Lemma Zge_le : forall n m:Z, n >= m -> m <= n.
Lemma Zle_ge : forall n m:Z, n <= m -> m >= n.
Lemma Zle_not_gt : forall n m:Z, n <= m -> ~ n > m.
Lemma Zgt_not_le : forall n m:Z, n > m -> ~ n <= m.
Lemma Zle_not_lt : forall n m:Z, n <= m -> ~ m < n.
Lemma Zlt_not_le : forall n m:Z, n < m -> ~ m <= n.
Lemma Znot_ge_lt : forall n m:Z, ~ n >= m -> n < m.
Lemma Znot_lt_ge : forall n m:Z, ~ n < m -> n >= m.
Lemma Znot_gt_le : forall n m:Z, ~ n > m -> n <= m.
Lemma Znot_le_gt : forall n m:Z, ~ n <= m -> n > m.
Lemma Zge_iff_le : forall n m:Z, n >= m <-> m <= n.
Lemma Zgt_iff_lt : forall n m:Z, n > m <-> m < n.

# Equivalence and order properties

Reflexivity
Lemma Zle_refl : forall n:Z, n <= n.
Lemma Zeq_le : forall n m:Z, n = m -> n <= m.
Hint Resolve Zle_refl: zarith.
Antisymmetry
Lemma Zle_antisym : forall n m:Z, n <= m -> m <= n -> n = m.
Asymmetry
Lemma Zgt_asym : forall n m:Z, n > m -> ~ m > n.
Lemma Zlt_asym : forall n m:Z, n < m -> ~ m < n.
Irreflexivity
Lemma Zgt_irrefl : forall n:Z, ~ n > n.
Lemma Zlt_irrefl : forall n:Z, ~ n < n.
Lemma Zlt_not_eq : forall n m:Z, n < m -> n <> m.
Large = strict or equal
Lemma Zlt_le_weak : forall n m:Z, n < m -> n <= m.
Lemma Zle_lt_or_eq : forall n m:Z, n <= m -> n < m \/ n = m.
Lemma Zle_lt_or_eq_iff : forall n m, n <= m <-> n < m \/ n = m.
Dichotomy
Lemma Zle_or_lt : forall n m:Z, n <= m \/ m < n.
Transitivity of strict orders
Lemma Zgt_trans : forall n m p:Z, n > m -> m > p -> n > p.
Lemma Zlt_trans : forall n m p:Z, n < m -> m < p -> n < p.
Mixed transitivity
Lemma Zle_gt_trans : forall n m p:Z, m <= n -> m > p -> n > p.
Lemma Zgt_le_trans : forall n m p:Z, n > m -> p <= m -> n > p.
Lemma Zlt_le_trans : forall n m p:Z, n < m -> m <= p -> n < p.
Lemma Zle_lt_trans : forall n m p:Z, n <= m -> m < p -> n < p.
Transitivity of large orders
Lemma Zle_trans : forall n m p:Z, n <= m -> m <= p -> n <= p.
Lemma Zge_trans : forall n m p:Z, n >= m -> m >= p -> n >= p.
Hint Resolve Zle_trans: zarith.

# Compatibility of order and operations on Z

## Successor

Compatibility of successor wrt to order
Lemma Zsucc_le_compat : forall n m:Z, m <= n -> Zsucc m <= Zsucc n.
Lemma Zsucc_gt_compat : forall n m:Z, m > n -> Zsucc m > Zsucc n.
Lemma Zsucc_lt_compat : forall n m:Z, n < m -> Zsucc n < Zsucc m.
Hint Resolve Zsucc_le_compat: zarith.
Simplification of successor wrt to order
Lemma Zsucc_gt_reg : forall n m:Z, Zsucc m > Zsucc n -> m > n.
Lemma Zsucc_le_reg : forall n m:Z, Zsucc m <= Zsucc n -> m <= n.
Lemma Zsucc_lt_reg : forall n m:Z, Zsucc n < Zsucc m -> n < m.
Special base instances of order
Lemma Zgt_succ : forall n:Z, Zsucc n > n.
Lemma Znot_le_succ : forall n:Z, ~ Zsucc n <= n.
Lemma Zlt_succ : forall n:Z, n < Zsucc n.
Lemma Zlt_pred : forall n:Z, Zpred n < n.
Relating strict and large order using successor or predecessor
Lemma Zgt_le_succ : forall n m:Z, m > n -> Zsucc n <= m.
Lemma Zle_gt_succ : forall n m:Z, n <= m -> Zsucc m > n.
Lemma Zle_lt_succ : forall n m:Z, n <= m -> n < Zsucc m.
Lemma Zlt_le_succ : forall n m:Z, n < m -> Zsucc n <= m.
Lemma Zgt_succ_le : forall n m:Z, Zsucc m > n -> n <= m.
Lemma Zlt_succ_le : forall n m:Z, n < Zsucc m -> n <= m.
Lemma Zle_succ_gt : forall n m:Z, Zsucc n <= m -> m > n.
Lemma Zlt_succ_r : forall n m, n < Zsucc m <-> n <= m.
Weakening order
Lemma Zle_succ : forall n:Z, n <= Zsucc n.
Hint Resolve Zle_succ: zarith.
Lemma Zle_pred : forall n:Z, Zpred n <= n.
Lemma Zlt_lt_succ : forall n m:Z, n < m -> n < Zsucc m.
Lemma Zle_le_succ : forall n m:Z, n <= m -> n <= Zsucc m.
Lemma Zle_succ_le : forall n m:Z, Zsucc n <= m -> n <= m.
Hint Resolve Zle_le_succ: zarith.
Relating order wrt successor and order wrt predecessor
Lemma Zgt_succ_pred : forall n m:Z, m > Zsucc n -> Zpred m > n.
Lemma Zlt_succ_pred : forall n m:Z, Zsucc n < m -> n < Zpred m.
Relating strict order and large order on positive
Lemma Zlt_0_le_0_pred : forall n:Z, 0 < n -> 0 <= Zpred n.
Lemma Zgt_0_le_0_pred : forall n:Z, n > 0 -> 0 <= Zpred n.
Special cases of ordered integers
Lemma Zlt_0_1 : 0 < 1.
Lemma Zle_0_1 : 0 <= 1.
Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q.
Lemma Zgt_pos_0 : forall p:positive, Zpos p > 0.
Lemma Zle_0_pos : forall p:positive, 0 <= Zpos p.
Lemma Zlt_neg_0 : forall p:positive, Zneg p < 0.
Lemma Zle_0_nat : forall n:nat, 0 <= Z_of_nat n.
Hint Immediate Zeq_le: zarith.
Transitivity using successor
Lemma Zgt_trans_succ : forall n m p:Z, Zsucc n > m -> m > p -> n > p.
Derived lemma
Lemma Zgt_succ_gt_or_eq : forall n m:Z, Zsucc n > m -> n > m \/ m = n.

## Addition

Compatibility of addition wrt to order
Lemma Zplus_gt_compat_l : forall n m p:Z, n > m -> p + n > p + m.
Lemma Zplus_gt_compat_r : forall n m p:Z, n > m -> n + p > m + p.
Lemma Zplus_le_compat_l : forall n m p:Z, n <= m -> p + n <= p + m.
Lemma Zplus_le_compat_r : forall n m p:Z, n <= m -> n + p <= m + p.
Lemma Zplus_lt_compat_l : forall n m p:Z, n < m -> p + n < p + m.
Lemma Zplus_lt_compat_r : forall n m p:Z, n < m -> n + p < m + p.
Lemma Zplus_lt_le_compat : forall n m p q:Z, n < m -> p <= q -> n + p < m + q.
Lemma Zplus_le_lt_compat : forall n m p q:Z, n <= m -> p < q -> n + p < m + q.
Lemma Zplus_le_compat : forall n m p q:Z, n <= m -> p <= q -> n + p <= m + q.
Lemma Zplus_lt_compat : forall n m p q:Z, n < m -> p < q -> n + p < m + q.
Compatibility of addition wrt to being positive
Lemma Zplus_le_0_compat : forall n m:Z, 0 <= n -> 0 <= m -> 0 <= n + m.
Simplification of addition wrt to order
Lemma Zplus_gt_reg_l : forall n m p:Z, p + n > p + m -> n > m.
Lemma Zplus_gt_reg_r : forall n m p:Z, n + p > m + p -> n > m.
Lemma Zplus_le_reg_l : forall n m p:Z, p + n <= p + m -> n <= m.
Lemma Zplus_le_reg_r : forall n m p:Z, n + p <= m + p -> n <= m.
Lemma Zplus_lt_reg_l : forall n m p:Z, p + n < p + m -> n < m.
Lemma Zplus_lt_reg_r : forall n m p:Z, n + p < m + p -> n < m.

## Multiplication

Compatibility of multiplication by a positive wrt to order
Lemma Zmult_le_compat_r : forall n m p:Z, n <= m -> 0 <= p -> n * p <= m * p.
Lemma Zmult_le_compat_l : forall n m p:Z, n <= m -> 0 <= p -> p * n <= p * m.
Lemma Zmult_lt_compat_r : forall n m p:Z, 0 < p -> n < m -> n * p < m * p.
Lemma Zmult_gt_compat_r : forall n m p:Z, p > 0 -> n > m -> n * p > m * p.
Lemma Zmult_gt_0_lt_compat_r :
forall n m p:Z, p > 0 -> n < m -> n * p < m * p.
Lemma Zmult_gt_0_le_compat_r :
forall n m p:Z, p > 0 -> n <= m -> n * p <= m * p.
Lemma Zmult_lt_0_le_compat_r :
forall n m p:Z, 0 < p -> n <= m -> n * p <= m * p.
Lemma Zmult_gt_0_lt_compat_l :
forall n m p:Z, p > 0 -> n < m -> p * n < p * m.
Lemma Zmult_lt_compat_l : forall n m p:Z, 0 < p -> n < m -> p * n < p * m.
Lemma Zmult_gt_compat_l : forall n m p:Z, p > 0 -> n > m -> p * n > p * m.
Lemma Zmult_ge_compat_r : forall n m p:Z, n >= m -> p >= 0 -> n * p >= m * p.
Lemma Zmult_ge_compat_l : forall n m p:Z, n >= m -> p >= 0 -> p * n >= p * m.
Lemma Zmult_ge_compat :
forall n m p q:Z, n >= p -> m >= q -> p >= 0 -> q >= 0 -> n * m >= p * q.
Lemma Zmult_le_compat :
forall n m p q:Z, n <= p -> m <= q -> 0 <= n -> 0 <= m -> n * m <= p * q.
Simplification of multiplication by a positive wrt to being positive
Lemma Zmult_gt_0_lt_reg_r : forall n m p:Z, p > 0 -> n * p < m * p -> n < m.
Lemma Zmult_lt_reg_r : forall n m p:Z, 0 < p -> n * p < m * p -> n < m.
Lemma Zmult_le_reg_r : forall n m p:Z, p > 0 -> n * p <= m * p -> n <= m.
Lemma Zmult_lt_0_le_reg_r : forall n m p:Z, 0 < p -> n * p <= m * p -> n <= m.
Lemma Zmult_ge_reg_r : forall n m p:Z, p > 0 -> n * p >= m * p -> n >= m.
Lemma Zmult_gt_reg_r : forall n m p:Z, p > 0 -> n * p > m * p -> n > m.
Compatibility of multiplication by a positive wrt to being positive
Lemma Zmult_le_0_compat : forall n m:Z, 0 <= n -> 0 <= m -> 0 <= n * m.
Lemma Zmult_gt_0_compat : forall n m:Z, n > 0 -> m > 0 -> n * m > 0.
Lemma Zmult_lt_0_compat : forall n m:Z, 0 < n -> 0 < m -> 0 < n * m.
For compatibility
Notation Zmult_lt_O_compat := Zmult_lt_0_compat (only parsing).
Lemma Zmult_gt_0_le_0_compat : forall n m:Z, n > 0 -> 0 <= m -> 0 <= m * n.
Simplification of multiplication by a positive wrt to being positive
Lemma Zmult_le_0_reg_r : forall n m:Z, n > 0 -> 0 <= m * n -> 0 <= m.
Lemma Zmult_gt_0_lt_0_reg_r : forall n m:Z, n > 0 -> 0 < m * n -> 0 < m.
Lemma Zmult_lt_0_reg_r : forall n m:Z, 0 < n -> 0 < m * n -> 0 < m.
Lemma Zmult_gt_0_reg_l : forall n m:Z, n > 0 -> n * m > 0 -> m > 0.

## Square

Simplification of square wrt order
Lemma Zgt_square_simpl :
forall n m:Z, n >= 0 -> n * n > m * m -> n > m.
Lemma Zlt_square_simpl :
forall n m:Z, 0 <= n -> m * m < n * n -> m < n.

# Equivalence between inequalities

Lemma Zle_plus_swap : forall n m p:Z, n + p <= m <-> n <= m - p.
Lemma Zlt_plus_swap : forall n m p:Z, n + p < m <-> n < m - p.
Lemma Zeq_plus_swap : forall n m p:Z, n + p = m <-> n = m - p.
Lemma Zlt_minus_simpl_swap : forall n m:Z, 0 < m -> n - m < n.
Lemma Zlt_0_minus_lt : forall n m:Z, 0 < n - m -> m < n.
Lemma Zle_0_minus_le : forall n m:Z, 0 <= n - m -> m <= n.
Lemma Zle_minus_le_0 : forall n m:Z, m <= n -> 0 <= n - m.
Lemma Zmult_lt_compat:
forall n m p q : Z, 0 <= n < p -> 0 <= m < q -> n * m < p * q.
Lemma Zmult_lt_compat2:
forall n m p q : Z, 0 < n <= p -> 0 < m < q -> n * m < p * q.
For compatibility
Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing).