theorem nle_gen_succ_2: \forall y,x. x <= succ y \to
x = zero \lor \exists z. x = succ z \land z <= y.
intros 2; elim x; clear x; intros;
theorem nle_gen_succ_2: \forall y,x. x <= succ y \to
x = zero \lor \exists z. x = succ z \land z <= y.
intros 2; elim x; clear x; intros;