(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/factorial".
-
include "nat/le_arith.ma".
let rec fact n \def
[ 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.