Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(* -*- coding: utf-8 -*- *)
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Binary Integers : results about order predicates

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 Import BinPos BinInt Decidable Zcompare.
Require Import Arith_base. (* Useless now, for compatibility only *)

Local Open Scope Z_scope.

(*********************************************************)

Properties of the order relations on binary integers

Trichotomy

Theorem Ztrichotomy_inf n m : {n < m} + {n = m} + {n > m}.n, m:Z
{n < m} + {n = m} + {n > m}
Proof.n, m:Z
{n < m} + {n = m} + {n > m}
  unfold ">", "<".n, m:Z
{(n ?= m) = Lt} + {n = m} + {(n ?= m) = Gt} generalize (Z.compare_eq n m).n, m:Z
((n ?= m) = Eq -> n = m) ->
{(n ?= m) = Lt} + {n = m} + {(n ?= m) = Gt}
  destruct (n ?= m); [ left; right | left; left | right]; auto.
Defined.

Theorem Ztrichotomy n m : n < m \/ n = m \/ n > m.n, m:Z
n < m \/ n = m \/ n > m
Proof.n, m:Z
n < m \/ n = m \/ n > m
  Z.swap_greater.n, m:Z
n < m \/ n = m \/ m < n apply Z.lt_trichotomy.
Qed.

(**********************************************************************)

Decidability of equality and order on Z

Notation dec_eq := Z.eq_decidable (only parsing).
Notation dec_Zle := Z.le_decidable (only parsing).
Notation dec_Zlt := Z.lt_decidable (only parsing).

Theorem dec_Zne n m : decidable (Zne n m).n, m:Z
decidable (Zne n m)
Proof.n, m:Z
decidable (Zne n m)
  destruct (Z.eq_decidable n m); [right|left]; subst; auto.
Qed.

Theorem dec_Zgt n m : decidable (n > m).n, m:Z
decidable (n > m)
Proof.n, m:Z
decidable (n > m)
  destruct (Z.lt_decidable m n); [left|right]; Z.swap_greater; auto.
Qed.

Theorem dec_Zge n m : decidable (n >= m).n, m:Z
decidable (n >= m)
Proof.n, m:Z
decidable (n >= m)
  destruct (Z.le_decidable m n); [left|right]; Z.swap_greater; auto.
Qed.

Theorem not_Zeq n m : n <> m -> n < m \/ m < n.n, m:Z
n <> m -> n < m \/ m < n
Proof.n, m:Z
n <> m -> n < m \/ m < n
  apply Z.lt_gt_cases.
Qed.

Register dec_Zne as plugins.omega.dec_Zne.
Register dec_Zgt as plugins.omega.dec_Zgt.
Register dec_Zge as plugins.omega.dec_Zge.
Register not_Zeq as plugins.omega.not_Zeq.

Relating strict and large orders

Notation Zgt_iff_lt := Z.gt_lt_iff (only parsing).
Notation Zge_iff_le := Z.ge_le_iff (only parsing).

Lemma Zle_not_lt n m : n <= m -> ~ m < n.n, m:Z
n <= m -> ~ m < n
Proof.n, m:Z
n <= m -> ~ m < n
 apply Z.le_ngt.
Qed.

Lemma Zlt_not_le n m : n < m -> ~ m <= n.n, m:Z
n < m -> ~ m <= n
Proof.n, m:Z
n < m -> ~ m <= n
 apply Z.lt_nge.
Qed.

Lemma Zle_not_gt n m : n <= m -> ~ n > m.n, m:Z
n <= m -> ~ n > m
Proof.n, m:Z
n <= m -> ~ n > m
  trivial.
Qed.

Lemma Zgt_not_le n m : n > m -> ~ n <= m.n, m:Z
n > m -> ~ n <= m
Proof.n, m:Z
n > m -> ~ n <= m
  Z.swap_greater.n, m:Z
m < n -> ~ n <= m apply Z.lt_nge.
Qed.

Lemma Znot_ge_lt n m : ~ n >= m -> n < m.n, m:Z
~ n >= m -> n < m
Proof.n, m:Z
~ n >= m -> n < m
  Z.swap_greater.n, m:Z
~ m <= n -> n < m apply Z.nle_gt.
Qed.

Lemma Znot_lt_ge n m : ~ n < m -> n >= m.n, m:Z
~ n < m -> n >= m
Proof.n, m:Z
~ n < m -> n >= m
  trivial.
Qed.

Lemma Znot_gt_le n m: ~ n > m -> n <= m.n, m:Z
~ n > m -> n <= m
Proof.n, m:Z
~ n > m -> n <= m
  trivial.
Qed.

