------------------------------------------------------------------------
-- Convenient syntax for "equational reasoning" using a strict partial
-- order
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.StrictPartialOrderReasoning
         (p : StrictPartialOrder) where

import Relation.Binary.PreorderReasoning as PreR
import Relation.Binary.Props.StrictPartialOrder as SPO
open PreR (SPO.preorder p) public renaming (_∼⟨_⟩_ to _<⟨_⟩_)