# HG changeset patch
# User haftmann
# Date 1476603063 -7200
# Node ID de5cd9217d4c929b09e393cdc9637baf5f250b66
# Parent  b60a9752b6d097412291f67739ed1822c43b8111
added lemma

diff -r b60a9752b6d0 -r de5cd9217d4c src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Rings.thy	Sun Oct 16 09:31:03 2016 +0200
@@ -1918,6 +1918,10 @@
 lemma sgn_less [simp]: "sgn a < 0 \<longleftrightarrow> a < 0"
   unfolding sgn_if by auto
 
+lemma abs_sgn_eq_1 [simp]:
+  "a \<noteq> 0 \<Longrightarrow> \<bar>sgn a\<bar> = 1"
+  by (simp add: abs_if)
+
 lemma abs_sgn_eq: "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
   by (simp add: sgn_if)