Lemma Znot_le_gt n m : ~ n <= m -> n > m.n, m:Z
~ n <= m -> n > m
Proof.n, m:Z
~ n <= m -> n > m
  Z.swap_greater.n, m:Z
~ n <= m -> m < n apply Z.nle_gt.
Qed.

Lemma not_Zne n m : ~ Zne n m -> n = m.n, m:Z
~ Zne n m -> n = m
Proof.n, m:Z
~ Zne n m -> n = m
  intros H.n, m:Z
H:~ Zne n m
n = m
  destruct (Z.eq_decidable n m); [assumption|now elim H].
Qed.

Register Znot_le_gt as plugins.omega.Znot_le_gt.
Register Znot_lt_ge as plugins.omega.Znot_lt_ge.
Register Znot_ge_lt as plugins.omega.Znot_ge_lt.
Register Znot_gt_le as plugins.omega.Znot_gt_le.
Register not_Zne as plugins.omega.not_Zne.

Equivalence and order properties

Reflexivity

Notation Zeq_le := Z.eq_le_incl (only parsing).

Hint Resolve Z.le_refl: zarith.

Antisymmetry

Notation Zle_antisym := Z.le_antisymm (only parsing).

Asymmetry

Notation Zlt_asym := Z.lt_asymm (only parsing).

Lemma Zgt_asym n m : n > m -> ~ m > n.n, m:Z
n > m -> ~ m > n
Proof.n, m:Z
n > m -> ~ m > n
  Z.swap_greater.n, m:Z
m < n -> ~ n < m apply Z.lt_asymm.
Qed.

Irreflexivity

Notation Zlt_not_eq := Z.lt_neq (only parsing).

Lemma Zgt_irrefl n : ~ n > n.n:Z
~ n > n
Proof.n:Z
~ n > n
  Z.swap_greater.n:Z
~ n < n apply Z.lt_irrefl.
Qed.

Large = strict or equal

Notation Zlt_le_weak := Z.lt_le_incl (only parsing).
Notation Zle_lt_or_eq_iff := Z.lt_eq_cases (only parsing).

Lemma Zle_lt_or_eq n m : n <= m -> n < m \/ n = m.n, m:Z
n <= m -> n < m \/ n = m
Proof.n, m:Z
n <= m -> n < m \/ n = m
  apply Z.lt_eq_cases.
Qed.

Dichotomy

Notation Zle_or_lt := Z.le_gt_cases (only parsing).

Transitivity of strict orders

Lemma Zgt_trans n m p : n > m -> m > p -> n > p.n, m, p:Z
n > m -> m > p -> n > p
Proof.n, m, p:Z
n > m -> m > p -> n > p
  Z.swap_greater.n, m, p:Z
m < n -> p < m -> p < n intros; now transitivity m.
Qed.

Mixed transitivity

Lemma Zle_gt_trans n m p : m <= n -> m > p -> n > p.n, m, p:Z
m <= n -> m > p -> n > p
Proof.n, m, p:Z
m <= n -> m > p -> n > p
  Z.swap_greater.n, m, p:Z
m <= n -> p < m -> p < n Z.order.
Qed.

Lemma Zgt_le_trans n m p : n > m -> p <= m -> n > p.n, m, p:Z
n > m -> p <= m -> n > p
Proof.n, m, p:Z
n > m -> p <= m -> n > p
  Z.swap_greater.n, m, p:Z
m < n -> p <= m -> p < n Z.order.
Qed.

Transitivity of large orders

Lemma Zge_trans n m p : n >= m -> m >= p -> n >= p.n, m, p:Z
n >= m -> m >= p -> n >= p
Proof.n, m, p:Z
n >= m -> m >= p -> n >= p
  Z.swap_greater.n, m, p:Z
m <= n -> p <= m -> p <= n Z.order.
Qed.

Hint Resolve Z.le_trans: zarith.

Compatibility of order and operations on Z

Successor

Compatibility of successor wrt to order

Lemma Zsucc_le_compat n m : m <= n -> Z.succ m <= Z.succ n.n, m:Z
m <= n -> Z.succ m <= Z.succ n
Proof.n, m:Z
m <= n -> Z.succ m <= Z.succ n
  apply Z.succ_le_mono.
Qed.

Lemma Zsucc_lt_compat n m : n < m -> Z.succ n < Z.succ m.n, m:Z
n < m -> Z.succ n < Z.succ m
Proof.n, m:Z
n < m -> Z.succ n < Z.succ m
  apply Z.succ_lt_mono.
Qed.

Lemma Zsucc_gt_compat n m : m > n -> Z.succ m > Z.succ n.n, m:Z
m > n -> Z.succ m > Z.succ n
Proof.n, m:Z
m > n -> Z.succ m > Z.succ n
  Z.swap_greater.n, m:Z
