src/HOL/Fact.thy
changeset 50240 019d642d422d
parent 50224 aacd6da09825
child 57113 7e95523302e6
     1.1 --- a/src/HOL/Fact.thy	Mon Nov 26 21:46:04 2012 +0100
     1.2 +++ b/src/HOL/Fact.thy	Tue Nov 27 10:56:31 2012 +0100
     1.3 @@ -315,4 +315,13 @@
     1.4      by (auto simp: image_iff)
     1.5  qed (auto intro: inj_onI)
     1.6  
     1.7 +lemma fact_div_fact_le_pow:
     1.8 +  assumes "r \<le> n" shows "fact n div fact (n - r) \<le> n ^ r"
     1.9 +proof -
    1.10 +  have "\<And>r. r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}"
    1.11 +    by (subst setprod_insert[symmetric]) (auto simp: atLeastAtMost_insertL)
    1.12 +  with assms show ?thesis
    1.13 +    by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono)
    1.14 +qed
    1.15 +
    1.16  end