src/HOL/Rings.thy
changeset 60615 e5fa1d5d3952
parent 60570 7ed2cde6806d
child 60685 cb21b7022b00
     1.1 --- a/src/HOL/Rings.thy	Mon Jun 29 13:49:21 2015 +0200
     1.2 +++ b/src/HOL/Rings.thy	Tue Jun 30 13:56:16 2015 +0100
     1.3 @@ -1362,7 +1362,30 @@
     1.4  
     1.5  lemma add_diff_inverse: "~ a<b \<Longrightarrow> b + (a - b) = a"
     1.6    by simp
     1.7 -  
     1.8 +
     1.9 +lemma add_le_imp_le_diff: 
    1.10 +  shows "i + k \<le> n \<Longrightarrow> i \<le> n - k"
    1.11 +  apply (subst add_le_cancel_right [where c=k, symmetric])
    1.12 +  apply (frule le_add_diff_inverse2)
    1.13 +  apply (simp only: add.assoc [symmetric])
    1.14 +  using add_implies_diff by fastforce
    1.15 +
    1.16 +lemma add_le_add_imp_diff_le: 
    1.17 +  assumes a1: "i + k \<le> n"
    1.18 +      and a2: "n \<le> j + k"
    1.19 +  shows "\<lbrakk>i + k \<le> n; n \<le> j + k\<rbrakk> \<Longrightarrow> n - k \<le> j"
    1.20 +proof -
    1.21 +  have "n - (i + k) + (i + k) = n"
    1.22 +    using a1 by simp
    1.23 +  moreover have "n - k = n - k - i + i"
    1.24 +    using a1 by (simp add: add_le_imp_le_diff)
    1.25 +  ultimately show ?thesis
    1.26 +    using a2
    1.27 +    apply (simp add: add.assoc [symmetric])
    1.28 +    apply (rule add_le_imp_le_diff [of _ k "j+k", simplified add_diff_cancel_right'])
    1.29 +    by (simp add: add.commute diff_diff_add)
    1.30 +qed
    1.31 +
    1.32  lemma pos_add_strict:
    1.33    shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
    1.34    using add_strict_mono [of 0 a b c] by simp