n < m -> Z.succ n < Z.succ m apply Z.succ_lt_mono.
Qed.

Hint Resolve Zsucc_le_compat: zarith.

Simplification of successor wrt to order

Lemma Zsucc_gt_reg n m : Z.succ m > Z.succ n -> m > n.n, m:Z
Z.succ m > Z.succ n -> m > n
Proof.n, m:Z
Z.succ m > Z.succ n -> m > n
  Z.swap_greater.n, m:Z
Z.succ n < Z.succ m -> n < m apply Z.succ_lt_mono.
Qed.

Lemma Zsucc_le_reg n m : Z.succ m <= Z.succ n -> m <= n.n, m:Z
Z.succ m <= Z.succ n -> m <= n
Proof.n, m:Z
Z.succ m <= Z.succ n -> m <= n
  apply Z.succ_le_mono.
Qed.

Lemma Zsucc_lt_reg n m : Z.succ n < Z.succ m -> n < m.n, m:Z
Z.succ n < Z.succ m -> n < m
Proof.n, m:Z
Z.succ n < Z.succ m -> n < m
  apply Z.succ_lt_mono.
Qed.

Special base instances of order

Notation Zlt_succ := Z.lt_succ_diag_r (only parsing).
Notation Zlt_pred := Z.lt_pred_l (only parsing).

Lemma Zgt_succ n : Z.succ n > n.n:Z
Z.succ n > n
Proof.n:Z
Z.succ n > n
  Z.swap_greater.n:Z
n < Z.succ n apply Z.lt_succ_diag_r.
Qed.

Lemma Znot_le_succ n : ~ Z.succ n <= n.n:Z
~ Z.succ n <= n
Proof.n:Z
~ Z.succ n <= n
  apply Z.lt_nge, Z.lt_succ_diag_r.
Qed.

Relating strict and large order using successor or predecessor

Lemma Zgt_le_succ n m : m > n -> Z.succ n <= m.n, m:Z
m > n -> Z.succ n <= m
Proof.n, m:Z
m > n -> Z.succ n <= m
  Z.swap_greater.n, m:Z
n < m -> Z.succ n <= m apply Z.le_succ_l.
Qed.

Lemma Zle_gt_succ n m : n <= m -> Z.succ m > n.n, m:Z
n <= m -> Z.succ m > n
Proof.n, m:Z
n <= m -> Z.succ m > n
  Z.swap_greater.n, m:Z
n <= m -> n < Z.succ m apply Z.lt_succ_r.
Qed.

Lemma Zle_lt_succ n m : n <= m -> n < Z.succ m.n, m:Z
n <= m -> n < Z.succ m
Proof.n, m:Z
n <= m -> n < Z.succ m
  apply Z.lt_succ_r.
Qed.

Lemma Zlt_le_succ n m : n < m -> Z.succ n <= m.n, m:Z
n < m -> Z.succ n <= m
Proof.n, m:Z
n < m -> Z.succ n <= m
  apply Z.le_succ_l.
Qed.

Lemma Zgt_succ_le n m : Z.succ m > n -> n <= m.n, m:Z
Z.succ m > n -> n <= m
Proof.n, m:Z
Z.succ m > n -> n <= m
  Z.swap_greater.n, m:Z
n < Z.succ m -> n <= m apply Z.lt_succ_r.
Qed.

Lemma Zlt_succ_le n m : n < Z.succ m -> n <= m.n, m:Z
n < Z.succ m -> n <= m
Proof.n, m:Z
n < Z.succ m -> n <= m
  apply Z.lt_succ_r.
Qed.

Lemma Zle_succ_gt n m : Z.succ n <= m -> m > n.n, m:Z
Z.succ n <= m -> m > n
Proof.n, m:Z
Z.succ n <= m -> m > n
  Z.swap_greater.n, m:Z
Z.succ n <= m -> n < m apply Z.le_succ_l.
Qed.

Weakening order

Notation Zle_succ := Z.le_succ_diag_r (only parsing).
Notation Zle_pred := Z.le_pred_l (only parsing).
Notation Zlt_lt_succ := Z.lt_lt_succ_r (only parsing).
Notation Zle_le_succ := Z.le_le_succ_r (only parsing).

Lemma Zle_succ_le n m : Z.succ n <= m -> n <= m.n, m:Z
Z.succ n <= m -> n <= m
Proof.n, m:Z
Z.succ n <= m -> n <= m
  intros.n, m:Z
H:Z.succ n <= m
n <= m now apply Z.lt_le_incl, Z.le_succ_l.
Qed.

