diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,4 +1,10 @@
-# Revision history for boring
+# Revision history for fin
+
+## 0.0.3
+
+- Add `Data.Type.Nat.LE`, `Data.Type.Nat.LT` and `Data.Type.Nat.LE.ReflStep`
+  modules
+- Add `withSNat` and `discreteNat`
 
 ## 0.0.2
 
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2017, Oleg Grenrus
+Copyright (c) 2017-2019, Oleg Grenrus
 
 All rights reserved.
 
diff --git a/fin.cabal b/fin.cabal
--- a/fin.cabal
+++ b/fin.cabal
@@ -1,8 +1,8 @@
 cabal-version:      >=1.10
 name:               fin
-version:            0.0.2
+version:            0.0.3
 synopsis:           Nat and Fin: peano naturals and finite numbers
-category:           Data
+category:           Data, Dependent Types, Singletons
 description:
   This package provides two simple types, and some tools to work with them.
   Also on type level as @DataKinds@.
@@ -52,7 +52,7 @@
 license-file:       LICENSE
 author:             Oleg Grenrus <oleg.grenrus@iki.fi>
 maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>
-copyright:          (c) 2017 Oleg Grenrus
+copyright:          (c) 2017-2019 Oleg Grenrus
 build-type:         Simple
 extra-source-files: ChangeLog.md
 tested-with:
@@ -68,17 +68,21 @@
     Data.Fin.Enum
     Data.Nat
     Data.Type.Nat
+    Data.Type.Nat.LE
+    Data.Type.Nat.LE.ReflStep
+    Data.Type.Nat.LT
 
   build-depends:
       base      >=4.7     && <4.13
+    , dec       >=0.0.3   && <0.1
     , deepseq   >=1.3.0.2 && <1.5
-    , hashable  >=1.2.7.0 && <1.3
+    , hashable  >=1.2.7.0 && <1.4
 
   if !impl(ghc >=8.2)
     build-depends: bifunctors >=5.5.3 && <5.6
 
   if !impl(ghc >=8.0)
-    build-depends: semigroups >=0.18.4 && <0.19
+    build-depends: semigroups >=0.18.4 && <0.20
 
   if !impl(ghc >=7.10)
     build-depends:
