src/HOL/Rings.thy
changeset 59865 8a20dd967385
parent 59833 ab828c2c5d67
child 59910 815de5506080
     1.1 --- a/src/HOL/Rings.thy	Tue Mar 31 15:01:06 2015 +0100
     1.2 +++ b/src/HOL/Rings.thy	Tue Mar 31 16:48:48 2015 +0100
     1.3 @@ -1260,6 +1260,10 @@
     1.4    "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
     1.5    by (auto simp add: diff_less_eq ac_simps abs_less_iff)
     1.6  
     1.7 +lemma abs_diff_le_iff:
     1.8 +   "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r"
     1.9 +  by (auto simp add: diff_le_eq ac_simps abs_le_iff)
    1.10 +
    1.11  end
    1.12  
    1.13  hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib