src/HOL/Groups.thy
 changeset 62378 85ed00c1fe7c parent 62377 ace69956d018 child 62379 340738057c8c
```     1.1 --- a/src/HOL/Groups.thy	Fri Feb 12 16:09:07 2016 +0100
1.2 +++ b/src/HOL/Groups.thy	Fri Feb 19 13:40:50 2016 +0100
1.3 @@ -753,6 +753,13 @@
1.4  end
1.5
1.7 +begin
1.8 +
1.10 +  shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
1.11 +  using add_strict_mono [of 0 a b c] by simp
1.12 +
1.13 +end
1.14
1.16  begin
1.17 @@ -1311,15 +1318,37 @@
1.18    assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
1.19  begin
1.20
1.21 -lemma zero_le: "0 \<le> x"
1.22 +lemma zero_le[simp]: "0 \<le> x"
1.24
1.25 +lemma le_zero_eq[simp]: "n \<le> 0 \<longleftrightarrow> n = 0"
1.26 +  by (auto intro: antisym)
1.27 +
1.28 +lemma not_less_zero[simp]: "\<not> n < 0"
1.29 +  by (auto simp: less_le)
1.30 +
1.31 +lemma zero_less_iff_neq_zero: "(0 < n) \<longleftrightarrow> (n \<noteq> 0)"
1.32 +  by (auto simp: less_le)
1.33 +
1.34 +text \<open>This theorem is useful with \<open>blast\<close>\<close>
1.35 +lemma gr_zeroI: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n"
1.36 +  by (rule zero_less_iff_neq_zero[THEN iffD2]) iprover
1.37 +
1.38 +lemma not_gr_zero[simp]: "(\<not> (0 < n)) \<longleftrightarrow> (n = 0)"
1.39 +  by (simp add: zero_less_iff_neq_zero)
1.40 +
1.43
1.44  lemma add_eq_0_iff_both_eq_0: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"