# HG changeset patch
# User hoelzl
# Date 1473928810 -7200
# Node ID e26c7f58d78e7f8562b8cf957e0f5fcd755b814a
# Parent  b4051d3f4e94a9ef786679b0193a84f9e256bbd3
add add_eq_0_iff_both_eq_0 and zero_eq_add_iff_both_eq_0 to simp set

diff -r b4051d3f4e94 -r e26c7f58d78e src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Thu Sep 15 11:44:05 2016 +0200
+++ b/src/HOL/Groups.thy	Thu Sep 15 10:40:10 2016 +0200
@@ -1369,11 +1369,14 @@
 subclass ordered_comm_monoid_add
   proof qed (auto simp: le_iff_add add_ac)
 
-lemma add_eq_0_iff_both_eq_0: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
+lemma gr_implies_not_zero: "m < n \<Longrightarrow> n \<noteq> 0"
+  by auto
+
+lemma add_eq_0_iff_both_eq_0[simp]: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   by (intro add_nonneg_eq_0_iff zero_le)
 
-lemma gr_implies_not_zero: "m < n \<Longrightarrow> n \<noteq> 0"
-  using add_eq_0_iff_both_eq_0[of m] by (auto simp: le_iff_add less_le)
+lemma zero_eq_add_iff_both_eq_0[simp]: "0 = x + y \<longleftrightarrow> x = 0 \<and> y = 0"
+  using add_eq_0_iff_both_eq_0[of x y] unfolding eq_commute[of 0] .
 
 lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero
   \<comment> \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>