-intros 2.elim x.
-cut OZ < y \to Zsucc OZ \leq y.
-apply Hcut. assumption.simplify.elim y.
-simplify.exact H1.
-simplify.exact H1.
-simplify.apply le_O_n.
-cut neg n < y \to Zsucc (neg n) \leq y.
-apply Hcut. assumption.elim n.
-cut neg O < y \to Zsucc (neg O) \leq y.
-apply Hcut. assumption.simplify.elim y.
-simplify.exact I.simplify.apply not_le_Sn_O n1 H2.
-simplify.exact I.
-cut neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y.
-apply Hcut. assumption.simplify.
-elim y.
-simplify.exact I.
-simplify.apply le_S_S_to_le n2 n1 H3.
-simplify.exact I.
-exact H.
+intros 2.
+elim x.
+(* goal: x=OZ *)
+ cut (OZ < y \to Zsucc OZ \leq y).
+ apply Hcut. assumption.
+ simplify.elim y.
+ simplify.exact H1.
+ simplify.apply le_O_n.
+ simplify.exact H1.
+(* goal: x=pos *)
+ exact H.
+(* goal: x=neg *)
+ cut (neg n < y \to Zsucc (neg n) \leq y).
+ apply Hcut. assumption.
+ elim n.
+ cut (neg O < y \to Zsucc (neg O) \leq y).
+ apply Hcut. assumption.
+ simplify.elim y.
+ simplify.exact I.
+ simplify.exact I.
+ simplify.apply (not_le_Sn_O n1 H2).
+ cut (neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y).
+ apply Hcut. assumption.simplify.
+ elim y.
+ simplify.exact I.
+ simplify.exact I.
+ simplify.apply (le_S_S_to_le n2 n1 H3).