[ DRY ] refactor Algebra.Properties.{Quasigroup|Loop} (#2768)

* [ DRY ] refactor `Algebra.Properties.Quasigroup`

* refactor: also `Loop` properties

Author: jamesmckinna

src/Algebra/Properties/Loop.agda

@@ -17,28 +17,16 @@ open import Data.Product.Base using (proj₂)
 open import Relation.Binary.Reasoning.Setoid setoid
 
 x//x≈ε : ∀ x → x // x ≈ ε
-x//x≈ε x = begin
-  x // x       ≈⟨ //-congʳ (identityˡ x) ⟨
-  (ε ∙ x) // x ≈⟨ rightDividesʳ x ε ⟩
-  ε            ∎
+x//x≈ε x = sym (x≈z//y _ _ _ (identityˡ x))
 
 x\\x≈ε : ∀ x → x \\ x ≈ ε
-x\\x≈ε x = begin
-  x \\ x       ≈⟨ \\-congˡ (identityʳ x ) ⟨
-  x \\ (x ∙ ε) ≈⟨ leftDividesʳ x ε ⟩
-  ε            ∎
+x\\x≈ε x = sym (y≈x\\z _ _ _ (identityʳ x))
 
 ε\\x≈x : ∀ x → ε \\ x ≈ x
-ε\\x≈x x = begin
-  ε \\ x       ≈⟨ identityˡ (ε \\ x) ⟨
-  ε ∙ (ε \\ x) ≈⟨ leftDividesˡ ε x ⟩
-  x            ∎
+ε\\x≈x x = sym (y≈x\\z _ _ _ (identityˡ x))
 
 x//ε≈x : ∀ x → x // ε ≈ x
-x//ε≈x x = begin
- x // ε       ≈⟨ identityʳ (x // ε) ⟨
- (x // ε) ∙ ε ≈⟨ rightDividesˡ ε x ⟩
- x            ∎
+x//ε≈x x = sym (x≈z//y _ _ _ (identityʳ x))
 
 identityˡ-unique : ∀ x y → x ∙ y ≈ y → x ≈ ε
 identityˡ-unique x y eq = begin

src/Algebra/Properties/Quasigroup.agda

@@ -15,31 +15,29 @@ open import Algebra.Definitions _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
 open import Data.Product.Base using (_,_)
 
+y≈x\\z : ∀ x y z → x ∙ y ≈ z → y ≈ x \\ z
+y≈x\\z x y z eq = begin
+  y            ≈⟨ leftDividesʳ x y ⟨
+  x \\ (x ∙ y) ≈⟨ \\-congˡ eq ⟩
+  x \\ z       ∎
+
+x≈z//y : ∀ x y z → x ∙ y ≈ z → x ≈ z // y
+x≈z//y x y z eq = begin
+  x            ≈⟨ rightDividesʳ y x ⟨
+  (x ∙ y) // y ≈⟨ //-congʳ eq ⟩
+  z // y       ∎
+
 cancelˡ : LeftCancellative _∙_
 cancelˡ x y z eq = begin
-  y             ≈⟨ leftDividesʳ x y ⟨
-  x \\ (x ∙ y)  ≈⟨ \\-congˡ eq ⟩
+  y             ≈⟨ y≈x\\z x y (x ∙ z) eq ⟩
   x \\ (x ∙ z)  ≈⟨ leftDividesʳ x z ⟩
   z             ∎
 
 cancelʳ : RightCancellative _∙_
 cancelʳ x y z eq = begin
-  y             ≈⟨ rightDividesʳ x y ⟨
-  (y ∙ x) // x  ≈⟨ //-congʳ eq ⟩
+  y             ≈⟨ x≈z//y y x (z ∙ x) eq ⟩
   (z ∙ x) // x  ≈⟨ rightDividesʳ x z ⟩
   z             ∎
 
 cancel : Cancellative _∙_
 cancel = cancelˡ , cancelʳ
-
-y≈x\\z : ∀ x y z → x ∙ y ≈ z → y ≈ x \\ z
-y≈x\\z x y z eq = begin
-  y            ≈⟨ leftDividesʳ x y ⟨
-  x \\ (x ∙ y) ≈⟨ \\-congˡ eq ⟩
-  x \\ z       ∎
-
-x≈z//y : ∀ x y z → x ∙ y ≈ z → x ≈ z // y
-x≈z//y x y z eq = begin
-  x            ≈⟨ rightDividesʳ y x ⟨
-  (x ∙ y) // y ≈⟨ //-congʳ eq ⟩
-  z // y       ∎