diff --git a/src/algebra/order/monoid_lemmas.lean b/src/algebra/order/monoid_lemmas.lean
index 638cd6154490e..c356ce1d62dd6 100644
--- a/src/algebra/order/monoid_lemmas.lean
+++ b/src/algebra/order/monoid_lemmas.lean
@@ -328,7 +328,7 @@ calc  c < a     : ha
 
 /-- Assumes left covariance. -/
 @[to_additive "Assumes left covariance."]
-lemma left.mul_lt_one_of_lt_of_lt_one [covariant_class α α (*) (<)]
+lemma mul_lt_of_lt_of_lt_one [covariant_class α α (*) (<)]
   {a b c : α} (ha : a < c) (hb : b < 1) : a * b < c :=
 calc  a * b < a * 1 : mul_lt_mul_left' hb a
         ... = a     : mul_one a
@@ -336,7 +336,7 @@ calc  a * b < a * 1 : mul_lt_mul_left' hb a
 
 /-- Assumes right covariance. -/
 @[to_additive "Assumes right covariance."]
-lemma right.mul_lt_one_of_lt_of_lt_one [covariant_class α α (swap (*)) (<)]
+lemma mul_lt_of_lt_one_of_lt [covariant_class α α (swap (*)) (<)]
   {a b c : α} (ha : a < 1) (hb : b < c) : a * b < c :=
 calc  a * b < 1 * b : mul_lt_mul_right' ha b
         ... = b     : one_mul b
@@ -503,13 +503,6 @@ h.trans_le (mul_le_of_le_one_right' hle)
 lemma le_of_le_mul_of_le_one_left (h : a ≤ b * c) (hle : c ≤ 1) : a ≤ b :=
 h.trans (mul_le_of_le_one_right' hle)
 
-@[to_additive]
-theorem mul_lt_of_lt_of_lt_one (bc : b < c) (a1 : a < 1) :
-  b * a < c :=
-calc  b * a ≤ b * 1 : mul_le_mul_left' a1.le _
-        ... = b     : mul_one b
-        ... < c     : bc
-
 end mul_one_class
 
 end left
@@ -590,12 +583,6 @@ h.trans_le (mul_le_of_le_one_left' hle)
 lemma le_of_le_mul_of_le_one_right (h : a ≤ b * c) (hle : b ≤ 1) : a ≤ c :=
 h.trans (mul_le_of_le_one_left' hle)
 
-theorem mul_lt_of_lt_one_of_lt (a1 : a < 1) (bc : b < c) :
-  a * b < c :=
-calc  a * b ≤ 1 * b : mul_le_mul_right' a1.le _
-        ... = b : one_mul b
-        ... < c : bc
-
 end le_right
 
 section lt_right