author noschinl Mon Dec 19 14:41:08 2011 +0100 (2011-12-19) changeset 45933 ee70da42e08a parent 45932 6f08f8fe9752 child 45934 9321cd2572fe
 src/HOL/Nat.thy file | annotate | diff | revisions src/HOL/Number_Theory/Binomial.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Nat.thy	Mon Dec 19 14:41:08 2011 +0100
1.2 +++ b/src/HOL/Nat.thy	Mon Dec 19 14:41:08 2011 +0100
1.3 @@ -1615,6 +1615,9 @@
1.4  lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
1.5  by arith
1.6
1.7 +lemma Suc_diff_Suc: "n < m \<Longrightarrow> Suc (m - Suc n) = m - n"
1.8 +by simp
1.9 +
1.10  text{*Lemmas for ex/Factorization*}
1.11
1.12  lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
```
```     2.1 --- a/src/HOL/Number_Theory/Binomial.thy	Mon Dec 19 14:41:08 2011 +0100
2.2 +++ b/src/HOL/Number_Theory/Binomial.thy	Mon Dec 19 14:41:08 2011 +0100
2.3 @@ -349,4 +349,17 @@
2.4    qed
2.5  qed
2.6
2.7 +lemma choose_le_pow:
2.8 +  assumes "r \<le> n" shows "n choose r \<le> n ^ r"
2.9 +proof -
2.10 +  have X: "\<And>r. r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}"
2.11 +    by (subst setprod_insert[symmetric]) (auto simp: atLeastAtMost_insertL)
2.12 +  have "n choose r \<le> fact n div fact (n - r)"
2.13 +    using `r \<le> n` by (simp add: choose_altdef_nat div_le_mono2)
2.14 +  also have "\<dots> \<le> n ^ r" using `r \<le> n`
2.15 +    by (induct r rule: nat.induct)
2.16 +     (auto simp add: fact_div_fact Suc_diff_Suc X One_nat_def mult_le_mono)
2.17 + finally show ?thesis .
2.18 +qed
2.19 +
2.20  end
```