# HG changeset patch
# User huffman
# Date 1234659078 28800
# Node ID c9ced4f54e820fe889ebabbb0a6788f72eb43bc9
# Parent  89eadbe71e975ba0dbb3728217037dfed2bdd1c5
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup

diff -r 89eadbe71e97 -r c9ced4f54e82 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Sat Feb 14 15:30:26 2009 -0800
+++ b/src/HOL/Library/Formal_Power_Series.thy	Sat Feb 14 16:51:18 2009 -0800
@@ -691,16 +691,6 @@
   by (simp_all add: fps_power_def)
 end
 
-lemma eq_neg_iff_add_eq_0: "(a::'a::ring) = -b \<longleftrightarrow> a + b = 0"
-proof-
-  {assume "a = -b" hence "b + a = b + -b" by simp
-    hence "a + b = 0" by (simp add: ring_simps)}
-  moreover
-  {assume "a + b = 0" hence "a + b - b = -b" by simp
-    hence "a = -b" by simp}
-  ultimately show ?thesis by blast
-qed
-
 lemma fps_square_eq_iff: "(a:: 'a::idom fps)^ 2 = b^2  \<longleftrightarrow> (a = b \<or> a = -b)"
 proof-
   {assume "a = b \<or> a = -b" hence "a^2 = b^2" by auto}
diff -r 89eadbe71e97 -r c9ced4f54e82 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Sat Feb 14 15:30:26 2009 -0800
+++ b/src/HOL/OrderedGroup.thy	Sat Feb 14 16:51:18 2009 -0800
@@ -254,6 +254,16 @@
 
 declare diff_minus[symmetric, algebra_simps]
 
+lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0"
+proof
+  assume "a = - b" then show "a + b = 0" by simp
+next
+  assume "a + b = 0"
+  moreover have "a + (b + - b) = (a + b) + - b"
+    by (simp only: add_assoc)
+  ultimately show "a = - b" by simp
+qed
+
 end
 
 class ab_group_add = minus + uminus + comm_monoid_add +