# HG changeset patch
# User nipkow
# Date 1396797548 -7200
# Node ID 681717041f550de2f71fbaa3d462528537fdc9ab
# Parent  aab984137bcdd3c60efb0802872247a55ad19e14# Parent  49e95c9ebb59d7581d81eb3a74e25951936482ef
merged

diff -r aab984137bcd -r 681717041f55 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sun Apr 06 17:09:32 2014 +0200
+++ b/src/HOL/Fields.thy	Sun Apr 06 17:19:08 2014 +0200
@@ -174,6 +174,14 @@
   finally show ?thesis .
 qed
 
+lemma nonzero_neg_divide_eq_eq[field_simps]:
+  "b \<noteq> 0 \<Longrightarrow> -(a/b) = c \<longleftrightarrow> -a = c*b"
+using nonzero_divide_eq_eq[of b "-a" c] by (simp add: divide_minus_left)
+
+lemma nonzero_neg_divide_eq_eq2[field_simps]:
+  "b \<noteq> 0 \<Longrightarrow> c = -(a/b) \<longleftrightarrow> c*b = -a"
+using nonzero_neg_divide_eq_eq[of b a c] by auto
+
 lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
   by (simp add: divide_inverse mult_assoc)