diff --git a/src/Algebra/Properties/Loop.agda b/src/Algebra/Properties/Loop.agda index 46ed1e7f7c..590e842536 100644 --- a/src/Algebra/Properties/Loop.agda +++ b/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 diff --git a/src/Algebra/Properties/Quasigroup.agda b/src/Algebra/Properties/Quasigroup.agda index e8c7516978..1fee19a247 100644 --- a/src/Algebra/Properties/Quasigroup.agda +++ b/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 ∎