diff -r b98f1057da0e -r 10c712405854 src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Tue Aug 06 22:47:44 2024 +0100
+++ b/src/HOL/Analysis/Convex.thy	Wed Aug 07 12:39:09 2024 +0100
@@ -1194,16 +1194,6 @@
 lemma convex_gchoose: "convex_on {k-1..} (\<lambda>x. x gchoose k)"
   by (simp add: gbinomial_prod_rev convex_on_cdiv convex_gchoose_aux)
 
-lemma gbinomial_mono:
-  fixes k::nat and a::real
-  assumes "of_nat k \<le> a" "a \<le> b" shows "a gchoose k \<le> b gchoose k"
-  using assms
-  by (force simp: gbinomial_prod_rev intro!: divide_right_mono prod_mono)
-
-lemma gbinomial_is_prod: "(a gchoose k) = (\<Prod>i<k. (a - of_nat i) / (1 + of_nat i))"
-  unfolding gbinomial_prod_rev
-  by (induction k; simp add: divide_simps)
-
 subsection \<open>Some inequalities: Applications of convexity\<close>
 
 lemma Youngs_inequality_0: