theorem OZ_test_to_Prop :\forall z:Z.
match OZ_test z with
[true \Rightarrow z=OZ
-|false \Rightarrow \lnot (z=OZ)].
+|false \Rightarrow z \neq OZ].
intros.elim z.
simplify.reflexivity.
simplify.intros [H].
variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
\def injective_neg.
-theorem not_eq_OZ_pos: \forall n:nat. \lnot (OZ = (pos n)).
+theorem not_eq_OZ_pos: \forall n:nat. OZ \neq pos n.
simplify.intros [n; H].
discriminate H.
qed.
-theorem not_eq_OZ_neg :\forall n:nat. \lnot (OZ = (neg n)).
+theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n.
simplify.intros [n; H].
discriminate H.
qed.
-theorem not_eq_pos_neg :\forall n,m:nat. \lnot ((pos n) = (neg m)).
+theorem not_eq_pos_neg :\forall n,m:nat. pos n \neq neg m.
simplify.intros [n; m; H].
discriminate H.
qed.