src/HOL/Groups.thy
changeset 63878 e26c7f58d78e
parent 63680 6e1e8b5abbfa
child 64290 fb5c74a58796
     1.1 --- a/src/HOL/Groups.thy	Thu Sep 15 11:44:05 2016 +0200
     1.2 +++ b/src/HOL/Groups.thy	Thu Sep 15 10:40:10 2016 +0200
     1.3 @@ -1369,11 +1369,14 @@
     1.4  subclass ordered_comm_monoid_add
     1.5    proof qed (auto simp: le_iff_add add_ac)
     1.6  
     1.7 -lemma add_eq_0_iff_both_eq_0: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
     1.8 +lemma gr_implies_not_zero: "m < n \<Longrightarrow> n \<noteq> 0"
     1.9 +  by auto
    1.10 +
    1.11 +lemma add_eq_0_iff_both_eq_0[simp]: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
    1.12    by (intro add_nonneg_eq_0_iff zero_le)
    1.13  
    1.14 -lemma gr_implies_not_zero: "m < n \<Longrightarrow> n \<noteq> 0"
    1.15 -  using add_eq_0_iff_both_eq_0[of m] by (auto simp: le_iff_add less_le)
    1.16 +lemma zero_eq_add_iff_both_eq_0[simp]: "0 = x + y \<longleftrightarrow> x = 0 \<and> y = 0"
    1.17 +  using add_eq_0_iff_both_eq_0[of x y] unfolding eq_commute[of 0] .
    1.18  
    1.19  lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero
    1.20    \<comment> \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>