src/HOL/Int.thy
changeset 59536 03bde055a1a0
parent 59000 6eb0725503fc
child 59556 aa2deef7cf47
     1.1 --- a/src/HOL/Int.thy	Sat Feb 14 10:24:15 2015 +0100
     1.2 +++ b/src/HOL/Int.thy	Sat Feb 14 10:24:15 2015 +0100
     1.3 @@ -542,16 +542,6 @@
     1.4  
     1.5  text {* Preliminaries *}
     1.6  
     1.7 -lemma even_less_0_iff:
     1.8 -  "a + a < 0 \<longleftrightarrow> a < (0::'a::linordered_idom)"
     1.9 -proof -
    1.10 -  have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: distrib_right del: one_add_one)
    1.11 -  also have "(1+1)*a < 0 \<longleftrightarrow> a < 0"
    1.12 -    by (simp add: mult_less_0_iff zero_less_two 
    1.13 -                  order_less_not_sym [OF zero_less_two])
    1.14 -  finally show ?thesis .
    1.15 -qed
    1.16 -
    1.17  lemma le_imp_0_less: 
    1.18    assumes le: "0 \<le> z"
    1.19    shows "(0::int) < 1 + z"