added lemma
authorhaftmann
Sun Oct 16 09:31:03 2016 +0200 (2016-10-16)
changeset 64239de5cd9217d4c
parent 64238 b60a9752b6d0
child 64240 eabf80376aab
added lemma
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Rings.thy	Sun Oct 16 09:31:03 2016 +0200
     1.2 +++ b/src/HOL/Rings.thy	Sun Oct 16 09:31:03 2016 +0200
     1.3 @@ -1918,6 +1918,10 @@
     1.4  lemma sgn_less [simp]: "sgn a < 0 \<longleftrightarrow> a < 0"
     1.5    unfolding sgn_if by auto
     1.6  
     1.7 +lemma abs_sgn_eq_1 [simp]:
     1.8 +  "a \<noteq> 0 \<Longrightarrow> \<bar>sgn a\<bar> = 1"
     1.9 +  by (simp add: abs_if)
    1.10 +
    1.11  lemma abs_sgn_eq: "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
    1.12    by (simp add: sgn_if)
    1.13