--- 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"