-intros.elim x.simplify.reflexivity.
-elim n.rewrite < (Zpred_Zplus_neg_O (y+z)).
-rewrite < (Zpred_Zplus_neg_O y).
-rewrite < Zplus_Zpred.
-reflexivity.
-rewrite > Zplus_Zpred (neg n1).
-rewrite > Zplus_Zpred (neg n1).
-rewrite > Zplus_Zpred ((neg n1)+y).
-apply eq_f.assumption.
-elim n.rewrite < Zsucc_Zplus_pos_O.
-rewrite < Zsucc_Zplus_pos_O.
-rewrite > Zplus_Zsucc.
-reflexivity.
-rewrite > Zplus_Zsucc (pos n1).
-rewrite > Zplus_Zsucc (pos n1).
-rewrite > Zplus_Zsucc ((pos n1)+y).
-apply eq_f.assumption.
+intros.elim x.
+ simplify.reflexivity.
+ elim n.
+ rewrite < Zsucc_Zplus_pos_O.rewrite < Zsucc_Zplus_pos_O.
+ rewrite > Zplus_Zsucc.reflexivity.
+ rewrite > (Zplus_Zsucc (pos n1)).rewrite > (Zplus_Zsucc (pos n1)).
+ rewrite > (Zplus_Zsucc ((pos n1)+y)).apply eq_f.assumption.
+ elim n.
+ rewrite < (Zpred_Zplus_neg_O (y+z)).rewrite < (Zpred_Zplus_neg_O y).
+ rewrite < Zplus_Zpred.reflexivity.
+ rewrite > (Zplus_Zpred (neg n1)).rewrite > (Zplus_Zpred (neg n1)).
+ rewrite > (Zplus_Zpred ((neg n1)+y)).apply eq_f.assumption.