--- a/src/HOL/Rings.thy Tue Apr 15 15:17:25 2025 +0200
+++ b/src/HOL/Rings.thy Tue Apr 15 17:38:20 2025 +0200
@@ -422,6 +422,15 @@
then show "- x dvd y" ..
qed
+lemma dvd_diff_right_iff:
+ assumes "a dvd b"
+ shows "a dvd b - c \<longleftrightarrow> a dvd c" (is "?P \<longleftrightarrow> ?Q")
+ using dvd_add_right_iff[of a b "-c"] assms by auto
+
+lemma dvd_diff_left_iff:
+ shows "a dvd c \<Longrightarrow> a dvd b - c \<longleftrightarrow> a dvd b"
+ using dvd_add_left_iff[of a "-c" b] by auto
+
lemma dvd_diff [simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
using dvd_add [of x y "- z"] by simp