src/HOL/Rings.thy

 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
 begin
 
 subclass semiring_0_cancel ..
 
-lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
+lemma mult_nonneg_nonneg[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
 using mult_left_mono [of 0 b a] by simp
 
 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
 using mult_left_mono [of b 0 a] by simp
 

 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
 using mult_right_mono_neg [of a 0 b] by simp
 
 lemma split_mult_pos_le:
   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
-by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
+by (auto simp add: mult_nonpos_nonpos)
 
 end
 
 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
 begin

     by (auto simp add: abs_if not_le not_less algebra_simps simp del: add.commute dest: add_neg_neg add_nonneg_nonneg)
 qed (auto simp add: abs_if)
 
 lemma zero_le_square [simp]: "0 \<le> a * a"
   using linear [of 0 a]
-  by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
+  by (auto simp add: mult_nonpos_nonpos)
 
 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
   by (simp add: not_less)
 
 end