diff -r b0215440311d -r 3842556b757c src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Sun Aug 14 18:38:40 2022 +0200
+++ b/src/HOL/Binomial.thy	Sun Aug 14 23:51:47 2022 +0100
@@ -1045,17 +1045,11 @@
     by (simp add: binomial_altdef_nat)
   also have "... = fact (m + r + k) * fact (m + k) div
                  (fact (m + k) * fact (m + r - m) * (fact k * fact m))"
-    apply (subst div_mult_div_if_dvd)
-      apply (auto simp: algebra_simps fact_fact_dvd_fact)
-    apply (metis add.assoc add.commute fact_fact_dvd_fact)
-    done
+    by (metis add_implies_diff add_le_mono1 choose_dvd diff_cancel2 div_mult_div_if_dvd le_add1 le_add2)
   also have "\<dots> = fact (m + r + k) div (fact r * (fact k * fact m))"
     by (auto simp: algebra_simps fact_fact_dvd_fact)
   also have "\<dots> = (fact (m + r + k) * fact (m + r)) div (fact r * (fact k * fact m) * fact (m + r))"
-    apply (subst div_mult_div_if_dvd [symmetric])
-    apply (auto simp add: algebra_simps)
-    apply (metis fact_fact_dvd_fact dvd_trans nat_mult_dvd_cancel_disj)
-    done
+    by simp
   also have "\<dots> =
       (fact (m + r + k) div (fact k * fact (m + r)) * (fact (m + r) div (fact r * fact m)))"
     by (auto simp: div_mult_div_if_dvd fact_fact_dvd_fact algebra_simps)
@@ -1068,6 +1062,26 @@
   "k \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> (n choose m) * (m choose k) = (n choose k) * ((n - k) choose (m - k))"
   using choose_mult_lemma [of "m-k" "n-m" k] by simp
 
+lemma of_nat_binomial_eq_mult_binomial_Suc:
+  assumes "k \<le> n"
+  shows "(of_nat :: (nat \<Rightarrow> ('a :: field_char_0))) (n choose k) = of_nat (n + 1 - k) / of_nat (n + 1) * of_nat (Suc n choose k)"
+proof (cases k)
+  case 0 then show ?thesis by simp
+next
+  case (Suc l)
+  have "of_nat (n + 1) * (\<Prod>i=0..<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
+    using prod.atLeast0_lessThan_Suc [where ?'a = 'a, symmetric, of "\<lambda>i. of_nat (Suc n - i)" k]
+    by (simp add: ac_simps prod.atLeast0_lessThan_Suc_shift del: prod.op_ivl_Suc)
+  also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (Suc n - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
+    by (simp add: Suc atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
+  also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
+    by (simp only: Suc_eq_plus1)
+  finally have "(\<Prod>i=0..<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) / of_nat (n + 1) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
+    by (simp add: field_simps)
+  with assms show ?thesis
+    by (simp add: binomial_altdef_of_nat prod_dividef)
+qed
+
 
 subsection \<open>More on Binomial Coefficients\<close>