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

• useful Bottom-up lemmas

• 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

Simplification lemmas

No subgoal or smaller subgoals

Reversible simplification lemmas (no loss of information)

Should clearly be declared as hints Lemmas ending by eq

Lemmas ending by Zgt

Lemmas ending by Zlt

Lemmas ending by Zle

Irreversible simplification lemmas

Probably to be declared as hints, when no other simplification is possible Lemmas ending by eq

Lemmas ending by Zge

Lemmas ending by Zlt

Lemmas ending by Zle