--- a/src/HOL/Big_Operators.thy Thu Oct 31 16:54:22 2013 +0100
+++ b/src/HOL/Big_Operators.thy Fri Nov 01 18:51:14 2013 +0100
@@ -696,11 +696,7 @@
lemma setsum_subtractf:
"setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
setsum f A - setsum g A"
-proof (cases "finite A")
- case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
-next
- case False thus ?thesis by simp
-qed
+ using setsum_addf [of f "- g" A] by (simp add: setsum_negf)
lemma setsum_nonneg:
assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"