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