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.
(************************************************************************)
(*         *   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)         *)
(************************************************************************)
This file centralizes the lemmas about Z, classifying them according to the way they can be used in automatic search
Lemmas which clearly leads to simplification during proof search are
declared as Hints. A definite status (Hint or not) for the other lemmas
remains to be given
Structure of the file
Lemmas involving positive and compare are not taken into account 
Require Import BinInt.
Require Import Zorder.
Require Import Zmin.
Require Import Zabs.
Require Import Zcompare.
Require Import Znat.
Require Import auxiliary.
Require Import Zmisc.
Require Import Wf_Z.

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

Simplification lemmas

No subgoal or smaller subgoals 
Hint Resolve
  (** ** Reversible simplification lemmas (no loss of information)      *)
  (** Should clearly be declared as hints                               *)

  (** Lemmas ending by eq *)
  Zsucc_eq_compat (* n = m -> Z.succ n = Z.succ m *)

  (** Lemmas ending by Z.gt *)
  Zsucc_gt_compat (* m > n -> Z.succ m > Z.succ n *)
  Zgt_succ (* Z.succ n > n *)
  Zorder.Zgt_pos_0 (* Z.pos p > 0 *)
  Zplus_gt_compat_l (* n > m -> p+n > p+m *)
  Zplus_gt_compat_r (* n > m -> n+p > m+p *)

  (** Lemmas ending by Z.lt *)
  Pos2Z.is_pos (* 0 < Z.pos p *)
  Z.lt_succ_diag_r (* n < Z.succ n *)
  Zsucc_lt_compat (* n < m -> Z.succ n < Z.succ m *)
  Z.lt_pred_l (* Z.pred n < n *)
  Zplus_lt_compat_l (* n < m -> p+n < p+m *)
  Zplus_lt_compat_r (* n < m -> n+p < m+p *)

  (** Lemmas ending by Z.le *)
  Nat2Z.is_nonneg (* 0 <= Z.of_nat n *)
  Pos2Z.is_nonneg (* 0 <= Z.pos p *)
  Z.le_refl (* n <= n *)
  Z.le_succ_diag_r (* n <= Z.succ n *)
  Zsucc_le_compat (* m <= n -> Z.succ m <= Z.succ n *)
  Z.le_pred_l (* Z.pred n <= n *)
  Z.le_min_l (* Z.min n m <= n *)
  Z.le_min_r (* Z.min n m <= m *)
  Zplus_le_compat_l (* n <= m -> p+n <= p+m *)
  Zplus_le_compat_r (* a <= b -> a+c <= b+c *)
  Z.abs_nonneg (* 0 <= |x| *)

  (** ** Irreversible simplification lemmas *)
  (** Probably to be declared as hints, when no other simplification is possible *)

  (** Lemmas ending by eq *)
  Z_eq_mult (* y = 0 -> y*x = 0 *)
  Zplus_eq_compat (* n = m -> p = q -> n+p = m+q *)

  (** Lemmas ending by Z.ge *)
  Zorder.Zmult_ge_compat_r (* a >= b -> c >= 0 -> a*c >= b*c *)
  Zorder.Zmult_ge_compat_l (* a >= b -> c >= 0 -> c*a >= c*b *)
  Zorder.Zmult_ge_compat (* :
      a >= c -> b >= d -> c >= 0 -> d >= 0 -> a*b >= c*d *)

  (** Lemmas ending by Z.lt *)
  Zorder.Zmult_gt_0_compat (* a > 0 -> b > 0 -> a*b > 0 *)
  Z.lt_lt_succ_r (* n < m -> n < Z.succ m *)

  (** Lemmas ending by Z.le *)
  Z.mul_nonneg_nonneg (* 0 <= x -> 0 <= y -> 0 <= x*y *)
  Zorder.Zmult_le_compat_r (* a <= b -> 0 <= c -> a*c <= b*c *)
  Zorder.Zmult_le_compat_l (* a <= b -> 0 <= c -> c*a <= c*b *)
  Z.add_nonneg_nonneg (* 0 <= x -> 0 <= y -> 0 <= x+y *)
  Z.le_le_succ_r (* x <= y -> x <= Z.succ y *)
  Z.add_le_mono (* n <= m -> p <= q -> n+p <= m+q *)

  : zarith.