-theorem le_SSO_fact : \forall n. (S O) < n \to (S(S O)) \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.
+theorem le_SSO_fact : \forall n. (S O) < n \to (S(S O)) \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.