[ refactor ] Algebra.Properties.Magma.Divisibility (#2631)

* fix: issue #2629

* fix: uncaught use of deprecated name

* check: possible knock opportunity

Author: jamesmckinna

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

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