src/HOL/Rings.thy
changeset 62626 de25474ce728
parent 62608 19f87fa0cfcb
child 63040 eb4ddd18d635
     1.1 --- a/src/HOL/Rings.thy	Tue Mar 15 14:08:25 2016 +0000
     1.2 +++ b/src/HOL/Rings.thy	Wed Mar 16 13:57:06 2016 +0000
     1.3 @@ -2088,6 +2088,9 @@
     1.4     "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r"
     1.5    by (auto simp add: diff_le_eq ac_simps abs_le_iff)
     1.6  
     1.7 +lemma abs_add_one_gt_zero: "0 < 1 + \<bar>x\<bar>"
     1.8 +  by (force simp: abs_if not_less intro: zero_less_one add_strict_increasing less_trans)
     1.9 +
    1.10  end
    1.11  
    1.12  subsection \<open>Dioids\<close>