-intro.apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H.
-intros.change with (S (S O)) \le (S m)*m!.
-apply trans_le ? ((S(S O))*(S O)).apply le_n.
+intro.apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H).
+intros.change with ((S (S O)) \le (S m)*m!).
+apply (trans_le ? ((S(S O))*(S O))).apply le_n.