proposition: Lemma Z_inj_nat_inj: forall (x y : Z), Z_inj_nat x = Z_inj_nat y -> x = y.
proof: Proof. intros x y H. apply (f_equal Z_inj_nat_rev) in H. do 2 rewrite Z_inj_nat_id in H. assumption. Qed.
imports: ZArith ConstructiveEpsilon