src/HOL/Fact.thy
changeset 45930 2a882ef2cd73
parent 41550 efa734d9b221
child 46240 933f35c4e126
     1.1 --- a/src/HOL/Fact.thy	Mon Dec 19 13:58:54 2011 +0100
     1.2 +++ b/src/HOL/Fact.thy	Mon Dec 19 14:41:08 2011 +0100
     1.3 @@ -285,6 +285,12 @@
     1.4      (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
     1.5  by (cases m) auto
     1.6  
     1.7 +lemma fact_le_power: "fact n \<le> n^n"
     1.8 +proof (induct n)
     1.9 +  case (Suc n)
    1.10 +  then have "fact n \<le> Suc n ^ n" by (rule le_trans) (simp add: power_mono)
    1.11 +  then show ?case by (simp add: add_le_mono)
    1.12 +qed simp
    1.13  
    1.14  subsection {* @{term fact} and @{term of_nat} *}
    1.15