diff --git a/src/Data/Type/Nat.hs b/src/Data/Type/Nat.hs
--- a/src/Data/Type/Nat.hs
+++ b/src/Data/Type/Nat.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP                  #-}
 {-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE EmptyCase            #-}
 {-# LANGUAGE GADTs                #-}
 {-# LANGUAGE KindSignatures       #-}
 {-# LANGUAGE RankNTypes           #-}
@@ -26,12 +27,14 @@
     snatToNatural,
     -- * Implicit
     SNatI(..),
+    withSNat,
     reify,
     reflect,
     reflectToNum,
     -- * Equality
     eqNat,
     EqNat,
+    discreteNat,
     -- * Induction
     induction,
     induction1,
@@ -63,6 +66,7 @@
 import Data.Nat
 import Data.Proxy         (Proxy (..))
 import Data.Type.Equality
+import Data.Type.Dec
 import Numeric.Natural    (Natural)
 
 import qualified GHC.TypeLits as GHC
@@ -85,6 +89,13 @@
 instance            SNatI 'Z         where snat = SZ
 instance SNatI n => SNatI ('S n)     where snat = SS
 
+-- | Constructor 'SNatI' dictionary from 'SNat'.
+--
+-- @since 0.0.3
+withSNat :: SNat n -> (SNatI n => r) -> r
+withSNat SZ k = k
+withSNat SS k = k
+
 -- | Reflect type-level 'Nat' to the term level.
 reflect :: forall n proxy. SNatI n => proxy n -> Nat
 reflect _ = unTagged (induction1 (Tagged Z) (retagMap S) :: Tagged n Nat)
@@ -152,6 +163,32 @@
         return Refl
 
 newtype NatEq n = NatEq { getNatEq :: forall m. SNatI m => Maybe (n :~: m) }
+
+-- | Decide equality of type-level numbers.
+--
+-- >>> decShow (discreteNat :: Dec (Nat3 :~: Plus Nat1 Nat2))
+-- "Yes Refl"
+--
+-- @since 0.0.3
+discreteNat :: forall n m. (SNatI n, SNatI m) => Dec (n :~: m)
+discreteNat = getDiscreteNat $ induction (DiscreteNat start) (\p -> DiscreteNat (step p))
+  where
+    start :: forall p. SNatI p => Dec ('Z :~: p)
+    start = case snat :: SNat p of
+        SZ -> Yes Refl
+        SS -> No $ \p -> case p of {}
+
+    step :: forall p q. SNatI q => DiscreteNat p -> Dec ('S p :~: q)
+    step rec = case snat :: SNat q of
+        SZ -> No $ \p -> case p of {}
+        SS -> step' rec
+
+    step' :: forall p q. SNatI q => DiscreteNat p -> Dec ('S p :~: 'S q)
+    step' (DiscreteNat rec) = case rec :: Dec (p :~: q) of
+        Yes Refl -> Yes Refl
+        No np    -> No $ \Refl -> np Refl
+
+newtype DiscreteNat n = DiscreteNat { getDiscreteNat :: forall m. SNatI m => Dec (n :~: m) }
 
 instance TestEquality SNat where
     testEquality SZ SZ = Just Refl
diff --git a/src/Data/Type/Nat/LE.hs b/src/Data/Type/Nat/LE.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Nat/LE.hs
@@ -0,0 +1,184 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE EmptyCase             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE StandaloneDeriving    #-}
+{-# LANGUAGE TypeOperators         #-}
+
+{-# LANGUAGE UndecidableInstances  #-}
+-- | Less-than-or-equal relation for (unary) natural numbers 'Nat'.
+--
+-- There are at least three ways to encode this relation.
+--
+-- * \(zero : 0 \le m\) and \(succ : n \le m \to 1 + n \le 1 + m\) (this module),
+--
+-- * \(refl : n \le n \) and \(step : n \le m \to n \le 1 + m\) ("Data.Type.Nat.LE.ReflStep"),
+--
+-- * \(ex : \exists p. n + p \equiv m \) (tricky in Haskell).
+--
+-- Depending on a situation, usage ergonomics are different.
+--
+module Data.Type.Nat.LE (
+    -- * Relation
+    LE (..),
+    LEProof (..),
+    withLEProof,
+    -- * Decidability
+    decideLE,
+    -- * Lemmas
+    -- ** Constructor like
+    leZero,
+    leSucc,
+    leRefl,
+    leStep,
+    -- ** Partial order
+    leAsym,
+    leTrans,
+    -- ** Total order
+    leSwap,
+    leSwap',
+    -- ** More
+    leStepL,
+    lePred,
+    proofZeroLEZero,
+    ) where
+
+import Data.Type.Dec      (Dec (..), Decidable (..), Neg)
+import Data.Type.Equality
+import Data.Type.Nat
+import Data.Void          (absurd)
+
+-------------------------------------------------------------------------------
+-- Proof
+-------------------------------------------------------------------------------
+
+-- | An evidence of \(n \le m\). /zero+succ/ definition.
+data LEProof n m where
+    LEZero :: LEProof 'Z m
+    LESucc :: LEProof n m -> LEProof ('S n) ('S m)
+
+deriving instance Show (LEProof n m)
+
+-- | 'LEProof' values are unique (not @'Boring'@ though!).
+instance Eq (LEProof n m) where
+    _ == _ = True
+
+instance Ord (LEProof n m) where
+    compare _ _ = EQ
+
+-------------------------------------------------------------------------------
+-- Class
+-------------------------------------------------------------------------------
+
+-- | Total order of 'Nat', less-than-or-Equal-to, \( \le \).
+--
+class LE n m where
+    leProof :: LEProof n m
+
+instance LE 'Z m where
+    leProof = LEZero
+
+instance (m ~ 'S m', LE n m') => LE ('S n) m where
+    leProof = LESucc leProof
+
+-- | Constructor 'LE' dictionary from 'LEProof'.
+withLEProof :: LEProof n m -> (LE n m => r) -> r
+withLEProof LEZero     k = k
+withLEProof (LESucc p) k = withLEProof p k
+
+-------------------------------------------------------------------------------
+-- Lemmas
+-------------------------------------------------------------------------------
+
+-- | \(\forall n : \mathbb{N}, 0 \le n \)
+leZero :: LEProof 'Z n
+leZero = LEZero
+
+-- | \(\forall n\, m : \mathbb{N}, n \le m \to 1 + n \le 1 + m \)
+leSucc :: LEProof n m -> LEProof ('S n) ('S m)
+leSucc = LESucc
+
+-- | \(\forall n\, m : \mathbb{N}, 1 + n \le 1 + m \to n \le m \)
+lePred :: LEProof ('S n) ('S m) -> LEProof n m
+lePred (LESucc p) = p
+
+-- | \(\forall n : \mathbb{N}, n \le n \)
+leRefl :: forall n. SNatI n => LEProof n n
+leRefl = case snat :: SNat n of
+    SZ -> LEZero
+    SS -> LESucc leRefl
+
+-- | \(\forall n\, m : \mathbb{N}, n \le m \to n \le 1 + m \)
+leStep :: LEProof n m -> LEProof n ('S m)
+leStep LEZero     = LEZero
+leStep (LESucc p) = LESucc (leStep p)
+
+-- | \(\forall n\, m : \mathbb{N}, 1 + n \le m \to n \le m \)
+leStepL :: LEProof ('S n) m -> LEProof n m
+leStepL (LESucc p) = leStep p
+
+-- | \(\forall n\, m : \mathbb{N}, n \le m \to m \le n \to n \equiv m \)
+leAsym :: LEProof n m -> LEProof m n -> n :~: m
+leAsym LEZero     LEZero     = Refl
+leAsym (LESucc p) (LESucc q) = case leAsym p q of Refl -> Refl
+-- leAsym LEZero p = case p of {}
+-- leAsym p LEZero = case p of {}
+
+-- | \(\forall n\, m\, p : \mathbb{N}, n \le m \to m \le p \to n \le p \)
+leTrans :: LEProof n m -> LEProof m p -> LEProof n p
+leTrans LEZero     _          = LEZero
+leTrans (LESucc p) (LESucc q) = LESucc (leTrans p q)
+-- leTrans (LESucc _) q = case q of {}
+
+-- | \(\forall n\, m : \mathbb{N}, \neg (n \le m) \to 1 + m \le n \)
+leSwap :: forall n m. (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof ('S m) n
+leSwap np = case (snat :: SNat m, snat :: SNat n) of
+    (_,  SZ) -> absurd (np LEZero)
+    (SZ, SS) -> LESucc LEZero
+    (SS, SS) -> LESucc $ leSwap $ \p -> np $ LESucc p
+
+-- | \(\forall n\, m : \mathbb{N}, n \le m \to \neg (1 + m \le n) \)
+--
+-- >>> leProof :: LEProof Nat2 Nat3
+-- LESucc (LESucc LEZero)
+--
+-- >>> leSwap (leSwap' (leProof :: LEProof Nat2 Nat3))
+-- LESucc (LESucc (LESucc LEZero))
+--
+-- >>> lePred (leSwap (leSwap' (leProof :: LEProof Nat2 Nat3)))
+-- LESucc (LESucc LEZero)
+--
+leSwap' :: LEProof n m -> LEProof ('S m) n -> void
+leSwap' p (LESucc q) = case p of LESucc p' -> leSwap' p' q
+
+-------------------------------------------------------------------------------
+-- Dedidablity
+-------------------------------------------------------------------------------
+
+-- | Find the @'LEProof' n m@, i.e. compare numbers.
+decideLE :: forall n m. (SNatI n, SNatI m) => Dec (LEProof n m)
+decideLE = case snat :: SNat n of
+    SZ -> Yes leZero
+    SS -> caseSnm
+  where
+    caseSnm :: forall n' m'. (SNatI n', SNatI m') => Dec (LEProof ('S n') m')
+    caseSnm = case snat :: SNat m' of
+        SZ -> No $ \p -> case p of {} -- ooh, GHC is smart!
+        SS -> case decideLE of
+            Yes p -> Yes (leSucc p)
+            No  p -> No $ \p' -> p (lePred p')
+
+instance (SNatI n, SNatI m) => Decidable (LEProof n m) where
+    decide = decideLE
+
+-------------------------------------------------------------------------------
+-- More lemmas
+-------------------------------------------------------------------------------
+
+-- | \(\forall n\ : \mathbb{N}, n \le 0 \to n \equiv 0 \)
+proofZeroLEZero :: LEProof n 'Z -> n :~: 'Z
+proofZeroLEZero LEZero = Refl
diff --git a/src/Data/Type/Nat/LE/ReflStep.hs b/src/Data/Type/Nat/LE/ReflStep.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Nat/LE/ReflStep.hs
@@ -0,0 +1,169 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE EmptyCase             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE StandaloneDeriving    #-}
+{-# LANGUAGE TypeOperators         #-}
+
+{-# LANGUAGE UndecidableInstances  #-}
+module Data.Type.Nat.LE.ReflStep (
+    -- * Relation
+    LEProof (..),
+    fromZeroSucc,
+    toZeroSucc,
+    -- * Decidability
+    decideLE,
+    -- * Lemmas
+    -- ** Constructor like
+    leZero,
+    leSucc,
+    leRefl,
+    leStep,
+    -- ** Partial order
+    leAsym,
+    leTrans,
+    -- ** Total order
+    leSwap,
+    leSwap',
+    -- ** More
+    leStepL,
+    lePred,
+    proofZeroLEZero,
+    ) where
+
+import Data.Type.Dec      (Dec (..), Decidable (..), Neg)
+import Data.Type.Equality
+import Data.Type.Nat
+import Data.Void          (absurd)
+
+import qualified Data.Type.Nat.LE as ZeroSucc
+
+-------------------------------------------------------------------------------
+-- Proof
+-------------------------------------------------------------------------------
+
+-- | An evidence of \(n \le m\). /refl+step/ definition.
+data LEProof n m where
+    LERefl :: LEProof n n
+    LEStep :: LEProof n m -> LEProof n ('S m)
+
+deriving instance Show (LEProof n m)
+
+-- | 'LEProof' values are unique (not @'Boring'@ though!).
+instance Eq (LEProof n m) where
+    _ == _ = True
+
+instance Ord (LEProof n m) where
+    compare _ _ = EQ
+
+-------------------------------------------------------------------------------
+-- Conversion
+-------------------------------------------------------------------------------
+
+-- | Convert from /zero+succ/ to /refl+step/ definition.
+--
+-- Inverse of 'toZeroSucc'.
+--
+fromZeroSucc :: forall n m. SNatI m => ZeroSucc.LEProof n m -> LEProof n m
+fromZeroSucc ZeroSucc.LEZero     = leZero
+fromZeroSucc (ZeroSucc.LESucc p) = case snat :: SNat m of
+    SS -> leSucc (fromZeroSucc p)
+    -- q  -> case q of {} -- for older GHC
+
+-- | Convert /refl+step/ to /zero+succ/ definition.
+--
+-- Inverse of 'fromZeroSucc'.
+--
+toZeroSucc :: SNatI n => LEProof n m -> ZeroSucc.LEProof n m
+toZeroSucc LERefl     = ZeroSucc.leRefl
+toZeroSucc (LEStep p) = ZeroSucc.leStep (toZeroSucc p)
+
+-------------------------------------------------------------------------------
+-- Lemmas
+-------------------------------------------------------------------------------
+
+-- | \(\forall n : \mathbb{N}, 0 \le n \)
+leZero :: forall n. SNatI n => LEProof 'Z n
+leZero = case snat :: SNat n of
+    SZ -> LERefl
+    SS -> LEStep leZero
+
+-- | \(\forall n\, m : \mathbb{N}, n \le m \to 1 + n \le 1 + m \)
+leSucc :: LEProof n m -> LEProof ('S n) ('S m)
+leSucc LERefl     = LERefl
+leSucc (LEStep p) = LEStep (leSucc p)
+
+-- | \(\forall n\, m : \mathbb{N}, 1 + n \le 1 + m \to n \le m \)
+lePred :: LEProof ('S n) ('S m) -> LEProof n m
+lePred LERefl              = LERefl
+lePred (LEStep LERefl)     = LEStep LERefl
+lePred (LEStep (LEStep q)) = LEStep (leStepL q)
+
+-- | \(\forall n : \mathbb{N}, n \le n \)
+leRefl :: LEProof n n
+leRefl = LERefl
+
+-- | \(\forall n\, m : \mathbb{N}, n \le m \to n \le 1 + m \)
+leStep :: LEProof n m -> LEProof n ('S m)
+leStep = LEStep
+
+-- | \(\forall n\, m : \mathbb{N}, 1 + n \le m \to n \le m \)
+leStepL :: LEProof ('S n) m -> LEProof n m
+leStepL LERefl     = LEStep LERefl
+leStepL (LEStep p) = LEStep (leStepL p)
+
+-- | \(\forall n\, m : \mathbb{N}, n \le m \to m \le n \to n \equiv m \)
+leAsym :: LEProof n m -> LEProof m n -> n :~: m
+leAsym LERefl _ = Refl
+leAsym _ LERefl = Refl
+leAsym (LEStep p) (LEStep q) = case leAsym (leStepL p) (leStepL q) of
+    Refl -> Refl
+
+-- | \(\forall n\, m\, p : \mathbb{N}, n \le m \to m \le p \to n \le p \)
+leTrans :: LEProof n m -> LEProof m p -> LEProof n p
+leTrans LERefl     q          = q
+leTrans p          LERefl     = p
+leTrans (LEStep p) (LEStep q) = LEStep $ leTrans p $ leStepL q
+
+-- | \(\forall n\, m : \mathbb{N}, \neg (n \le m) \to 1 + m \le n \)
+leSwap :: forall n m. (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof ('S m) n
+leSwap np = case (snat :: SNat m, snat :: SNat n) of
+    (_,  SZ) -> absurd (np leZero)
+    (SZ, SS) -> leSucc leZero
+    (SS, SS) -> leSucc $ leSwap $ \p -> np $ leSucc p
+
+-- | \(\forall n\, m : \mathbb{N}, n \le m \to \neg (1 + m \le n) \)
+leSwap' :: LEProof n m -> LEProof ('S m) n -> void
+leSwap' p LERefl     = case p of LEStep p' -> leSwap' (leStepL p') LERefl
+leSwap' p (LEStep q) = leSwap' (leStepL p) q
+
+-------------------------------------------------------------------------------
+-- Decidability
+-------------------------------------------------------------------------------
+
+-- | Find the @'LEProof' n m@, i.e. compare numbers.
+decideLE :: forall n m. (SNatI n, SNatI m) => Dec (LEProof n m)
+decideLE = case snat :: SNat n of
+    SZ -> Yes leZero
+    SS -> caseSnm
+  where
+    caseSnm :: forall n' m'. (SNatI n', SNatI m') => Dec (LEProof ('S n') m')
+    caseSnm = case snat :: SNat m' of
+        SZ -> No $ \p -> case p of {} -- ooh, GHC is smart!
+        SS -> case decideLE of
+            Yes p -> Yes (leSucc p)
+            No  p -> No $ \p' -> p (lePred p')
+
+instance (SNatI n, SNatI m) => Decidable (LEProof n m) where
+    decide = decideLE
+
+-------------------------------------------------------------------------------
+-- More lemmas
+---------------------------------------------------------------------------------
+
+-- | \(\forall n\ : \mathbb{N}, n \le 0 \to n \equiv 0 \)
+proofZeroLEZero :: LEProof n 'Z -> n :~: 'Z
+proofZeroLEZero LERefl = Refl
diff --git a/src/Data/Type/Nat/LT.hs b/src/Data/Type/Nat/LT.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Nat/LT.hs
@@ -0,0 +1,68 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
+module Data.Type.Nat.LT (
+    LT (..),
+    LTProof,
+    withLTProof,
+    -- * Lemmas
+    ltReflAbsurd,
+    ltSymAbsurd,
+    ltTrans,
+    ) where
+
+import Data.Type.Nat
+import Data.Type.Nat.LE
+
+-- | An evidence \(n < m\) which is the same as (\1 + n \le m\).
+type LTProof n m = LEProof ('S n) m
+
+-------------------------------------------------------------------------------
+-- Class
+-------------------------------------------------------------------------------
+
+-- | Less-Than-or. \(<\). Well-founded relation on 'Nat'.
+--
+-- GHC can solve this for us!
+--
+-- >>> ltProof :: LTProof Nat0 Nat4
+-- LESucc LEZero
+--
+-- >>> ltProof :: LTProof Nat2 Nat4
+-- LESucc (LESucc (LESucc LEZero))
+--
+-- >>> ltProof :: LTProof Nat3 Nat3
+-- ...
+-- ...error...
+-- ...
+--
+class LT (n :: Nat) (m :: Nat) where
+    ltProof :: LTProof n m
+
+instance LE ('S n) m => LT n m where
+    ltProof = leProof
+
+withLTProof :: LTProof n m -> (LT n m => r) -> r
+withLTProof p f = withLEProof p f -- eta expansion needed for old GHC
+
+-------------------------------------------------------------------------------
+-- Lemmas
+-------------------------------------------------------------------------------
+
+-- | \(\forall n : \mathbb{N}, n < n \to \bot \)
+ltReflAbsurd :: LTProof n n -> a
+ltReflAbsurd (LESucc p) = ltReflAbsurd p
+
+-- | \(\forall n\, m : \mathbb{N}, n < m \to m < n \to \bot \)
+ltSymAbsurd :: LTProof n m -> LTProof m n -> a
+ltSymAbsurd (LESucc p) (LESucc q) = ltSymAbsurd p q
+
+-- | \(\forall n\, m\, p : \mathbb{N}, n < m \to m < p \to n < p \)
+ltTrans :: LTProof n m -> LTProof m p -> LTProof n p
+ltTrans p (LESucc q) = leStep $ leTrans p q