src/HOL/Groups.thy
changeset 62348 9a5f43dac883
parent 62347 2230b7047376
child 62376 85f38d5f8807
     1.1 --- a/src/HOL/Groups.thy	Wed Feb 17 21:51:57 2016 +0100
     1.2 +++ b/src/HOL/Groups.thy	Wed Feb 17 21:51:57 2016 +0100
     1.3 @@ -999,14 +999,17 @@
     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 +lemma diff_gt_0_iff_gt [simp]:
    1.10 +  "a - b > 0 \<longleftrightarrow> a > b"
    1.11 +  by (simp add: less_diff_eq)
    1.12  
    1.13 -lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
    1.14 -by (auto simp add: le_less diff_less_eq )
    1.15 +lemma diff_le_eq [algebra_simps, field_simps]:
    1.16 +  "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
    1.17 +  by (auto simp add: le_less diff_less_eq )
    1.18  
    1.19 -lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
    1.20 -by (auto simp add: le_less less_diff_eq)
    1.21 +lemma le_diff_eq [algebra_simps, field_simps]:
    1.22 +  "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
    1.23 +  by (auto simp add: le_less less_diff_eq)
    1.24  
    1.25  lemma diff_le_0_iff_le [simp]:
    1.26    "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
    1.27 @@ -1014,6 +1017,10 @@
    1.28  
    1.29  lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
    1.30  
    1.31 +lemma diff_ge_0_iff_ge [simp]:
    1.32 +  "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
    1.33 +  by (simp add: le_diff_eq)
    1.34 +
    1.35  lemma diff_eq_diff_less:
    1.36    "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
    1.37    by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])