- \exists z. y = succ z \land x <= z.
- intros. inversion H; clear H; intros;
- [ apply (eq_gen_succ_zero ? ? H)
- | lapply linear eq_gen_succ_succ to H2 as H0.
- rewrite > H0. clear H0.
- apply ex_intro; [|auto] (**)
- ].
+ \exists z. y = succ z \land x <= z.
+ unfold NLE.
+ intros. decompose.
+ lapply linear nplus_gen_succ_2 to H1 as H.
+ decompose. subst.
+ apply ex_intro; auto. (**)