src/HOL/Ring_and_Field.thy

 qed
 
 lemma one_dvd [simp]: "1 dvd a"
 by (auto intro!: dvdI)
 
-lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)"
+lemma dvd_mult[simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"
 by (auto intro!: mult_left_commute dvdI elim!: dvdE)
 
-lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)"
+lemma dvd_mult2[simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"
   apply (subst mult_commute)
   apply (erule dvd_mult)
   done
 
 lemma dvd_triv_right [simp]: "a dvd b * a"

 
 lemma dvd_triv_left [simp]: "a dvd a * b"
 by (rule dvd_mult2) (rule dvd_refl)
 
 lemma mult_dvd_mono:
-  assumes ab: "a dvd b"
-    and "cd": "c dvd d"
+  assumes "a dvd b"
+    and "c dvd d"
   shows "a * c dvd b * d"
 proof -
-  from ab obtain b' where "b = a * b'" ..
-  moreover from "cd" obtain d' where "d = c * d'" ..
+  from `a dvd b` obtain b' where "b = a * b'" ..
+  moreover from `c dvd d` obtain d' where "d = c * d'" ..
   ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
   then show ?thesis ..
 qed
 
 lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"

   then obtain k where "y = x * k" ..
   then have "y = - x * - k" by simp
   then show "- x dvd y" ..
 qed
 
-lemma dvd_diff: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
-by (simp add: diff_minus dvd_add dvd_minus_iff)
+lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
+by (simp add: diff_minus dvd_minus_iff)
 
 end
 
 class ring_no_zero_divisors = ring + no_zero_divisors
 begin

   then show "a = b \<or> a = - b"
     by (simp add: right_minus_eq eq_neg_iff_add_eq_0)
 next
   assume "a = b \<or> a = - b"
   then show "a * a = b * b" by auto
+qed
+
+lemma dvd_mult_cancel_right [simp]:
+  "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
+proof -
+  have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
+    unfolding dvd_def by (simp add: mult_ac)
+  also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
+    unfolding dvd_def by simp
+  finally show ?thesis .
+qed
+
+lemma dvd_mult_cancel_left [simp]:
+  "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
+proof -
+  have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
+    unfolding dvd_def by (simp add: mult_ac)
+  also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
+    unfolding dvd_def by simp
+  finally show ?thesis .
 qed
 
 end
 
 class division_ring = ring_1 + inverse +