# HG changeset patch
# User nipkow
# Date 1396797537 -7200
# Node ID 49e95c9ebb59d7581d81eb3a74e25951936482ef
# Parent  96b54a96b1177b14db9c9a26301ffd590704d6d6
made field_simps "more complete"

diff -r 96b54a96b117 -r 49e95c9ebb59 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sat Apr 05 23:56:21 2014 +0200
+++ b/src/HOL/Fields.thy	Sun Apr 06 17:18:57 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)