diff --git a/src/Algebra/Properties/CommutativeMagma/Divisibility.agda b/src/Algebra/Properties/CommutativeMagma/Divisibility.agda
index 9261d80e82..432f039203 100644
--- a/src/Algebra/Properties/CommutativeMagma/Divisibility.agda
+++ b/src/Algebra/Properties/CommutativeMagma/Divisibility.agda
@@ -28,7 +28,7 @@ x∣xy : ∀ x y → x ∣ x ∙ y
 x∣xy x y = y , comm y x
 
 xy≈z⇒x∣z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z
-xy≈z⇒x∣z x y xy≈z = ∣-respʳ xy≈z (x∣xy x y)
+xy≈z⇒x∣z x y xy≈z = ∣-respʳ-≈ xy≈z (x∣xy x y)
 
 x|xy∧y|xy : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y)
 x|xy∧y|xy x y = x∣xy x y , x∣yx y x
diff --git a/src/Algebra/Properties/Magma/Divisibility.agda b/src/Algebra/Properties/Magma/Divisibility.agda
index cbbc4cac70..1d38c29d42 100644
--- a/src/Algebra/Properties/Magma/Divisibility.agda
+++ b/src/Algebra/Properties/Magma/Divisibility.agda
@@ -39,7 +39,7 @@ x∣yx : ∀ x y → x ∣ y ∙ x
 x∣yx x y = y , refl
 
 xy≈z⇒y∣z : ∀ x y {z} → x ∙ y ≈ z → y ∣ z
-xy≈z⇒y∣z x y xy≈z = ∣-respʳ-≈ xy≈z (x∣yx y x)
+xy≈z⇒y∣z x y xy≈z = x , xy≈z
 
 ------------------------------------------------------------------------
 -- Properties of non-divisibility