{-# OPTIONS --without-K #-} module sets.nat.ordering.leq where open import sets.nat.ordering.leq.core public open import sets.nat.ordering.leq.level public open import sets.nat.ordering.leq.decide public