src/HOL/Groups.thy

--- a/src/HOL/Groups.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Groups.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -999,6 +999,9 @@
 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_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
 by (auto simp add: le_less diff_less_eq )