diff -r 06350a8745c9 -r 362d750f5788 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Aug 01 14:07:34 2024 +0200
+++ b/src/HOL/Presburger.thy	Fri Aug 02 18:25:18 2024 +0200
@@ -241,7 +241,7 @@
 next
   assume d: "d dvd D"
   {fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x + D) + t"
-      by (clarsimp simp add: dvd_def,erule_tac x= "ka - k" in allE,simp add: algebra_simps)}
+      using dvd_add_left_iff[OF d, of "x+t"] by (simp add: algebra_simps)}
   thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x + D) + t)" by auto
 qed blast