Hint Resolve Z.le_succ_diag_r: zarith.
Hint Resolve Z.le_le_succ_r: zarith.

Relating order wrt successor and order wrt predecessor

Lemma Zgt_succ_pred n m : m > Z.succ n -> Z.pred m > n.n, m:Z
m > Z.succ n -> Z.pred m > n
Proof.n, m:Z
m > Z.succ n -> Z.pred m > n
  Z.swap_greater.n, m:Z
Z.succ n < m -> n < Z.pred m apply Z.lt_succ_lt_pred.
Qed.

Lemma Zlt_succ_pred n m : Z.succ n < m -> n < Z.pred m.n, m:Z
Z.succ n < m -> n < Z.pred m
Proof.n, m:Z
Z.succ n < m -> n < Z.pred m
  apply Z.lt_succ_lt_pred.
Qed.

Relating strict order and large order on positive

Lemma Zlt_0_le_0_pred n : 0 < n -> 0 <= Z.pred n.n:Z
0 < n -> 0 <= Z.pred n
Proof.n:Z
0 < n -> 0 <= Z.pred n
  apply Z.lt_le_pred.
Qed.

Lemma Zgt_0_le_0_pred n : n > 0 -> 0 <= Z.pred n.n:Z
n > 0 -> 0 <= Z.pred n
Proof.n:Z
n > 0 -> 0 <= Z.pred n
  Z.swap_greater.n:Z
0 < n -> 0 <= Z.pred n apply Z.lt_le_pred.
Qed.

Special cases of ordered integers

Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q.forall p q : positive, Z.neg p <= Z.pos q
Proof.forall p q : positive, Z.neg p <= Z.pos q
  exact Pos2Z.neg_le_pos.
Qed.

Lemma Zgt_pos_0 : forall p:positive, Zpos p > 0.forall p : positive, Z.pos p > 0
Proof.forall p : positive, Z.pos p > 0
  easy.
Qed.

(* weaker but useful (in [Z.pow] for instance) *)
Lemma Zle_0_pos : forall p:positive, 0 <= Zpos p.forall p : positive, 0 <= Z.pos p
Proof.forall p : positive, 0 <= Z.pos p
  exact Pos2Z.pos_is_nonneg.
Qed.

Lemma Zlt_neg_0 : forall p:positive, Zneg p < 0.forall p : positive, Z.neg p < 0
Proof.forall p : positive, Z.neg p < 0
  exact Pos2Z.neg_is_neg.
Qed.

Lemma Zle_0_nat : forall n:nat, 0 <= Z.of_nat n.forall n : nat, 0 <= Z.of_nat n
Proof.forall n : nat, 0 <= Z.of_nat n
  induction n; simpl; intros.0 <= 0
n:nat
IHn:0 <= Z.of_nat n
0 <= Z.pos (Pos.of_succ_nat n) apply Z.le_refl.n:nat
IHn:0 <= Z.of_nat n
0 <= Z.pos (Pos.of_succ_nat n) easy.
Qed.

Hint Immediate Z.eq_le_incl: zarith.

Derived lemma

Lemma Zgt_succ_gt_or_eq n m : Z.succ n > m -> n > m \/ m = n.n, m:Z
Z.succ n > m -> n > m \/ m = n
Proof.n, m:Z
Z.succ n > m -> n > m \/ m = n
  Z.swap_greater.n, m:Z
m < Z.succ n -> m < n \/ m = n intros.n, m:Z
H:m < Z.succ n
m < n \/ m = n now apply Z.lt_eq_cases, Z.lt_succ_r.
Qed.

Addition

Compatibility of addition wrt to order

Notation Zplus_lt_le_compat := Z.add_lt_le_mono (only parsing).
Notation Zplus_le_lt_compat := Z.add_le_lt_mono (only parsing).
Notation Zplus_le_compat := Z.add_le_mono (only parsing).
Notation Zplus_lt_compat := Z.add_lt_mono (only parsing).

Lemma Zplus_gt_compat_l n m p : n > m -> p + n > p + m.n, m, p:Z
n > m -> p + n > p + m
Proof.n, m, p:Z
n > m -> p + n > p + m
  Z.swap_greater.n, m, p:Z
m < n -> p + m < p + n apply Z.add_lt_mono_l.
Qed.

Lemma Zplus_gt_compat_r n m p : n > m -> n + p > m + p.n, m, p:Z
n > m -> n + p > m + p
Proof.n, m, p:Z
n > m -> n + p > m + p
  Z.swap_greater.n, m, p:Z
m < n -> m + p < n + p apply Z.add_lt_mono_r.
Qed.

