# HG changeset patch
# User wenzelm
# Date 1723056991 -7200
# Node ID cbfc1058df7c9a53edf9e51aa5bbe720beb95b7b
# Parent  10c712405854bb19cc2b00f0dbeb324ba155648f# Parent  e8a47adda46b8046ab6d2fbe4dce88d8d9f2f06f
merged

diff -r e8a47adda46b -r cbfc1058df7c src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Wed Aug 07 20:15:03 2024 +0200
+++ b/src/HOL/Analysis/Convex.thy	Wed Aug 07 20:56:31 2024 +0200
@@ -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:
diff -r e8a47adda46b -r cbfc1058df7c src/HOL/Binomial_Plus.thy
--- a/src/HOL/Binomial_Plus.thy	Wed Aug 07 20:15:03 2024 +0200
+++ b/src/HOL/Binomial_Plus.thy	Wed Aug 07 20:56:31 2024 +0200
@@ -178,6 +178,12 @@
 corollary gbinomial_eq_0: "0 \<le> a \<Longrightarrow> a < int k \<Longrightarrow> a gchoose k = 0"
   by (metis nat_eq_iff2 nat_less_iff gbinomial_eq_0_int)
 
+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 int_binomial: "int (n choose k) = (int n) gchoose k"
 proof (cases "k \<le> n")
   case True