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.
apply eq_gen_S_O. exact m. elim H1. auto paramodulation.
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.
apply eq_gen_S_O. exact m. elim H1. auto paramodulation.