src/HOL/Library/Formal_Power_Series.thy
changeset 61649 268d88ec9087
parent 61610 4f54d2759a0b
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -3787,10 +3787,8 @@
     1.4  lemma binomial_Vandermonde:
     1.5    "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n"
     1.6    using gbinomial_Vandermonde[of "(of_nat a)" "of_nat b" n]
     1.7 -  apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric]
     1.8 -                    of_nat_setsum[symmetric] of_nat_add[symmetric])
     1.9 -  apply blast
    1.10 -  done
    1.11 +  by (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric]
    1.12 +                 of_nat_setsum[symmetric] of_nat_add[symmetric] of_nat_eq_iff)
    1.13  
    1.14  lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)\<^sup>2) {0..n} = (2 * n) choose n"
    1.15    using binomial_Vandermonde[of n n n, symmetric]