intros.elim z.
simplify.reflexivity.
simplify.intros.
-cut match neg e1 with
+cut match neg n with
[ OZ \Rightarrow True
| (pos n) \Rightarrow False
| (neg n) \Rightarrow False].
apply Hcut.rewrite > H.simplify.exact I.
simplify.intros.
-cut match pos e2 with
+cut match pos n with
[ OZ \Rightarrow True
| (pos n) \Rightarrow False
| (neg n) \Rightarrow False].
theorem Zpred_Zsucc: \forall z:Z. eq Z (Zpred (Zsucc z)) z.
intros.elim z.reflexivity.
-elim e1.reflexivity.
+elim n.reflexivity.
reflexivity.
reflexivity.
qed.
theorem Zsucc_Zpred: \forall z:Z. eq Z (Zsucc (Zpred z)) z.
intros.elim z.reflexivity.
reflexivity.
-elim e2.reflexivity.
+elim n.reflexivity.
reflexivity.
qed.
intros.elim z.
simplify.reflexivity.
simplify.reflexivity.
-elim e2.simplify.reflexivity.
+elim n.simplify.reflexivity.
simplify.reflexivity.
qed.
theorem Zsucc_Zplus_pos_O : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z).
intros.elim z.
simplify.reflexivity.
-elim e1.simplify.reflexivity.
+elim n.simplify.reflexivity.
simplify.reflexivity.
simplify.reflexivity.
qed.
(\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro.
intros.elim n1.
simplify. reflexivity.
-elim e1.simplify. reflexivity.
+elim n2.simplify. reflexivity.
simplify. reflexivity.
intros. elim n1.
simplify. reflexivity.
(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro.
intros.elim n1.
simplify. reflexivity.
-elim e1.simplify. reflexivity.
+elim n2.simplify. reflexivity.
simplify. reflexivity.
intros. elim n1.
simplify. reflexivity.
(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))).
intros.elim n1.
simplify. reflexivity.
-elim e1.simplify. reflexivity.
+elim n2.simplify. reflexivity.
simplify. reflexivity.
intros. elim n1.
simplify. reflexivity.
change with \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)).
(* simplify. *)
intros.elim x.simplify.reflexivity.
-elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)).
+elim n.rewrite < (Zpred_Zplus_neg_O (Zplus y z)).
rewrite < (Zpred_Zplus_neg_O y).
rewrite < Zplus_Zpred.
reflexivity.
-rewrite > Zplus_Zpred (neg e).
-rewrite > Zplus_Zpred (neg e).
-rewrite > Zplus_Zpred (Zplus (neg e) y).
+rewrite > Zplus_Zpred (neg n1).
+rewrite > Zplus_Zpred (neg n1).
+rewrite > Zplus_Zpred (Zplus (neg n1) y).
apply eq_f.assumption.
-elim e2.rewrite < Zsucc_Zplus_pos_O.
+elim n.rewrite < Zsucc_Zplus_pos_O.
rewrite < Zsucc_Zplus_pos_O.
rewrite > Zplus_Zsucc.
reflexivity.
-rewrite > Zplus_Zsucc (pos e1).
-rewrite > Zplus_Zsucc (pos e1).
-rewrite > Zplus_Zsucc (Zplus (pos e1) y).
+rewrite > Zplus_Zsucc (pos n1).
+rewrite > Zplus_Zsucc (pos n1).
+rewrite > Zplus_Zsucc (Zplus (pos n1) y).
apply eq_f.assumption.
qed.