--- a/src/HOL/Groups.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Groups.thy Wed Feb 17 21:51:57 2016 +0100
@@ -999,14 +999,17 @@
apply (simp add: algebra_simps)
done
-lemma diff_gt_0_iff_gt [simp]: "a - b > 0 \<longleftrightarrow> a > b"
-by (simp add: less_diff_eq)
+lemma diff_gt_0_iff_gt [simp]:
+ "a - b > 0 \<longleftrightarrow> a > b"
+ by (simp add: less_diff_eq)
-lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
-by (auto simp add: le_less diff_less_eq )
+lemma diff_le_eq [algebra_simps, field_simps]:
+ "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
+ by (auto simp add: le_less diff_less_eq )
-lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
-by (auto simp add: le_less less_diff_eq)
+lemma le_diff_eq [algebra_simps, field_simps]:
+ "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
+ by (auto simp add: le_less less_diff_eq)
lemma diff_le_0_iff_le [simp]:
"a - b \<le> 0 \<longleftrightarrow> a \<le> b"
@@ -1014,6 +1017,10 @@
lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
+lemma diff_ge_0_iff_ge [simp]:
+ "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
+ by (simp add: le_diff_eq)
+
lemma diff_eq_diff_less:
"a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])