equal
deleted
inserted
replaced
313 by (intro bexI[of _ "k - i"]) simp_all } |
313 by (intro bexI[of _ "k - i"]) simp_all } |
314 then show "{1..k} = (\<lambda>i. k - i) ` {..<k}" |
314 then show "{1..k} = (\<lambda>i. k - i) ` {..<k}" |
315 by (auto simp: image_iff) |
315 by (auto simp: image_iff) |
316 qed (auto intro: inj_onI) |
316 qed (auto intro: inj_onI) |
317 |
317 |
|
318 lemma fact_div_fact_le_pow: |
|
319 assumes "r \<le> n" shows "fact n div fact (n - r) \<le> n ^ r" |
|
320 proof - |
|
321 have "\<And>r. r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}" |
|
322 by (subst setprod_insert[symmetric]) (auto simp: atLeastAtMost_insertL) |
|
323 with assms show ?thesis |
|
324 by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono) |
|
325 qed |
|
326 |
318 end |
327 end |