intros.change with ((S m) < (S m)*m!).
apply (lt_to_le_to_lt ? ((S m)*(S (S O)))).
rewrite < sym_times.
-simplify.
+simplify.unfold lt.
apply le_S_S.rewrite < plus_n_O.
apply le_plus_n.
apply le_times_r.apply le_SSO_fact.
-simplify.apply le_S_S_to_le.exact H.
+simplify.unfold lt.apply le_S_S_to_le.exact H.
qed.