    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Some derivable properties
    ------------------------------------------------------------------------

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

    open import Algebra using (MoufangLoop)

    module Algebra.Properties.MoufangLoop {a ℓ} (M : MoufangLoop a ℓ) where

    open MoufangLoop M
    open import Algebra.Definitions _≈_
    open import Relation.Binary.Reasoning.Setoid setoid
    open import Data.Product.Base using (_,_)

    alternativeˡ : LeftAlternative _∙_
    alternativeˡ x y = begin
      (x ∙ x) ∙ y       ≈⟨ ∙-congʳ (∙-congˡ (sym (identityˡ x))) ⟩
      (x ∙ (ε ∙ x)) ∙ y ≈⟨ sym (leftBol x ε y) ⟩
      x ∙ (ε ∙ (x ∙ y)) ≈⟨ ∙-congˡ (identityˡ ((x ∙ y))) ⟩
      x ∙ (x ∙ y)       ∎

    alternativeʳ : RightAlternative _∙_
    alternativeʳ x y = begin
      x ∙ (y ∙ y)         ≈⟨ ∙-congˡ(∙-congʳ(sym (identityʳ y))) ⟩
      x ∙ ((y ∙ ε) ∙ y)   ≈⟨ sym (rightBol y ε x) ⟩
      ((x ∙ y) ∙ ε ) ∙ y  ≈⟨ ∙-congʳ (identityʳ ((x ∙ y))) ⟩
      (x ∙ y) ∙ y         ∎

    alternative : Alternative _∙_
    alternative = alternativeˡ , alternativeʳ

    flex : Flexible _∙_
    flex x y = begin
      (x ∙ y) ∙ x       ≈⟨ ∙-congˡ (sym (identityˡ x)) ⟩
      (x ∙ y) ∙ (ε ∙ x) ≈⟨ identical y ε x ⟩
      x ∙ ((y ∙ ε) ∙ x) ≈⟨ ∙-congˡ (∙-congʳ (identityʳ y)) ⟩
      x ∙ (y ∙ x)       ∎

    z∙xzy≈zxz∙y : ∀ x y z → (z ∙ (x ∙ (z ∙ y))) ≈ (((z ∙ x) ∙ z) ∙ y)
    z∙xzy≈zxz∙y x y z = sym (begin
      ((z ∙ x) ∙ z) ∙ y ≈⟨ (∙-congʳ (flex z x )) ⟩
      (z ∙ (x ∙ z)) ∙ y ≈⟨ sym (leftBol z x y) ⟩
      z ∙ (x ∙ (z ∙ y)) ∎)

    x∙zyz≈xzy∙z : ∀ x y z → (x ∙ (z ∙ (y ∙ z))) ≈ (((x ∙ z) ∙ y) ∙ z)
    x∙zyz≈xzy∙z x y z = begin
      x ∙ (z ∙ (y ∙ z))  ≈⟨ (∙-congˡ (sym (flex z y ))) ⟩
      x ∙ ((z ∙ y) ∙  z) ≈⟨ sym (rightBol z y x) ⟩
      ((x ∙ z) ∙ y) ∙ z  ∎

    z∙xyz≈zxy∙z : ∀ x y z → (z ∙ ((x ∙ y) ∙ z)) ≈ ((z ∙ (x ∙ y)) ∙ z)
    z∙xyz≈zxy∙z x y z = sym (flex z (x ∙ y))