```------------------------------------------------------------------------
-- 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
open import Data.Product
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              ∎
```