    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Some basic properties of Quasigroup
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    open import Algebra.Bundles using (MiddleBolLoop)

    module Algebra.Properties.MiddleBolLoop {m₁ m₂} (M : MiddleBolLoop m₁ m₂) where

    open MiddleBolLoop M
    open import Algebra.Definitions _≈_
    open import Relation.Binary.Reasoning.Setoid setoid
    import Algebra.Properties.Loop as LoopProperties
    open LoopProperties loop public

    xyx\\x≈y\\x : ∀ x y → x ∙ ((y ∙ x) \\ x) ≈ y \\ x
    xyx\\x≈y\\x x y = begin
      x ∙ ((y ∙ x) \\ x)  ≈⟨ middleBol x y x ⟩
      (x // x) ∙ (y \\ x) ≈⟨ ∙-congʳ (x//x≈ε x) ⟩
      ε ∙ (y \\ x)        ≈⟨ identityˡ ((y \\ x)) ⟩
      y \\ x              ∎

    xxz\\x≈x//z : ∀ x z → x ∙ ((x ∙ z) \\ x) ≈ x // z
    xxz\\x≈x//z x z = begin
      x ∙ ((x ∙ z) \\ x)  ≈⟨ middleBol x x z ⟩
      (x // z) ∙ (x \\ x) ≈⟨ ∙-congˡ (x\\x≈ε x) ⟩
      (x // z) ∙ ε        ≈⟨ identityʳ ((x // z)) ⟩
      x // z              ∎

    xz\\x≈x//zx : ∀ x z → x ∙ (z \\ x) ≈ (x // z) ∙ x
    xz\\x≈x//zx x z = begin
      x ∙ (z \\ x)       ≈⟨ ∙-congˡ (\\-congʳ( sym (identityˡ z))) ⟩
      x ∙ ((ε ∙ z) \\ x) ≈⟨ middleBol x ε z ⟩
      x // z ∙ (ε \\ x)  ≈⟨ ∙-congˡ (ε\\x≈x x) ⟩
      x // z ∙ x         ∎

    x//yzx≈x//zy\\x : ∀ x y z → (x // (y ∙ z)) ∙ x ≈ (x // z) ∙ (y \\ x)
    x//yzx≈x//zy\\x x y z = begin
     (x // (y ∙ z)) ∙ x  ≈⟨ sym (xz\\x≈x//zx x ((y ∙ z))) ⟩
     x ∙ ((y ∙ z) \\ x)  ≈⟨ middleBol x y z ⟩
     (x // z) ∙ (y \\ x) ∎

    x//yxx≈y\\x : ∀ x y → (x // (y ∙ x)) ∙ x ≈ y \\ x
    x//yxx≈y\\x x y = begin
      (x // (y ∙ x)) ∙ x  ≈⟨ x//yzx≈x//zy\\x  x y x ⟩
      (x // x) ∙ (y \\ x) ≈⟨ ∙-congʳ (x//x≈ε x) ⟩
      ε ∙ (y \\ x)        ≈⟨ identityˡ ((y \\ x)) ⟩
      y \\ x              ∎

    x//xzx≈x//z : ∀ x z → (x // (x ∙ z)) ∙ x ≈ x // z
    x//xzx≈x//z x z = begin
      (x // (x ∙ z)) ∙ x  ≈⟨ x//yzx≈x//zy\\x x x z ⟩
      (x // z) ∙ (x \\ x) ≈⟨ ∙-congˡ (x\\x≈ε x) ⟩
      (x // z) ∙ ε        ≈⟨ identityʳ (x // z) ⟩
      x // z              ∎