# HG changeset patch
# User noschinl
# Date 1324302068 -3600
# Node ID ee70da42e08ab86e839700032ad7f2e9f5f32979
# Parent  6f08f8fe9752a4aee279743d1707679af681bab5
add lemmas

diff -r 6f08f8fe9752 -r ee70da42e08a src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Dec 19 14:41:08 2011 +0100
+++ b/src/HOL/Nat.thy	Mon Dec 19 14:41:08 2011 +0100
@@ -1615,6 +1615,9 @@
 lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
 by arith
 
+lemma Suc_diff_Suc: "n < m \<Longrightarrow> Suc (m - Suc n) = m - n"
+by simp
+
 text{*Lemmas for ex/Factorization*}
 
 lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
diff -r 6f08f8fe9752 -r ee70da42e08a src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Mon Dec 19 14:41:08 2011 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Mon Dec 19 14:41:08 2011 +0100
@@ -349,4 +349,17 @@
   qed
 qed
 
+lemma choose_le_pow:
+  assumes "r \<le> n" shows "n choose r \<le> n ^ r"
+proof -
+  have X: "\<And>r. r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}"
+    by (subst setprod_insert[symmetric]) (auto simp: atLeastAtMost_insertL)
+  have "n choose r \<le> fact n div fact (n - r)"
+    using `r \<le> n` by (simp add: choose_altdef_nat div_le_mono2)
+  also have "\<dots> \<le> n ^ r" using `r \<le> n`
+    by (induct r rule: nat.induct)
+     (auto simp add: fact_div_fact Suc_diff_Suc X One_nat_def mult_le_mono)
+ finally show ?thesis .
+qed
+
 end