added lemma

--- a/src/HOL/Groups_Big.thy	Tue Sep 16 16:04:08 2014 +0200
+++ b/src/HOL/Groups_Big.thy	Tue Sep 16 18:42:33 2014 +0200
@@ -948,6 +948,9 @@
 apply (auto simp add: algebra_simps)
 done
 
+lemma setsum_Suc: "setsum (%x. Suc(f x)) A = setsum f A + card A"
+using setsum.distrib[of f "%_. 1" A] by(simp)
+
 lemma setsum_bounded:
   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
   shows "setsum f A \<le> of_nat (card A) * K"