Lemma Zplus_le_compat_l n m p : n <= m -> p + n <= p + m.n, m, p:Z
n <= m -> p + n <= p + m
Proof.n, m, p:Z
n <= m -> p + n <= p + m
  apply Z.add_le_mono_l.
Qed.

Lemma Zplus_le_compat_r n m p : n <= m -> n + p <= m + p.n, m, p:Z
n <= m -> n + p <= m + p
Proof.n, m, p:Z
n <= m -> n + p <= m + p
  apply Z.add_le_mono_r.
Qed.

Lemma Zplus_lt_compat_l n m p : n < m -> p + n < p + m.n, m, p:Z
n < m -> p + n < p + m
Proof.n, m, p:Z
n < m -> p + n < p + m
  apply Z.add_lt_mono_l.
Qed.

Lemma Zplus_lt_compat_r n m p : n < m -> n + p < m + p.n, m, p:Z
n < m -> n + p < m + p
Proof.n, m, p:Z
n < m -> n + p < m + p
  apply Z.add_lt_mono_r.
Qed.

Compatibility of addition wrt to being positive

Notation Zplus_le_0_compat := Z.add_nonneg_nonneg (only parsing).

Simplification of addition wrt to order

Lemma Zplus_le_reg_l n m p : p + n <= p + m -> n <= m.n, m, p:Z
p + n <= p + m -> n <= m
Proof.n, m, p:Z
p + n <= p + m -> n <= m
 apply Z.add_le_mono_l.
Qed.

Lemma Zplus_le_reg_r n m p : n + p <= m + p -> n <= m.n, m, p:Z
n + p <= m + p -> n <= m
Proof.n, m, p:Z
n + p <= m + p -> n <= m
 apply Z.add_le_mono_r.
Qed.

Lemma Zplus_lt_reg_l n m p : p + n < p + m -> n < m.n, m, p:Z
p + n < p + m -> n < m
Proof.n, m, p:Z
p + n < p + m -> n < m
 apply Z.add_lt_mono_l.
Qed.

Lemma Zplus_lt_reg_r n m p : n + p < m + p -> n < m.n, m, p:Z
n + p < m + p -> n < m
Proof.n, m, p:Z
n + p < m + p -> n < m
 apply Z.add_lt_mono_r.
Qed.

Lemma Zplus_gt_reg_l n m p : p + n > p + m -> n > m.n, m, p:Z
p + n > p + m -> n > m
Proof.n, m, p:Z
p + n > p + m -> n > m
 Z.swap_greater.n, m, p:Z
p + m < p + n -> m < n apply Z.add_lt_mono_l.
Qed.

Lemma Zplus_gt_reg_r n m p : n + p > m + p -> n > m.n, m, p:Z
n + p > m + p -> n > m
Proof.n, m, p:Z
n + p > m + p -> n > m
 Z.swap_greater.n, m, p:Z
m + p < n + p -> m < n apply Z.add_lt_mono_r.
Qed.

Multiplication

Compatibility of multiplication by a positive wrt to order

Lemma Zmult_le_compat_r n m p : n <= m -> 0 <= p -> n * p <= m * p.n, m, p:Z
n <= m -> 0 <= p -> n * p <= m * p
Proof.n, m, p:Z
n <= m -> 0 <= p -> n * p <= m * p
 intros.n, m, p:Z
H:n <= m
H0:0 <= p
n * p <= m * p now apply Z.mul_le_mono_nonneg_r.
Qed.

Lemma Zmult_le_compat_l n m p : n <= m -> 0 <= p -> p * n <= p * m.n, m, p:Z
n <= m -> 0 <= p -> p * n <= p * m
Proof.n, m, p:Z
n <= m -> 0 <= p -> p * n <= p * m
 intros.n, m, p:Z
H:n <= m
H0:0 <= p
p * n <= p * m now apply Z.mul_le_mono_nonneg_l.
Qed.

Lemma Zmult_lt_compat_r n m p : 0 < p -> n < m -> n * p < m * p.n, m, p:Z
0 < p -> n < m -> n * p < m * p
Proof.n, m, p:Z
0 < p -> n < m -> n * p < m * p
 apply Z.mul_lt_mono_pos_r.
Qed.

Lemma Zmult_gt_compat_r n m p : p > 0 -> n > m -> n * p > m * p.n, m, p:Z
p > 0 -> n > m -> n * p > m * p
Proof.n, m, p:Z
p > 0 -> n > m -> n * p > m * p
 Z.swap_greater.n, m, p:Z
0 < p -> m < n -> m * p < n * p apply Z.mul_lt_mono_pos_r.
Qed.

