This file centralizes the lemmas about Z, classifying them
according to the way they can be used in automatic search
|
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.
Hint Resolve
Zsucc_eq_compat
Zsucc_gt_compat Zgt_succ Zorder.Zgt_pos_0 Zplus_gt_compat_l Zplus_gt_compat_r
Zlt_succ Zsucc_lt_compat Zlt_pred Zplus_lt_compat_l Zplus_lt_compat_r
Zle_0_nat Zorder.Zle_0_pos Zle_refl Zle_succ Zsucc_le_compat Zle_pred Zle_min_l Zle_min_r Zplus_le_compat_l Zplus_le_compat_r Zabs_pos
BinInt.Z_eq_mult Zplus_eq_compat
Zorder.Zmult_ge_compat_r Zorder.Zmult_ge_compat_l Zorder.Zmult_ge_compat
Zorder.Zmult_gt_0_compat Zlt_lt_succ
Zorder.Zmult_le_0_compat Zorder.Zmult_le_compat_r Zorder.Zmult_le_compat_l Zplus_le_0_compat Zle_le_succ Zplus_le_compat
: zarith.