Library Stdlib.ZArith.Zhints
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
- simplification lemmas (only those are declared as Hints)
- reversible lemmas relating operators
- irreversible lemmas with meta-variables
- unclear or too specific lemmas
- lemmas to be used as rewrite rules
Lemmas involving positive and compare are not taken into account
From Stdlib Require Import BinInt.
From Stdlib Require Import Zorder.
From Stdlib Require Import Zmin.
From Stdlib Require Import Zabs.
From Stdlib Require Import Zcompare.
From Stdlib Require Import Znat.
From Stdlib Require Import auxiliary.
From Stdlib Require Import Zmisc.
From Stdlib Require Import Wf_Z.
Simplification lemmas
No subgoal or smaller subgoals
#[global]
Hint Resolve
Reversible simplification lemmas (no loss of information)
Should clearly be declared as hints
Lemmas ending by eq
Zsucc_eq_compat
Lemmas ending by Z.gt
Zsucc_gt_compat
Zgt_succ
Zorder.Zgt_pos_0
Zplus_gt_compat_l
Zplus_gt_compat_r
Lemmas ending by Z.lt
Pos2Z.is_pos
Z.lt_succ_diag_r
Zsucc_lt_compat
Z.lt_pred_l
Zplus_lt_compat_l
Zplus_lt_compat_r
Lemmas ending by Z.le
Nat2Z.is_nonneg
Pos2Z.is_nonneg
Z.le_refl
Z.le_succ_diag_r
Zsucc_le_compat
Z.le_pred_l
Z.le_min_l
Z.le_min_r
Zplus_le_compat_l
Zplus_le_compat_r
Z.abs_nonneg
Irreversible simplification lemmas
Probably to be declared as hints, when no other simplification is possible
Lemmas ending by eq
Z_eq_mult
Zplus_eq_compat
Lemmas ending by Z.ge
Zorder.Zmult_ge_compat_r
Zorder.Zmult_ge_compat_l
Zorder.Zmult_ge_compat
Lemmas ending by Z.lt
Zorder.Zmult_gt_0_compat
Z.lt_lt_succ_r
Lemmas ending by Z.le
Z.mul_nonneg_nonneg
Zorder.Zmult_le_compat_r
Zorder.Zmult_le_compat_l
Z.add_nonneg_nonneg
Z.le_le_succ_r
Z.add_le_mono
: zarith.