# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1473946435 -3600
# Node ID 729accd056ad9800b40c74d8e53dd95e3568166d
# Parent  15bbf6360339dc4c89837b9a068b2991d4a4d67f# Parent  e26c7f58d78e7f8562b8cf957e0f5fcd755b814a
Merge

diff -r 15bbf6360339 -r 729accd056ad src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Thu Sep 15 14:14:49 2016 +0100
+++ b/src/HOL/Groups.thy	Thu Sep 15 14:33:55 2016 +0100
@@ -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>