diff -r bac8921e2901 -r d56e4eeae967 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Wed Nov 11 11:27:44 2020 +0000
+++ b/src/HOL/Real.thy	Wed Nov 11 14:27:17 2020 +0000
@@ -950,24 +950,6 @@
 lifting_forget real.lifting
 
 
-subsection \<open>More Lemmas\<close>
-
-text \<open>BH: These lemmas should not be necessary; they should be
-  covered by existing simp rules and simplification procedures.\<close>
-
-lemma real_mult_less_iff1 [simp]: "0 < z \<Longrightarrow> x * z < y * z \<longleftrightarrow> x < y"
-  for x y z :: real
-  by simp (* solved by linordered_ring_less_cancel_factor simproc *)
-
-lemma real_mult_le_cancel_iff1 [simp]: "0 < z \<Longrightarrow> x * z \<le> y * z \<longleftrightarrow> x \<le> y"
-  for x y z :: real
-  by simp (* solved by linordered_ring_le_cancel_factor simproc *)
-
-lemma real_mult_le_cancel_iff2 [simp]: "0 < z \<Longrightarrow> z * x \<le> z * y \<longleftrightarrow> x \<le> y"
-  for x y z :: real
-  by simp (* solved by linordered_ring_le_cancel_factor simproc *)
-
-
 subsection \<open>Embedding numbers into the Reals\<close>
 
 abbreviation real_of_nat :: "nat \<Rightarrow> real"