diff -r 85ed00c1fe7c -r 340738057c8c src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Groups.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -1203,6 +1203,16 @@
   thus "\<bar>a\<bar> \<le> 0" by simp
 qed
 
+lemma abs_le_self_iff [simp]: "\<bar>a\<bar> \<le> a \<longleftrightarrow> 0 \<le> a"
+proof -
+  have "\<forall>a. (0::'a) \<le> \<bar>a\<bar>"
+    using abs_ge_zero by blast
+  then have "\<bar>a\<bar> \<le> a \<Longrightarrow> 0 \<le> a"
+    using order.trans by blast
+  then show ?thesis
+    using abs_of_nonneg eq_refl by blast
+qed
+
 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
 by (simp add: less_le)