Lemma Zmult_gt_0_lt_compat_r n m p : p > 0 -> n < m -> n * p < m * p.n, m, p:Z
p > 0 -> n < m -> n * p < m * p
Proof.n, m, p:Z
p > 0 -> n < m -> n * p < m * p
 Z.swap_greater.n, m, p:Z
0 < p -> n < m -> n * p < m * p apply Z.mul_lt_mono_pos_r.
Qed.

Lemma Zmult_gt_0_le_compat_r n m p : p > 0 -> n <= m -> n * p <= m * p.n, m, p:Z
p > 0 -> n <= m -> n * p <= m * p
Proof.n, m, p:Z
p > 0 -> n <= m -> n * p <= m * p
 Z.swap_greater.n, m, p:Z
0 < p -> n <= m -> n * p <= m * p apply Z.mul_le_mono_pos_r.
Qed.

Lemma Zmult_lt_0_le_compat_r n m p : 0 < p -> n <= m -> n * p <= m * p.n, m, p:Z
0 < p -> n <= m -> n * p <= m * p
Proof.n, m, p:Z
0 < p -> n <= m -> n * p <= m * p
 apply Z.mul_le_mono_pos_r.
Qed.

Lemma Zmult_gt_0_lt_compat_l n m p : p > 0 -> n < m -> p * n < p * m.n, m, p:Z
p > 0 -> n < m -> p * n < p * m
Proof.n, m, p:Z
p > 0 -> n < m -> p * n < p * m
 Z.swap_greater.n, m, p:Z
0 < p -> n < m -> p * n < p * m apply Z.mul_lt_mono_pos_l.
Qed.

Lemma Zmult_lt_compat_l n m p : 0 < p -> n < m -> p * n < p * m.n, m, p:Z
0 < p -> n < m -> p * n < p * m
Proof.n, m, p:Z
0 < p -> n < m -> p * n < p * m
 apply Z.mul_lt_mono_pos_l.
Qed.

Lemma Zmult_gt_compat_l n m p : p > 0 -> n > m -> p * n > p * m.n, m, p:Z
p > 0 -> n > m -> p * n > p * m
Proof.n, m, p:Z
p > 0 -> n > m -> p * n > p * m
 Z.swap_greater.n, m, p:Z
0 < p -> m < n -> p * m < p * n apply Z.mul_lt_mono_pos_l.
Qed.

Lemma Zmult_ge_compat_r n m p : n >= m -> p >= 0 -> n * p >= m * p.n, m, p:Z
n >= m -> p >= 0 -> n * p >= m * p
Proof.n, m, p:Z
n >= m -> p >= 0 -> n * p >= m * p
 Z.swap_greater.n, m, p:Z
m <= n -> 0 <= p -> m * p <= n * p intros.n, m, p:Z
H:m <= n
H0:0 <= p
m * p <= n * p now apply Z.mul_le_mono_nonneg_r.
Qed.

Lemma Zmult_ge_compat_l n m p : n >= m -> p >= 0 -> p * n >= p * m.n, m, p:Z
n >= m -> p >= 0 -> p * n >= p * m
Proof.n, m, p:Z
n >= m -> p >= 0 -> p * n >= p * m
 Z.swap_greater.n, m, p:Z
m <= n -> 0 <= p -> p * m <= p * n intros.n, m, p:Z
H:m <= n
H0:0 <= p
p * m <= p * n now apply Z.mul_le_mono_nonneg_l.
Qed.

Lemma Zmult_ge_compat n m p q :
  n >= p -> m >= q -> p >= 0 -> q >= 0 -> n * m >= p * q.n, m, p, q:Z
n >= p -> m >= q -> p >= 0 -> q >= 0 -> n * m >= p * q
Proof.n, m, p, q:Z
n >= p -> m >= q -> p >= 0 -> q >= 0 -> n * m >= p * q
 Z.swap_greater.n, m, p, q:Z
p <= n -> q <= m -> 0 <= p -> 0 <= q -> p * q <= n * m intros.n, m, p, q:Z
H:p <= n
H0:q <= m
H1:0 <= p
H2:0 <= q
p * q <= n * m now apply Z.mul_le_mono_nonneg.
Qed.

Lemma Zmult_le_compat n m p q :
  n <= p -> m <= q -> 0 <= n -> 0 <= m -> n * m <= p * q.n, m, p, q:Z
n <= p -> m <= q -> 0 <= n -> 0 <= m -> n * m <= p * q
Proof.n, m, p, q:Z
n <= p -> m <= q -> 0 <= n -> 0 <= m -> n * m <= p * q
 intros.n, m, p, q:Z
H:n <= p
H0:m <= q
H1:0 <= n
H2:0 <= m
n * m <= p * q now apply Z.mul_le_mono_nonneg.
Qed.

