src/HOL/OrderedGroup.thy
changeset 29914 c9ced4f54e82
parent 29904 856f16a3b436
child 30629 5cd9b19edef3
     1.1 --- a/src/HOL/OrderedGroup.thy	Sat Feb 14 15:30:26 2009 -0800
     1.2 +++ b/src/HOL/OrderedGroup.thy	Sat Feb 14 16:51:18 2009 -0800
     1.3 @@ -254,6 +254,16 @@
     1.4  
     1.5  declare diff_minus[symmetric, algebra_simps]
     1.6  
     1.7 +lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0"
     1.8 +proof
     1.9 +  assume "a = - b" then show "a + b = 0" by simp
    1.10 +next
    1.11 +  assume "a + b = 0"
    1.12 +  moreover have "a + (b + - b) = (a + b) + - b"
    1.13 +    by (simp only: add_assoc)
    1.14 +  ultimately show "a = - b" by simp
    1.15 +qed
    1.16 +
    1.17  end
    1.18  
    1.19  class ab_group_add = minus + uminus + comm_monoid_add +