# HG changeset patch
# User chaieb
# Date 1247668304 -7200
# Node ID 4dc119d4fc8bff1166f0ac1d95bafa27c5bede44
# Parent  adea7a729c7a66ed01bdf8971e12ce92d8673b0d
Moved theorem binomial_symmetric from Formal_Power_Series to here

diff -r adea7a729c7a -r 4dc119d4fc8b src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Wed Jul 15 06:14:25 2009 +0200
+++ b/src/HOL/Library/Binomial.thy	Wed Jul 15 16:31:44 2009 +0200
@@ -459,4 +459,14 @@
   ultimately show ?thesis by (cases k, auto)
 qed
 
+
+lemma binomial_symmetric: assumes kn: "k \<le> n" 
+  shows "n choose k = n choose (n - k)"
+proof-
+  from kn have kn': "n - k \<le> n" by arith
+  from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn']
+  have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp
+  then show ?thesis using kn by simp
+qed
+
 end