# 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.

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 Zlt_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 Zlt_succ_gt : forall n m:Z, Zsucc n <= m -> m > n.

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.

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).