qed.
theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m.
-intros.elim m.simplify.apply le_n.
-simplify.rewrite > times_n_SO.
+intros.elim m.simplify.unfold lt.apply le_n.
+simplify.unfold lt.rewrite > times_n_SO.
apply le_times.assumption.assumption.
qed.
theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.
-intros.elim m.simplify.reflexivity.
-simplify.
+intros.elim m.simplify.unfold lt.reflexivity.
+simplify.unfold lt.
apply (trans_le ? ((S(S O))*(S n1))).
simplify.
rewrite < plus_n_Sm.apply le_S_S.apply le_S_S.
apply H1.
(* esprimere inj_times senza S *)
cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b).
-apply Hcut.simplify. apply le_S_S_to_le. apply le_S. assumption.
+apply Hcut.simplify.unfold lt.apply le_S_S_to_le. apply le_S. assumption.
assumption.
intros 2.
apply (nat_case n).