# HG changeset patch
# User huffman
# Date 1231439210 28800
# Node ID 6d10cf26b5dcb507189aa33e65c19d0cc279429c
# Parent  5ef7e97fd9e4aa34ea5649492faa6c35a170f4d2
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1

diff -r 5ef7e97fd9e4 -r 6d10cf26b5dc src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Thu Jan 08 10:07:39 2009 -0800
+++ b/src/HOL/Ring_and_Field.thy	Thu Jan 08 10:26:50 2009 -0800
@@ -295,6 +295,30 @@
 subclass ring_1 ..
 subclass comm_semiring_1_cancel ..
 
+lemma dvd_minus_iff: "x dvd - y \<longleftrightarrow> x dvd y"
+proof
+  assume "x dvd - y"
+  then have "x dvd - 1 * - y" by (rule dvd_mult)
+  then show "x dvd y" by simp
+next
+  assume "x dvd y"
+  then have "x dvd - 1 * y" by (rule dvd_mult)
+  then show "x dvd - y" by simp
+qed
+
+lemma minus_dvd_iff: "- x dvd y \<longleftrightarrow> x dvd y"
+proof
+  assume "- x dvd y"
+  then obtain k where "y = - x * k" ..
+  then have "y = x * - k" by simp
+  then show "x dvd y" ..
+next
+  assume "x dvd y"
+  then obtain k where "y = x * k" ..
+  then have "y = - x * - k" by simp
+  then show "- x dvd y" ..
+qed
+
 end
 
 class ring_no_zero_divisors = ring + no_zero_divisors