Simplification of multiplication by a positive wrt to being positive

Lemma Zmult_gt_0_lt_reg_r n m p : p > 0 -> n * p < m * p -> n < m.n, m, p:Z
p > 0 -> n * p < m * p -> n < m
Proof.n, m, p:Z
p > 0 -> n * p < m * p -> n < m
 Z.swap_greater.n, m, p:Z
0 < p -> n * p < m * p -> n < m apply Z.mul_lt_mono_pos_r.
Qed.

Lemma Zmult_lt_reg_r n m p : 0 < p -> n * p < m * p -> n < m.n, m, p:Z
0 < p -> n * p < m * p -> n < m
Proof.n, m, p:Z
0 < p -> n * p < m * p -> n < m
 apply Z.mul_lt_mono_pos_r.
Qed.

Lemma Zmult_le_reg_r n m p : p > 0 -> n * p <= m * p -> n <= m.n, m, p:Z
p > 0 -> n * p <= m * p -> n <= m
Proof.n, m, p:Z
p > 0 -> n * p <= m * p -> n <= m
 Z.swap_greater.n, m, p:Z
0 < p -> n * p <= m * p -> n <= m apply Z.mul_le_mono_pos_r.
Qed.

Lemma Zmult_lt_0_le_reg_r n m p : 0 < p -> n * p <= m * p -> n <= m.n, m, p:Z
0 < p -> n * p <= m * p -> n <= m
Proof.n, m, p:Z
0 < p -> n * p <= m * p -> n <= m
 apply Z.mul_le_mono_pos_r.
Qed.

Lemma Zmult_ge_reg_r n m p : p > 0 -> n * p >= m * p -> n >= m.n, m, p:Z
p > 0 -> n * p >= m * p -> n >= m
Proof.n, m, p:Z
p > 0 -> n * p >= m * p -> n >= m
 Z.swap_greater.n, m, p:Z
0 < p -> m * p <= n * p -> m <= n apply Z.mul_le_mono_pos_r.
Qed.

Lemma Zmult_gt_reg_r n m p : p > 0 -> n * p > m * p -> n > m.n, m, p:Z
p > 0 -> n * p > m * p -> n > m
Proof.n, m, p:Z
p > 0 -> n * p > m * p -> n > m
 Z.swap_greater.n, m, p:Z
0 < p -> m * p < n * p -> m < n apply Z.mul_lt_mono_pos_r.
Qed.

Lemma Zmult_lt_compat n m p q :
  0 <= n < p -> 0 <= m < q -> n * m < p * q.n, m, p, q:Z
0 <= n < p -> 0 <= m < q -> n * m < p * q
Proof.n, m, p, q:Z
0 <= n < p -> 0 <= m < q -> n * m < p * q
 intros (Hn,Hnp) (Hm,Hmq).n, m, p, q:Z
Hn:0 <= n
Hnp:n < p
Hm:0 <= m
Hmq:m < q
n * m < p * q now apply Z.mul_lt_mono_nonneg.
Qed.

Lemma Zmult_lt_compat2 n m p q :
  0 < n <= p -> 0 < m < q -> n * m < p * q.n, m, p, q:Z
0 < n <= p -> 0 < m < q -> n * m < p * q
Proof.n, m, p, q:Z
0 < n <= p -> 0 < m < q -> n * m < p * q
  intros (Hn, Hnp) (Hm,Hmq).n, m, p, q:Z
Hn:0 < n
Hnp:n <= p
Hm:0 < m
Hmq:m < q
n * m < p * q
  apply Z.le_lt_trans with (p * m).n, m, p, q:Z
Hn:0 < n
Hnp:n <= p
Hm:0 < m
Hmq:m < q
n * m <= p * m
n, m, p, q:Z
Hn:0 < n
Hnp:n <= p
Hm:0 < m
Hmq:m < q
p * m < p * q
   apply Z.mul_le_mono_pos_r; trivial.n, m, p, q:Z
Hn:0 < n
Hnp:n <= p
Hm:0 < m
Hmq:m < q
p * m < p * q
   apply Z.mul_lt_mono_pos_l; Z.order.
Qed.

Compatibility of multiplication by a positive wrt to being positive

Notation Zmult_le_0_compat := Z.mul_nonneg_nonneg (only parsing).
Notation Zmult_lt_0_compat := Z.mul_pos_pos (only parsing).
Notation Zmult_lt_O_compat := Z.mul_pos_pos (only parsing).

Lemma Zmult_gt_0_compat n m : n > 0 -> m > 0 -> n * m > 0.n, m:Z
n > 0 -> m > 0 -> n * m > 0
Proof.n, m:Z
n > 0 -> m > 0 -> n * m > 0
 Z.swap_greater.n, m:Z
