[ O \Rightarrow (S O)
| (S m) \Rightarrow (S m)*(fact m)].
-interpretation "factorial" 'fact n = (cic:/matita/nat/factorial/fact.con n).
+interpretation "factorial" 'fact n = (fact n).
theorem le_SO_fact : \forall n. (S O) \le n!.
intro.elim n.simplify.apply le_n.