--- a/src/HOL/Fields.thy Mon Feb 24 13:52:48 2014 +0100
+++ b/src/HOL/Fields.thy Mon Feb 24 15:45:55 2014 +0000
@@ -1156,6 +1156,12 @@
apply (simp add: order_less_imp_le)
done
+lemma zero_le_divide_abs_iff [simp]: "(0 \<le> a / abs b) = (0 \<le> a | b = 0)"
+by (auto simp: zero_le_divide_iff)
+
+lemma divide_le_0_abs_iff [simp]: "(a / abs b \<le> 0) = (a \<le> 0 | b = 0)"
+by (auto simp: divide_le_0_iff)
+
lemma field_le_mult_one_interval:
assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
shows "x \<le> y"