-theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < exp n m.
-intros.elim m.simplify.reflexivity.
-simplify.
-apply trans_le ? ((S(S O))*(S n1)).
+theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.
+intros.elim m.simplify.unfold lt.reflexivity.
+simplify.unfold lt.
+apply (trans_le ? ((S(S O))*(S n1))).