# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1723030749 -3600
# Node ID 10c712405854bb19cc2b00f0dbeb324ba155648f
# Parent  b98f1057da0edd342f4b2a9836cd14e64aff2a43
Rearranged a couple of theorems

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:
diff -r b98f1057da0e -r 10c712405854 src/HOL/Binomial_Plus.thy
--- a/src/HOL/Binomial_Plus.thy	Tue Aug 06 22:47:44 2024 +0100
+++ b/src/HOL/Binomial_Plus.thy	Wed Aug 07 12:39:09 2024 +0100
@@ -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