    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Divisibility over magmas
    ------------------------------------------------------------------------

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

    open import Algebra.Bundles using (Magma)

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

    open import Data.Product.Base using (_,_; swap)
    open import Relation.Binary.Definitions
      using (_Respects_; _Respectsˡ_; _Respectsʳ_; _Respects₂_; Symmetric)
    open import Relation.Nullary.Negation.Core using (contradiction)

    open Magma M

    ------------------------------------------------------------------------
    -- Re-export divisibility relations publicly

    open import Algebra.Definitions.RawMagma rawMagma public
      using (_∣_; _∤_; _∥_; _∦_; _∣ˡ_; _∤ˡ_; _∣ʳ_; _∤ʳ_; _,_)

    ------------------------------------------------------------------------
    -- Properties of right divisibility

    ∣ʳ-respʳ-≈ : _∣ʳ_ Respectsʳ _≈_
    ∣ʳ-respʳ-≈ y≈z (q , qx≈y) = q , trans qx≈y y≈z

    ∣ʳ-respˡ-≈ : _∣ʳ_ Respectsˡ _≈_
    ∣ʳ-respˡ-≈ x≈z (q , qx≈y) = q , trans (∙-congˡ (sym x≈z)) qx≈y

    ∣ʳ-resp-≈ : _∣ʳ_ Respects₂ _≈_
    ∣ʳ-resp-≈ = ∣ʳ-respʳ-≈ , ∣ʳ-respˡ-≈

    x∣ʳyx : ∀ x y → x ∣ʳ y ∙ x
    x∣ʳyx x y = y , refl

    xy≈z⇒y∣ʳz : ∀ x y {z} → x ∙ y ≈ z → y ∣ʳ z
    xy≈z⇒y∣ʳz x y xy≈z = x , xy≈z

    ------------------------------------------------------------------------
    -- Properties of left divisibility

    ∣ˡ-respʳ-≈ : _∣ˡ_ Respectsʳ _≈_
    ∣ˡ-respʳ-≈ y≈z (q , xq≈y) = q , trans xq≈y y≈z

    ∣ˡ-respˡ-≈ : _∣ˡ_ Respectsˡ _≈_
    ∣ˡ-respˡ-≈ x≈z (q , xq≈y) = q , trans (∙-congʳ (sym x≈z)) xq≈y

    ∣ˡ-resp-≈ : _∣ˡ_ Respects₂ _≈_
    ∣ˡ-resp-≈ = ∣ˡ-respʳ-≈ , ∣ˡ-respˡ-≈

    x∣ˡxy : ∀ x y → x ∣ˡ x ∙ y
    x∣ˡxy x y = y , refl

    xy≈z⇒x∣ˡz : ∀ x y {z} → x ∙ y ≈ z → x ∣ˡ z
    xy≈z⇒x∣ˡz x y xy≈z = y , xy≈z

    ------------------------------------------------------------------------
    -- Properties of non-divisibility

    ∤-respˡ-≈ : _∤_ Respectsˡ _≈_
    ∤-respˡ-≈ x≈y x∤z y∣ʳz = contradiction (∣ʳ-respˡ-≈ (sym x≈y) y∣ʳz) x∤z

    ∤-respʳ-≈ : _∤_ Respectsʳ _≈_
    ∤-respʳ-≈ x≈y z∤x z∣ʳy = contradiction (∣ʳ-respʳ-≈ (sym x≈y) z∣ʳy) z∤x

    ∤-resp-≈ : _∤_ Respects₂ _≈_
    ∤-resp-≈ = ∤-respʳ-≈ , ∤-respˡ-≈

    ------------------------------------------------------------------------
    -- Properties of mutual divisibility _∥_

    ∥-sym : Symmetric _∥_
    ∥-sym = swap

    ∥-respˡ-≈ : _∥_ Respectsˡ _≈_
    ∥-respˡ-≈ x≈z (x∣ʳy , y∣ʳx) = ∣ʳ-respˡ-≈ x≈z x∣ʳy , ∣ʳ-respʳ-≈ x≈z y∣ʳx

    ∥-respʳ-≈ : _∥_ Respectsʳ _≈_
    ∥-respʳ-≈ y≈z (x∣ʳy , y∣ʳx) = ∣ʳ-respʳ-≈ y≈z x∣ʳy , ∣ʳ-respˡ-≈ y≈z y∣ʳx

    ∥-resp-≈ : _∥_ Respects₂ _≈_
    ∥-resp-≈ = ∥-respʳ-≈ , ∥-respˡ-≈

    ------------------------------------------------------------------------
    -- Properties of mutual non-divisibility _∤∤_

    ∦-sym : Symmetric _∦_
    ∦-sym x∦y y∥x = contradiction (∥-sym y∥x) x∦y

    ∦-respˡ-≈ : _∦_ Respectsˡ _≈_
    ∦-respˡ-≈ x≈y x∦z y∥z = contradiction (∥-respˡ-≈ (sym x≈y) y∥z) x∦z

    ∦-respʳ-≈ : _∦_ Respectsʳ _≈_
    ∦-respʳ-≈ x≈y z∦x z∥y = contradiction (∥-respʳ-≈ (sym x≈y) z∥y) z∦x

    ∦-resp-≈ : _∦_ Respects₂ _≈_
    ∦-resp-≈ = ∦-respʳ-≈ , ∦-respˡ-≈

    ------------------------------------------------------------------------
    -- DEPRECATED NAMES
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version 2.2

    ∣-respˡ = ∣ʳ-respˡ-≈
    {-# WARNING_ON_USAGE ∣-respˡ
    "Warning: ∣-respˡ was deprecated in v2.2.
    Please use ∣ʳ-respˡ-≈ instead. "
    #-}
    ∣-respʳ = ∣ʳ-respʳ-≈
    {-# WARNING_ON_USAGE ∣-respʳ
    "Warning: ∣-respʳ was deprecated in v2.2.
    Please use ∣ʳ-respʳ-≈ instead. "
    #-}
    ∣-resp = ∣ʳ-resp-≈
    {-# WARNING_ON_USAGE ∣-resp
    "Warning: ∣-resp was deprecated in v2.2.
    Please use ∣ʳ-resp-≈ instead. "
    #-}

    -- Version 2.3

    ∣∣-sym = ∥-sym
    {-# WARNING_ON_USAGE ∣∣-sym
    "Warning: ∣∣-sym was deprecated in v2.3.
    Please use ∥-sym instead. "
    #-}
    ∣∣-respˡ-≈ = ∥-respˡ-≈
    {-# WARNING_ON_USAGE ∣∣-respˡ-≈
    "Warning: ∣∣-respˡ-≈ was deprecated in v2.3.
    Please use ∥-respˡ-≈ instead. "
    #-}
    ∣∣-respʳ-≈ = ∥-respʳ-≈
    {-# WARNING_ON_USAGE ∣∣-respʳ-≈
    "Warning: ∣∣-respʳ-≈ was deprecated in v2.3.
    Please use ∥-respʳ-≈ instead. "
    #-}
    ∣∣-resp-≈ = ∥-resp-≈
    {-# WARNING_ON_USAGE ∣∣-resp-≈
    "Warning: ∣∣-resp-≈ was deprecated in v2.3.
    Please use ∥-resp-≈ instead. "
    #-}
    ∤∤-sym = ∦-sym
    {-# WARNING_ON_USAGE ∤∤-sym
    "Warning: ∤∤-sym was deprecated in v2.3.
    Please use ∦-sym instead. "
    #-}
    ∤∤-respˡ-≈ = ∦-respˡ-≈
    {-# WARNING_ON_USAGE ∤∤-respˡ-≈
    "Warning: ∤∤-respˡ-≈ was deprecated in v2.3.
    Please use ∦-respˡ-≈ instead. "
    #-}
    ∤∤-respʳ-≈ = ∦-respʳ-≈
    {-# WARNING_ON_USAGE ∤∤-respʳ-≈
    "Warning: ∤∤-respʳ-≈ was deprecated in v2.3.
    Please use ∦-respʳ-≈ instead. "
    #-}
    ∤∤-resp-≈ = ∦-resp-≈
    {-# WARNING_ON_USAGE ∤∤-resp-≈
    "Warning: ∤∤-resp-≈ was deprecated in v2.3.
    Please use ∦-resp-≈ instead. "
    #-}

    ∣-respʳ-≈ = ∣ʳ-respʳ-≈
    {-# WARNING_ON_USAGE ∣-respʳ-≈
    "Warning: ∣-respʳ-≈ was deprecated in v2.3.
    Please use ∣ʳ-respʳ-≈ instead. "
    #-}

    ∣-respˡ-≈ = ∣ʳ-respˡ-≈
    {-# WARNING_ON_USAGE ∣-respˡ-≈
    "Warning: ∣-respˡ-≈ was deprecated in v2.3.
    Please use ∣ʳ-respˡ-≈ instead. "
    #-}

    ∣-resp-≈ = ∣ʳ-resp-≈
    {-# WARNING_ON_USAGE ∣-resp-≈
    "Warning: ∣-resp-≈ was deprecated in v2.3.
    Please use ∣ʳ-resp-≈ instead. "
    #-}

    x∣yx = x∣ʳyx
    {-# WARNING_ON_USAGE x∣yx
    "Warning: x∣yx was deprecated in v2.3.
    Please use x∣ʳyx instead. "
    #-}

    xy≈z⇒y∣z = xy≈z⇒y∣ʳz
    {-# WARNING_ON_USAGE xy≈z⇒y∣z
    "Warning: xy≈z⇒y∣z was deprecated in v2.3.
    Please use xy≈z⇒y∣ʳz instead. "
    #-}