\lambda z.
match z with
[ OZ \Rightarrow O
-| (pos n) \Rightarrow n
-| (neg n) \Rightarrow n].
+| (pos n) \Rightarrow (S n)
+| (neg n) \Rightarrow (S n)].
definition OZ_test \def
\lambda z.
theorem injective_pos: injective nat Z pos.
unfold injective.
intros.
+apply inj_S.
change with (abs (pos x) = abs (pos y)).
apply eq_f.assumption.
qed.
theorem injective_neg: injective nat Z neg.
unfold injective.
intros.
+apply inj_S.
change with (abs (neg x) = abs (neg y)).
apply eq_f.assumption.
qed.