src/HOL/Groups_Big.thy

--- a/src/HOL/Groups_Big.thy	Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Groups_Big.thy	Wed Apr 10 13:34:55 2019 +0100
@@ -106,6 +106,11 @@
   ultimately show ?thesis by simp
 qed
 
+lemma Int_Diff:
+  assumes "finite A"
+  shows "F g A = F g (A \<inter> B) \<^bold>* F g (A - B)"
+  by (subst subset_diff [where B = "A - B"]) (auto simp:  Diff_Diff_Int assms)
+
 lemma setdiff_irrelevant:
   assumes "finite A"
   shows "F g (A - {x. g x = z}) = F g A"