src/HOL/Rings.thy
changeset 35631 0b8a5fd339ab
parent 35302 4bc6b4d70e08
child 35828 46cfc4b8112e
     1.1 --- a/src/HOL/Rings.thy	Sat Mar 06 16:02:22 2010 -0800
     1.2 +++ b/src/HOL/Rings.thy	Sat Mar 06 18:24:30 2010 -0800
     1.3 @@ -796,6 +796,13 @@
     1.4       auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg)
     1.5  qed (auto simp add: abs_if)
     1.6  
     1.7 +lemma zero_le_square [simp]: "0 \<le> a * a"
     1.8 +  using linear [of 0 a]
     1.9 +  by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
    1.10 +
    1.11 +lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
    1.12 +  by (simp add: not_less)
    1.13 +
    1.14  end
    1.15  
    1.16  (* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
    1.17 @@ -873,12 +880,6 @@
    1.18    apply force
    1.19    done
    1.20  
    1.21 -lemma zero_le_square [simp]: "0 \<le> a * a"
    1.22 -by (simp add: zero_le_mult_iff linear)
    1.23 -
    1.24 -lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
    1.25 -by (simp add: not_less)
    1.26 -
    1.27  text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
    1.28     also with the relations @{text "\<le>"} and equality.*}
    1.29