------------------------------------------------------------------------
-- Equational resoning for partial orders
------------------------------------------------------------------------

open import Tools.Relation

module Tools.Reasoning.PartialOrder
  {a ℓ ℓ′} (P : Poset a ℓ ℓ′)
  where

open import Relation.Binary.Reasoning.PartialOrder P public