--- a/src/HOL/Fun.thy Wed Feb 19 11:11:14 2025 +0100
+++ b/src/HOL/Fun.thy Fri Feb 21 18:46:59 2025 +0100
@@ -816,18 +816,12 @@
"(\<lambda>x. x - a) ` (s \<inter> t) = ((\<lambda>x. x - a) ` s) \<inter> ((\<lambda>x. x - a) ` t)"
by(rule image_Int)(simp add: inj_on_def diff_eq_eq)
-end
-
-(* TODO: prove in group_add *)
-context ab_group_add
-begin
-
lemma translation_Compl:
"(+) a ` (- t) = - ((+) a ` t)"
proof (rule set_eqI)
fix b
show "b \<in> (+) a ` (- t) \<longleftrightarrow> b \<in> - (+) a ` t"
- by (auto simp: image_iff algebra_simps intro!: bexI [of _ "b - a"])
+ by (auto simp: image_iff algebra_simps intro!: bexI [of _ "- a + b"])
qed
end