[ OZ \Rightarrow True
| (pos n) \Rightarrow False
| (neg n) \Rightarrow False].
apply Hcut.rewrite > H.simplify.exact I.
simplify.intros.
[ OZ \Rightarrow True
| (pos n) \Rightarrow False
| (neg n) \Rightarrow False].
apply Hcut.rewrite > H.simplify.exact I.
simplify.intros.
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.
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.
-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).
-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).