# HG changeset patch # User paulson # Date 1414687004 0 # Node ID 09974789e48360ab39533b9b19712354ad56099b # Parent ec9550bd5fd735dddcd6ac38906476a48fc03377 choose_reduce_nat: re-ordered operands diff -r ec9550bd5fd7 -r 09974789e483 src/HOL/Number_Theory/Binomial.thy --- a/src/HOL/Number_Theory/Binomial.thy Thu Oct 30 11:24:53 2014 +0100 +++ b/src/HOL/Number_Theory/Binomial.thy Thu Oct 30 16:36:44 2014 +0000 @@ -32,8 +32,8 @@ lemma choose_reduce_nat: "0 < (n::nat) \ 0 < k \ - (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))" - by (metis Suc_diff_1 binomial.simps(2) add.commute neq0_conv) + (n choose k) = ((n - 1) choose (k - 1)) + ((n - 1) choose k)" + by (metis Suc_diff_1 binomial.simps(2) neq0_conv) lemma binomial_eq_0: "n < k \ n choose k = 0" by (induct n arbitrary: k) auto @@ -524,7 +524,6 @@ using Suc apply auto done - have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) = ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\i\{0\nat..Suc h}. a - of_nat i)" apply (simp add: Suc field_simps del: fact_Suc) @@ -547,6 +546,10 @@ finally show ?thesis by (simp del: fact_Suc) qed +lemma gbinomial_reduce_nat: + "0 < k \ (a::'a::field_char_0) gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)" +by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc) + lemma binomial_symmetric: assumes kn: "k \ n"