cut n = m. elim Hcut. apply ex_intro. exact n1. auto paramodulation. auto. (* paramodulation non trova la prova *)
qed.
theorem le_gen_S_x: \forall m,x. (le (S m) x) \to
(\exists n. x = (S n) \land (le m n)).
cut n = m. elim Hcut. apply ex_intro. exact n1. auto paramodulation. auto. (* paramodulation non trova la prova *)
qed.
theorem le_gen_S_x: \forall m,x. (le (S m) x) \to
(\exists n. x = (S n) \land (le m n)).