src/HOL/Groups.thy
changeset 61762 d50b993b4fb9
parent 61605 1bf7b186542e
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Groups.thy	Mon Nov 30 14:24:51 2015 +0100
     1.2 +++ b/src/HOL/Groups.thy	Tue Dec 01 14:09:10 2015 +0000
     1.3 @@ -999,6 +999,9 @@
     1.4  apply (simp add: algebra_simps)
     1.5  done
     1.6  
     1.7 +lemma diff_gt_0_iff_gt [simp]: "a - b > 0 \<longleftrightarrow> a > b"
     1.8 +by (simp add: less_diff_eq)
     1.9 +
    1.10  lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
    1.11  by (auto simp add: le_less diff_less_eq )
    1.12