intros 4. elim H; clear H x y.
apply eq_gen_S_O. exact m. elim H1. auto paramodulation.
clear H2. cut (n = m).
-elim Hcut. apply ex_intro. exact n1. split; auto.
-apply eq_gen_S_S. auto.
+elim Hcut. apply ex_intro. exact n1. split; autobatch.
+apply eq_gen_S_S. autobatch.
qed.
theorem le_gen_S_x: \forall m,x. (le (S m) x) \to
theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z).
intros 1. elim x; clear H. clear x.
auto paramodulation.
-fwd H1 [H]. decompose H.
+fwd H1 [H]. decompose.
*)