--- a/src/HOL/Rings.thy Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Rings.thy Fri Feb 02 11:25:11 2024 +0000
@@ -2378,6 +2378,18 @@
lemma mult_less_cancel_left_neg: "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
by (auto simp: mult_less_cancel_left)
+lemma mult_le_cancel_right_pos: "0 < c \<Longrightarrow> a * c \<le> b * c \<longleftrightarrow> a \<le> b"
+ by (auto simp: mult_le_cancel_right)
+
+lemma mult_le_cancel_right_neg: "c < 0 \<Longrightarrow> a * c \<le> b * c \<longleftrightarrow> b \<le> a"
+ by (auto simp: mult_le_cancel_right)
+
+lemma mult_less_cancel_right_pos: "0 < c \<Longrightarrow> a * c < b * c \<longleftrightarrow> a < b"
+ by (auto simp: mult_less_cancel_right)
+
+lemma mult_less_cancel_right_neg: "c < 0 \<Longrightarrow> a * c < b * c \<longleftrightarrow> b < a"
+ by (auto simp: mult_less_cancel_right)
+
end
lemmas mult_sign_intros =
@@ -2784,7 +2796,6 @@
end
-
subsection \<open>Dioids\<close>
text \<open>