-
-definition Zopp : Z \to Z \def
-\lambda x:Z. match x with
-[ OZ \Rightarrow OZ
-| (pos n) \Rightarrow (neg n)
-| (neg n) \Rightarrow (pos n) ].
-
-theorem Zplus_Zopp: \forall x:Z. (eq Z (Zplus x (Zopp x)) OZ).
-intro.elim x.
-apply refl_eq.
-simplify.
-rewrite > nat_compare_n_n.
-simplify.apply refl_eq.
-simplify.
-rewrite > nat_compare_n_n.
-simplify.apply refl_eq.
-qed.