1.1 --- a/src/HOL/Groups.thy	Tue May 13 11:35:47 2014 +0200
     1.2 +++ b/src/HOL/Groups.thy	Tue May 13 11:35:51 2014 +0200
     1.3 @@ -1036,6 +1036,24 @@
     1.4    "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
     1.5    by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
     1.6  
     1.7 +lemma diff_mono: "a \<le> b \<Longrightarrow> d \<le> c \<Longrightarrow> a - c \<le> b - d"
     1.8 +  by (simp add: field_simps add_mono)
     1.9 +
    1.10 +lemma diff_left_mono: "b \<le> a \<Longrightarrow> c - a \<le> c - b"
    1.11 +  by (simp add: field_simps)
    1.12 +
    1.13 +lemma diff_right_mono: "a \<le> b \<Longrightarrow> a - c \<le> b - c"
    1.14 +  by (simp add: field_simps)
    1.15 +
    1.16 +lemma diff_strict_mono: "a < b \<Longrightarrow> d < c \<Longrightarrow> a - c < b - d"
    1.17 +  by (simp add: field_simps add_strict_mono)
    1.18 +
    1.19 +lemma diff_strict_left_mono: "b < a \<Longrightarrow> c - a < c - b"
    1.20 +  by (simp add: field_simps)
    1.21 +
    1.22 +lemma diff_strict_right_mono: "a < b \<Longrightarrow> a - c < b - c"
    1.23 +  by (simp add: field_simps)
    1.24 +
    1.25  end
    1.26  
    1.27  ML_file "Tools/group_cancel.ML"