src/HOL/Rings.thy
changeset 62608 19f87fa0cfcb
parent 62481 b5d8e57826df
child 62626 de25474ce728
     1.1 --- a/src/HOL/Rings.thy	Sun Mar 13 09:06:50 2016 +0100
     1.2 +++ b/src/HOL/Rings.thy	Sun Mar 13 10:22:46 2016 +0100
     1.3 @@ -1349,6 +1349,38 @@
     1.4    "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
     1.5  by (force simp add: mult_right_mono not_le [symmetric])
     1.6  
     1.7 +lemma less_eq_add_cancel_left_greater_eq_zero [simp]:
     1.8 +  "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
     1.9 +  using add_le_cancel_left [of a 0 b] by simp
    1.10 +
    1.11 +lemma less_eq_add_cancel_left_less_eq_zero [simp]:
    1.12 +  "a + b \<le> a \<longleftrightarrow> b \<le> 0"
    1.13 +  using add_le_cancel_left [of a b 0] by simp
    1.14 +
    1.15 +lemma less_eq_add_cancel_right_greater_eq_zero [simp]:
    1.16 +  "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
    1.17 +  using add_le_cancel_right [of 0 a b] by simp
    1.18 +
    1.19 +lemma less_eq_add_cancel_right_less_eq_zero [simp]:
    1.20 +  "b + a \<le> a \<longleftrightarrow> b \<le> 0"
    1.21 +  using add_le_cancel_right [of b a 0] by simp
    1.22 +
    1.23 +lemma less_add_cancel_left_greater_zero [simp]:
    1.24 +  "a < a + b \<longleftrightarrow> 0 < b"
    1.25 +  using add_less_cancel_left [of a 0 b] by simp
    1.26 +
    1.27 +lemma less_add_cancel_left_less_zero [simp]:
    1.28 +  "a + b < a \<longleftrightarrow> b < 0"
    1.29 +  using add_less_cancel_left [of a b 0] by simp
    1.30 +
    1.31 +lemma less_add_cancel_right_greater_zero [simp]:
    1.32 +  "a < b + a \<longleftrightarrow> 0 < b"
    1.33 +  using add_less_cancel_right [of 0 a b] by simp
    1.34 +
    1.35 +lemma less_add_cancel_right_less_zero [simp]:
    1.36 +  "b + a < a \<longleftrightarrow> b < 0"
    1.37 +  using add_less_cancel_right [of b a 0] by simp
    1.38 +
    1.39  end
    1.40  
    1.41  class linordered_semiring_1 = linordered_semiring + semiring_1