    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of the propositional suffix relation
    ------------------------------------------------------------------------

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

    module Data.List.Relation.Binary.Suffix.Propositional.Properties {a} {A : Set a} where

    open import Data.List.Base using (List; []; _∷_)
    open import Data.List.Properties using (++-monoid)

    open import Data.List.Relation.Binary.Suffix.Heterogeneous
      using (Suffix; here; there; fromView; _++_)
    open import Data.List.Relation.Binary.Prefix.Homogeneous.Properties
    import Data.List.Relation.Binary.Pointwise as Pointwise

    open import Algebra.Properties.Monoid.Divisibility (++-monoid A)

    open import Relation.Binary.PropositionalEquality using (_≡_; refl)
    open import Relation.Binary using (_⇒_)

    ------------------------------------------------------------------------
    -- The inductive definition of the propositional Suffix relation is
    -- equivalent to the notion of right divisibility induced by the
    -- (List A, _++_, []) monoid

    Suffix-as-∣ʳ : Suffix _≡_ ⇒ _∣ʳ_
    Suffix-as-∣ʳ (here equal) = ∣ʳ-reflexive (Pointwise.Pointwise-≡⇒≡ equal)
    Suffix-as-∣ʳ (there suff) = x∣ʳy⇒x∣ʳzy (_ ∷ []) (Suffix-as-∣ʳ suff)

    ∣ʳ-as-Suffix : _∣ʳ_ ⇒ Suffix _≡_
    ∣ʳ-as-Suffix (rest , refl) = fromView (rest ++ Pointwise.refl refl)