# HG changeset patch
# User nipkow
# Date 1410885753 -7200
# Node ID 107341a1594677701d4015cdd86a35028e92b17c
# Parent  2d47c7d10b62e585f6b673b1f0c1d2a220c403eb
added lemma

diff -r 2d47c7d10b62 -r 107341a15946 src/HOL/Groups_Big.thy
--- 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"