src/HOL/Fact.thy

--- a/src/HOL/Fact.thy	Mon Dec 19 13:58:54 2011 +0100
+++ b/src/HOL/Fact.thy	Mon Dec 19 14:41:08 2011 +0100
@@ -285,6 +285,12 @@
     (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
 by (cases m) auto
 
+lemma fact_le_power: "fact n \<le> n^n"
+proof (induct n)
+  case (Suc n)
+  then have "fact n \<le> Suc n ^ n" by (rule le_trans) (simp add: power_mono)
+  then show ?case by (simp add: add_le_mono)
+qed simp
 
 subsection {* @{term fact} and @{term of_nat} *}