--- a/src/HOL/Fields.thy Mon Jul 29 10:49:17 2024 +0100
+++ b/src/HOL/Fields.thy Mon Jul 29 16:22:05 2024 +0100
@@ -949,7 +949,7 @@
by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono)
lemma divide_left_mono:
- "\<lbrakk>b \<le> a; 0 \<le> c; 0 < b\<rbrakk> \<Longrightarrow> c / a \<le> c / b"
+ "\<lbrakk>b \<le> a; 0 \<le> c; 0 < a*b\<rbrakk> \<Longrightarrow> c / a \<le> c / b"
by (auto simp: field_simps zero_less_mult_iff mult_right_mono)
lemma divide_strict_left_mono_neg:
@@ -1156,7 +1156,7 @@
lemma divide_right_mono_neg: "a \<le> b \<Longrightarrow> c \<le> 0 \<Longrightarrow> b / c \<le> a / c"
by (auto dest: divide_right_mono [of _ _ "- c"])
-lemma divide_left_mono_neg: "a \<le> b \<Longrightarrow> c \<le> 0 \<Longrightarrow> 0 < a \<Longrightarrow> c / a \<le> c / b"
+lemma divide_left_mono_neg: "a \<le> b \<Longrightarrow> c \<le> 0 \<Longrightarrow> 0 < a * b \<Longrightarrow> c / a \<le> c / b"
by (auto simp add: mult.commute dest: divide_left_mono [of _ _ "- c"])
lemma inverse_le_iff: "inverse a \<le> inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b \<le> a) \<and> (a * b \<le> 0 \<longrightarrow> a \<le> b)"