--- a/src/HOL/Library/Formal_Power_Series.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Fri Nov 13 12:27:13 2015 +0000
@@ -3787,10 +3787,8 @@
lemma binomial_Vandermonde:
"setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n"
using gbinomial_Vandermonde[of "(of_nat a)" "of_nat b" n]
- apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric]
- of_nat_setsum[symmetric] of_nat_add[symmetric])
- apply blast
- done
+ by (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric]
+ of_nat_setsum[symmetric] of_nat_add[symmetric] of_nat_eq_iff)
lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)\<^sup>2) {0..n} = (2 * n) choose n"
using binomial_Vandermonde[of n n n, symmetric]