We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 098b4cf commit e533c8bCopy full SHA for e533c8b
src/Algebra/Properties/Magma/Divisibility.agda
@@ -39,7 +39,7 @@ x∣yx : ∀ x y → x ∣ y ∙ x
39
x∣yx x y = y , refl
40
41
xy≈z⇒y∣z : ∀ x y {z} → x ∙ y ≈ z → y ∣ z
42
-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
43
44
------------------------------------------------------------------------
45
-- Properties of non-divisibility
0 commit comments