-rewrite > Zsucc_plus (pos e1).
-rewrite > Zsucc_plus (pos e1).
-rewrite > Zsucc_plus (Zplus (pos e1) y).
-apply f_equal.assumption.
+rewrite > Zplus_Zsucc (pos n1).
+rewrite > Zplus_Zsucc (pos n1).
+rewrite > Zplus_Zsucc (Zplus (pos n1) y).
+apply eq_f.assumption.
+qed.
+
+variant assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z))
+\def associative_Zplus.
+
+(* Zopp *)
+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.