diff -r dafb3d343cd6 -r 9cde97e471df src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Tue Feb 06 18:08:43 2024 +0000
+++ b/src/HOL/Binomial.thy	Wed Feb 07 22:39:42 2024 +0000
@@ -21,6 +21,15 @@
 definition binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat"  (infixl "choose" 65)
   where "n choose k = card {K\<in>Pow {0..<n}. card K = k}"
 
+lemma binomial_mono:
+  assumes "m \<le> n" shows "m choose k \<le> n choose k"
+proof -
+  have "{K. K \<subseteq> {0..<m} \<and> card K = k} \<subseteq> {K. K \<subseteq> {0..<n} \<and> card K = k}"
+    using assms by auto
+  then show ?thesis
+    by (simp add: binomial_def card_mono)
+qed
+
 theorem n_subsets:
   assumes "finite A"
   shows "card {B. B \<subseteq> A \<and> card B = k} = card A choose k"