Library Coqtail.mytheories.MyZ

Require Import ZArith.
Require Import Setoid.

Local Open Scope Z_scope.

Add Parametric Relation : Z Zle
reflexivity proved by Zle_refl
transitivity proved by Zle_trans as le.

Lemma eq_Zle : (x y : Z), x = yx y.
Proof.
intros ; subst ; reflexivity.
Qed.