src/HOL/Rings.thy
changeset 66793 deabce3ccf1f
parent 65811 2653f1cd8775
child 66807 c3631f32dfeb
     1.1 --- a/src/HOL/Rings.thy	Sun Oct 08 16:50:37 2017 +0200
     1.2 +++ b/src/HOL/Rings.thy	Mon Oct 09 15:34:23 2017 +0100
     1.3 @@ -2241,6 +2241,10 @@
     1.4  lemma minus_less_iff_1 [simp, no_atp]: "- a < 1 \<longleftrightarrow> - 1 < a"
     1.5    by (fact minus_less_iff)
     1.6  
     1.7 +lemma add_less_zeroD:
     1.8 +  shows "x+y < 0 \<Longrightarrow> x<0 \<or> y<0"
     1.9 +  by (auto simp: not_less intro: le_less_trans [of _ "x+y"])
    1.10 +
    1.11  end
    1.12  
    1.13  text \<open>Simprules for comparisons where common factors can be cancelled.\<close>