# HG changeset patch
# User bulwahn
# Date 1516459815 -3600
# Node ID 14d3163588aeb39903ae39309ea37130f3b9613d
# Parent  056be95db7033ce129cdb5ab557bdf9abd413d3b
add lemma on lists from Falling_Factorial_Sum entry

diff -r 056be95db703 -r 14d3163588ae src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jan 19 20:11:14 2018 +0100
+++ b/src/HOL/List.thy	Sat Jan 20 15:50:15 2018 +0100
@@ -4864,6 +4864,16 @@
   finally show ?thesis by simp
 qed
 
+lemma finite_lists_distinct_length_eq [intro]:
+  assumes "finite A"
+  shows "finite {xs. length xs = n \<and> distinct xs \<and> set xs \<subseteq> A}" (is "finite ?S")
+proof -
+  have "finite {xs. set xs \<subseteq> A \<and> length xs = n}"
+    using \<open>finite A\<close> by (rule finite_lists_length_eq)
+  moreover have "?S \<subseteq> {xs. set xs \<subseteq> A \<and> length xs = n}" by auto
+  ultimately show ?thesis using finite_subset by auto
+qed
+
 lemma card_lists_distinct_length_eq:
   assumes "finite A" "k \<le> card A"
   shows "card {xs. length xs = k \<and> distinct xs \<and> set xs \<subseteq> A} = \<Prod>{card A - k + 1 .. card A}"