qed.
theorem le_gen_S_x_aux: \forall m,x,y. (le y x) \to (y = S m) \to
(\exists n. x = (S n) \land (le m n)).
intros 4. elim H; clear H x y.
qed.
theorem le_gen_S_x_aux: \forall m,x,y. (le y x) \to (y = S m) \to
(\exists n. x = (S n) \land (le m n)).
intros 4. elim H; clear H x y.