# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1414774914 0
# Node ID e16712bb1d413660ed44e8d5cb03cfcedccefa6d
# Parent  f4bb3068d819f12a719074e7466e4b713e4a23a1
Some comments and a new version of a result

diff -r f4bb3068d819 -r e16712bb1d41 src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Thu Oct 30 23:14:11 2014 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Fri Oct 31 17:01:54 2014 +0000
@@ -58,22 +58,25 @@
 lemma zero_less_binomial_iff [simp]: "n choose k > 0 \<longleftrightarrow> k \<le> n"
   by (metis binomial_eq_0_iff not_less0 not_less zero_less_binomial)
 
-(*Might be more useful if re-oriented*)
 lemma Suc_times_binomial_eq:
   "k \<le> n \<Longrightarrow> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
-  apply (induct n arbitrary: k)
-   apply (simp add: binomial.simps)
-   apply (case_tac k)
-  apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0)
+  apply (induct n arbitrary: k, simp)
+  apply (case_tac k)
+   apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0)
   done
 
-text{*This is the well-known version, but it's harder to use because of the
+text{*The absorption property*}
+lemma Suc_times_binomial:
+  "k \<le> n \<Longrightarrow> (Suc n choose Suc k) * Suc k = Suc n * (n choose k)"
+  by (rule Suc_times_binomial_eq [symmetric])
+
+text{*This is the well-known version of absorption, but it's harder to use because of the
   need to reason about division.*}
 lemma binomial_Suc_Suc_eq_times:
     "k \<le> n \<Longrightarrow> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
   by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right)
 
-text{*Another version, with -1 instead of Suc.*}
+text{*Another version of absorption, with -1 instead of Suc.*}
 lemma times_binomial_minus1_eq:
   "k \<le> n \<Longrightarrow> 0 < k \<Longrightarrow> (n choose k) * k = n * ((n - 1) choose (k - 1))"
   using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"]
@@ -201,6 +204,7 @@
   shows "(\<And>k. m \<le> k \<Longrightarrow> k \<le> n \<Longrightarrow> g k = f (m + n - k)) \<Longrightarrow> (\<Sum>k=m..n. f k) = (\<Sum>k=m..n. g k)"
   by (rule setsum.reindex_bij_witness[where i="\<lambda>k. m+n-k" and j="\<lambda>k. m+n-k"]) auto
 
+text{*NW diagonal sum property*}
 lemma sum_choose_diagonal:
   assumes "m\<le>n" shows "(\<Sum>k=0..m. (n-k) choose (m-k)) = Suc n choose m"
 proof -