src/HOL/Binomial.thy

     by (auto intro: prod_zero)
   with \<open>n < k\<close> show ?thesis
     by (simp add: binomial_eq_0 gbinomial_prod_rev prod_zero)
 next
   case True
-  then have "inj_on (op - n) {0..<k}"
-    by (auto intro: inj_onI)
-  then have "\<Prod>(op - n ` {0..<k}) = prod (op - n) {0..<k}"
-    by (auto dest: prod.reindex)
-  also have "op - n ` {0..<k} = {Suc (n - k)..n}"
-    using True by (auto simp add: image_def Bex_def) presburger  (* FIXME slow *)
-  finally have *: "prod (\<lambda>q. n - q) {0..<k} = \<Prod>{Suc (n - k)..n}" ..
+  from True have *: "prod (op - n) {0..<k} = \<Prod>{Suc (n - k)..n}"
+    by (intro prod.reindex_bij_witness[of _ "\<lambda>i. n - i" "\<lambda>i. n - i"]) auto
   from True have "n choose k = fact n div (fact k * fact (n - k))"
     by (rule binomial_fact')
   with * show ?thesis
     by (simp add: gbinomial_prod_rev mult.commute [of "fact k"] div_mult2_eq fact_div_fact)
 qed

   have fin_B: "finite ?B"
     by (intro finite_subset[where ?A = "?B" and ?B = "{xs. size xs = m \<and> set xs \<subseteq> {0..<N}}"])
       (auto simp: member_le_sum_list_nat less_Suc_eq_le fin)
   have uni: "?C = ?A' \<union> ?B'"
     by auto
-  have disj: "?A' \<inter> ?B' = {}"
-    by auto
+  have disj: "?A' \<inter> ?B' = {}" by blast
   have "card ?C = card(?A' \<union> ?B')"
     using uni by simp
   also have "\<dots> = card ?A + card ?B"
     using card_Un_disjoint[OF _ _ disj] bij_betw_finite[OF f] bij_betw_finite[OF g]
       bij_betw_same_card[OF f] bij_betw_same_card[OF g] fin_A fin_B

     then show ?case
       using card_length_sum_list_rec[OF Suc.prems] by auto
   qed
 qed
 
+lemma card_disjoint_shuffle: 
+  assumes "set xs \<inter> set ys = {}"
+  shows   "card (shuffle xs ys) = (length xs + length ys) choose length xs"
+using assms
+proof (induction xs ys rule: shuffle.induct)
+  case (3 x xs y ys)
+  have "shuffle (x # xs) (y # ys) = op # x ` shuffle xs (y # ys) \<union> op # y ` shuffle (x # xs) ys"
+    by (rule shuffle.simps)
+  also have "card \<dots> = card (op # x ` shuffle xs (y # ys)) + card (op # y ` shuffle (x # xs) ys)"
+    by (rule card_Un_disjoint) (insert "3.prems", auto)
+  also have "card (op # x ` shuffle xs (y # ys)) = card (shuffle xs (y # ys))"
+    by (rule card_image) auto
+  also have "\<dots> = (length xs + length (y # ys)) choose length xs"
+    using "3.prems" by (intro "3.IH") auto
+  also have "card (op # y ` shuffle (x # xs) ys) = card (shuffle (x # xs) ys)"
+    by (rule card_image) auto
+  also have "\<dots> = (length (x # xs) + length ys) choose length (x # xs)"
+    using "3.prems" by (intro "3.IH") auto
+  also have "length xs + length (y # ys) choose length xs + \<dots> = 
+               (length (x # xs) + length (y # ys)) choose length (x # xs)" by simp
+  finally show ?case .
+qed auto
+
 lemma Suc_times_binomial_add: "Suc a * (Suc (a + b) choose Suc a) = Suc b * (Suc (a + b) choose a)"
   \<comment> \<open>by Lukas Bulwahn\<close>
 proof -
   have dvd: "Suc a * (fact a * fact b) dvd fact (Suc (a + b))" for a b
     using fact_fact_dvd_fact[of "Suc a" "b", where 'a=nat]