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.
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.