0 < n -> 0 < m -> 0 < n * m apply Z.mul_pos_pos.
Qed.

(* To remove someday ... *)

Lemma Zmult_gt_0_le_0_compat n m : n > 0 -> 0 <= m -> 0 <= m * n.n, m:Z
n > 0 -> 0 <= m -> 0 <= m * n
Proof.n, m:Z
n > 0 -> 0 <= m -> 0 <= m * n
 Z.swap_greater.n, m:Z
0 < n -> 0 <= m -> 0 <= m * n intros.n, m:Z
H:0 < n
H0:0 <= m
0 <= m * n apply Z.mul_nonneg_nonneg.n, m:Z
H:0 < n
H0:0 <= m
0 <= m
n, m:Z
H:0 < n
H0:0 <= m
0 <= n trivial.n, m:Z
H:0 < n
H0:0 <= m
0 <= n
  now apply Z.lt_le_incl.
Qed.

Simplification of multiplication by a positive wrt to being positive

Lemma Zmult_le_0_reg_r n m : n > 0 -> 0 <= m * n -> 0 <= m.n, m:Z
n > 0 -> 0 <= m * n -> 0 <= m
Proof.n, m:Z
n > 0 -> 0 <= m * n -> 0 <= m
 Z.swap_greater.n, m:Z
0 < n -> 0 <= m * n -> 0 <= m apply Z.mul_nonneg_cancel_r.
Qed.

Lemma Zmult_lt_0_reg_r n m : 0 < n -> 0 < m * n -> 0 < m.n, m:Z
0 < n -> 0 < m * n -> 0 < m
Proof.n, m:Z
0 < n -> 0 < m * n -> 0 < m
 apply Z.mul_pos_cancel_r.
Qed.

Lemma Zmult_gt_0_lt_0_reg_r n m : n > 0 -> 0 < m * n -> 0 < m.n, m:Z
n > 0 -> 0 < m * n -> 0 < m
Proof.n, m:Z
n > 0 -> 0 < m * n -> 0 < m
 Z.swap_greater.n, m:Z
0 < n -> 0 < m * n -> 0 < m apply Z.mul_pos_cancel_r.
Qed.

Lemma Zmult_gt_0_reg_l n m : n > 0 -> n * m > 0 -> m > 0.n, m:Z
n > 0 -> n * m > 0 -> m > 0
Proof.n, m:Z
n > 0 -> n * m > 0 -> m > 0
 Z.swap_greater.n, m:Z
0 < n -> 0 < n * m -> 0 < m apply Z.mul_pos_cancel_l.
Qed.

Square

Simplification of square wrt order

Lemma Zlt_square_simpl n m : 0 <= n -> m * m < n * n -> m < n.n, m:Z
0 <= n -> m * m < n * n -> m < n
Proof.n, m:Z
0 <= n -> m * m < n * n -> m < n
 apply Z.square_lt_simpl_nonneg.
Qed.

Lemma Zgt_square_simpl n m : n >= 0 -> n * n > m * m -> n > m.n, m:Z
n >= 0 -> n * n > m * m -> n > m
Proof.n, m:Z
n >= 0 -> n * n > m * m -> n > m
 Z.swap_greater.n, m:Z
0 <= n -> m * m < n * n -> m < n apply Z.square_lt_simpl_nonneg.
Qed.

Equivalence between inequalities

Notation Zle_plus_swap := Z.le_add_le_sub_r (only parsing).
Notation Zlt_plus_swap := Z.lt_add_lt_sub_r (only parsing).
Notation Zlt_minus_simpl_swap := Z.lt_sub_pos (only parsing).

Lemma Zeq_plus_swap n m p : n + p = m <-> n = m - p.n, m, p:Z
n + p = m <-> n = m - p
Proof.n, m, p:Z
n + p = m <-> n = m - p
 apply Z.add_move_r.
Qed.

Lemma Zlt_0_minus_lt n m : 0 < n - m -> m < n.n, m:Z
0 < n - m -> m < n
Proof.n, m:Z
0 < n - m -> m < n
 apply Z.lt_0_sub.
Qed.

Lemma Zle_0_minus_le n m : 0 <= n - m -> m <= n.n, m:Z
0 <= n - m -> m <= n
Proof.n, m:Z
0 <= n - m -> m <= n
 apply Z.le_0_sub.
Qed.

Lemma Zle_minus_le_0 n m : m <= n -> 0 <= n - m.n, m:Z
m <= n -> 0 <= n - m
Proof.n, m:Z
m <= n -> 0 <= n - m
 apply Z.le_0_sub.
Qed.

For compatibility

Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing).