src/HOL/Int.thy
changeset 66886 960509bfd47e
parent 66836 4eb431c3f974
child 66912 a99a7cbf0fb5
     1.1 --- a/src/HOL/Int.thy	Thu Oct 19 17:16:13 2017 +0100
     1.2 +++ b/src/HOL/Int.thy	Fri Oct 20 07:46:10 2017 +0200
     1.3 @@ -552,6 +552,10 @@
     1.4  lemma diff_nat_numeral [simp]: "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
     1.5    by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
     1.6  
     1.7 +lemma nat_abs_triangle_ineq:
     1.8 +  "nat \<bar>k + l\<bar> \<le> nat \<bar>k\<bar> + nat \<bar>l\<bar>"
     1.9 +  by (simp add: nat_add_distrib [symmetric] nat_le_eq_zle abs_triangle_ineq)
    1.10 +
    1.11  lemma nat_of_bool [simp]:
    1.12    "nat (of_bool P) = of_bool P"
    1.13    by auto