diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,3 +1,11 @@
+## 0.2.1
+
+- Add `boring` instances
+- Explicitly implement `>=` and `>` for `Nat`.
+- `<=`, `>=` and `min` for `Nat` are lazier
+- Add `NFData (SNat n)` instance
+- Add `GEq`, `GCompare`, `GNFData`, `GShow` (from `some` package) instances for `SNat`.
+
 ## 0.2
 
 - `SNat` is now what was called `InlineInduction`.
diff --git a/fin.cabal b/fin.cabal
--- a/fin.cabal
+++ b/fin.cabal
@@ -1,6 +1,6 @@
 cabal-version:      >=1.10
 name:               fin
-version:            0.2
+version:            0.2.1
 synopsis:           Nat and Fin: peano naturals and finite numbers
 category:           Data, Dependent Types, Singletons, Math
 description:
@@ -65,6 +65,7 @@
    || ==8.8.4
    || ==8.10.4
    || ==9.0.1
+   || ==9.2.1
 
 source-repository head
   type:     git
@@ -86,18 +87,20 @@
 
   other-modules:    TrustworthyCompat
   build-depends:
-      base           >=4.7     && <4.16
+      base           >=4.7     && <4.17
+    , boring         >=0.2     && <0.3
     , dec            >=0.0.4   && <0.1
     , deepseq        >=1.3.0.2 && <1.5
-    , hashable       >=1.2.7.0 && <1.4
+    , hashable       >=1.2.7.0 && <1.5
     , QuickCheck     >=2.13.2  && <2.15
+    , some           >=1.0.3   && <1.1
     , universe-base  >=1.1.2   && <1.2
 
   if !impl(ghc >=8.2)
     build-depends: bifunctors >=5.5.3 && <5.6
 
   if !impl(ghc >=8.0)
-    build-depends: semigroups >=0.18.5 && <0.20
+    build-depends: semigroups >=0.18.5 && <0.21
 
   if !impl(ghc >=7.10)
     build-depends:
diff --git a/src/Data/Fin.hs b/src/Data/Fin.hs
--- a/src/Data/Fin.hs
+++ b/src/Data/Fin.hs
@@ -61,6 +61,7 @@
 import GHC.Exception      (ArithException (..), throw)
 import Numeric.Natural    (Natural)
 
+import qualified Data.Boring           as Boring
 import qualified Data.List.NonEmpty    as NE
 import qualified Data.Type.Nat         as N
 import qualified Data.Universe.Class   as U
@@ -213,6 +214,14 @@
     hashWithSalt salt = hashWithSalt salt . cata (0 :: Integer) succ
 
 -------------------------------------------------------------------------------
+-- Boring
+-------------------------------------------------------------------------------
+
+-- | @since 0.2.1
+instance n ~ 'Z => Boring.Absurd (Fin n) where
+    absurd = absurd
+
+-------------------------------------------------------------------------------
 -- QuickCheck
 -------------------------------------------------------------------------------
 
@@ -239,8 +248,8 @@
 
 instance (n ~ 'S m, N.SNatI m) => QC.Function (Fin n) where
     function = case N.snat :: N.SNat m of
-        N.SZ -> QC.functionMap (\FZ -> ()) (\() -> FZ)
-        N.SS -> QC.functionMap isMin       (maybe FZ FS)
+        N.SZ -> QC.functionMap (\_ -> ()) (\() -> FZ)
+        N.SS -> QC.functionMap isMin      (maybe FZ FS)
 
 -- TODO: https://github.com/nick8325/quickcheck/pull/283
 -- newtype Fun b m = Fun { getFun :: (Fin ('S m) -> b) -> Fin ('S m) QC.:-> b }
diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
--- a/src/Data/Nat.hs
+++ b/src/Data/Nat.hs
@@ -63,18 +63,15 @@
     compare (S _) Z     = GT
     compare (S n) (S m) = compare n m
 
-    Z   < Z   = False
-    Z   < S _ = True
-    S _ < Z   = False
-    S n < S m = n < m
-
-    Z   <= Z   = True
-    Z   <= S _ = True
+    Z   <= _   = True
     S _ <= Z   = False
     S n <= S m = n <= m
 
-    min Z     Z     = Z
-    min Z     (S _) = Z
+    n <  m = not (m <= n)
+    n >  m = not (n <= m)
+    n >= m = m <= n
+
+    min Z     _     = Z
     min (S _) Z     = Z
     min (S n) (S m) = S (min n m)
 
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
@@ -38,6 +38,7 @@
     eqNat,
     EqNat,
     discreteNat,
+    cmpNat,
     -- * Induction
     induction1,
     -- ** Example: unfoldedFix
@@ -64,20 +65,21 @@
     proofMultNOne,
     )  where
 
-import Data.Function   (fix)
-import Data.Proxy      (Proxy (..))
-import Data.Type.Dec   (Dec (..))
-import Data.Typeable   (Typeable)
-import Numeric.Natural (Natural)
+import Control.DeepSeq   (NFData (..))
+import Data.Boring       (Boring (..))
+import Data.Function     (fix)
+import Data.GADT.Compare (GCompare (..), GEq (..), GOrdering (..))
+import Data.GADT.DeepSeq (GNFData (..))
+import Data.GADT.Show    (GShow (..))
+import Data.Proxy        (Proxy (..))
+import Data.Type.Dec     (Dec (..))
+import Data.Typeable     (Typeable)
+import Numeric.Natural   (Natural)
 
 import qualified GHC.TypeLits as GHC
 
 import Unsafe.Coerce (unsafeCoerce)
 
-#if !MIN_VERSION_base(4,11,0)
-import Data.Type.Equality (type (==))
-#endif
-
 import Data.Nat
 import TrustworthyCompat
 
@@ -88,6 +90,7 @@
 -- >>> import Data.Type.Equality
 -- >>> import Control.Applicative (Const (..))
 -- >>> import Data.Coerce (coerce)
+-- >>> import Data.GADT.Compare (GOrdering (..))
 
 -------------------------------------------------------------------------------
 -- SNat
@@ -246,6 +249,65 @@
 type instance n == m = EqNat n m
 #endif
 
+-- | @since 0.2.1
+instance SNatI n => Boring (SNat n) where
+    boring = snat
+
+-- | @since 0.2.1
+instance GShow SNat where
+    gshowsPrec = showsPrec
+
+-- | @since 0.2.1
+instance NFData (SNat n) where
+    rnf SZ = ()
+    rnf SS = ()
+
+-- | @since 0.2.1
+instance GNFData SNat where
+    grnf = rnf
+
+-- | @since 0.2.1
+instance GEq SNat where
+    geq = testEquality
+
+-- | @since 0.2.1
+instance GCompare SNat where
+    gcompare SZ SZ = GEQ
+    gcompare SZ SS = GLT
+    gcompare SS SZ = GGT
+    gcompare SS SS = cmpNat
+
+-- | Decide equality of type-level numbers.
+--
+-- >>> cmpNat :: GOrdering Nat3 (Plus Nat1 Nat2)
+-- GEQ
+--
+-- >>> cmpNat :: GOrdering Nat3 (Mult Nat2 Nat2)
+-- GLT
+--
+-- >>> cmpNat :: GOrdering Nat5 (Mult Nat2 Nat2)
+-- GGT
+--
+cmpNat :: forall n m. (SNatI n, SNatI m) => GOrdering n m
+cmpNat = getNatCmp $ induction (NatCmp start) (\p -> NatCmp (step p)) where
+    start :: forall p. SNatI p => GOrdering 'Z p
+    start = case snat :: SNat p of
+        SZ -> GEQ
+        SS -> GLT
+
+    step :: forall p q. SNatI q => NatCmp p -> GOrdering ('S p) q
+    step hind = case snat :: SNat q of
+        SZ -> GGT
+        SS -> step' hind
+
+    step' :: forall p q. SNatI q => NatCmp p -> GOrdering ('S p) ('S q)
+    step' (NatCmp hind) = case hind :: GOrdering p q of
+        GEQ -> GEQ
+        GLT -> GLT
+        GGT -> GGT
+
+newtype NatCmp n = NatCmp { getNatCmp :: forall m. SNatI m => GOrdering n m }
+
 -------------------------------------------------------------------------------
 -- Induction
 -------------------------------------------------------------------------------
@@ -295,7 +357,7 @@
 -- | Convert to GHC 'GHC.Nat'.
 --
 -- >>> :kind! ToGHC Nat5
--- ToGHC Nat5 :: GHC.Nat
+-- ToGHC Nat5 :: GHC.Nat...
 -- = 5
 --
 type family ToGHC (n :: Nat) :: GHC.Nat where
@@ -343,13 +405,13 @@
 
 -- | Division by two. 'False' is 0 and 'True' is 1 as a remainder.
 --
--- >>> :kind! DivMod2 Nat7
--- DivMod2 Nat7 :: (Nat, Bool)
--- = '( 'S ('S ('S 'Z)), 'True)
+-- >>> :kind! DivMod2 Nat7 == '(Nat3, True)
+-- DivMod2 Nat7 == '(Nat3, True) :: Bool
+-- = 'True
 --
--- >>> :kind! DivMod2 Nat4
--- DivMod2 Nat4 :: (Nat, Bool)
--- = '( 'S ('S 'Z), 'False)
+-- >>> :kind! DivMod2 Nat4 == '(Nat2, False)
+-- DivMod2 Nat4 == '(Nat2, False) :: Bool
+-- = 'True
 --
 type family DivMod2 (n :: Nat) :: (Nat, Bool) where
     DivMod2 'Z          = '( 'Z, 'False)
diff --git a/src/Data/Type/Nat/LE.hs b/src/Data/Type/Nat/LE.hs
--- a/src/Data/Type/Nat/LE.hs
+++ b/src/Data/Type/Nat/LE.hs
@@ -49,9 +49,9 @@
     proofZeroLEZero,
     ) where
 
-import Data.Type.Dec      (Dec (..), Decidable (..), Neg)
-import Data.Typeable      (Typeable)
-import Data.Void          (absurd)
+import Data.Boring   (Boring (..), Absurd (..))
+import Data.Type.Dec (Dec (..), Decidable (..), Neg)
+import Data.Typeable (Typeable)
 
 import Data.Type.Nat
 import TrustworthyCompat
@@ -162,6 +162,18 @@
 --
 leSwap' :: LEProof n m -> LEProof ('S m) n -> void
 leSwap' p (LESucc q) = case p of LESucc p' -> leSwap' p' q
+
+-------------------------------------------------------------------------------
+-- Boring
+-------------------------------------------------------------------------------
+
+-- | @since 0.2.1
+instance LE n m => Boring (LEProof n m) where
+    boring = leProof
+
+-- | @since 0.2.1
+instance (LE m n, n' ~ 'S n) => Absurd (LEProof n' m) where
+    absurd = leSwap' leProof
 
 -------------------------------------------------------------------------------
 -- Dedidablity
diff --git a/src/Data/Type/Nat/LE/ReflStep.hs b/src/Data/Type/Nat/LE/ReflStep.hs
--- a/src/Data/Type/Nat/LE/ReflStep.hs
+++ b/src/Data/Type/Nat/LE/ReflStep.hs
@@ -36,9 +36,9 @@
     proofZeroLEZero,
     ) where
 
+import Data.Boring   (Absurd (..), Boring (..))
 import Data.Type.Dec (Dec (..), Decidable (..), Neg)
 import Data.Typeable (Typeable)
-import Data.Void     (absurd)
 
 import qualified Control.Category as C
 
@@ -150,6 +150,18 @@
 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
+
+-------------------------------------------------------------------------------
+-- Boring
+-------------------------------------------------------------------------------
+
+-- | @since 0.2.1
+instance (ZeroSucc.LE n m, SNatI m) => Boring (LEProof n m) where
+    boring = fromZeroSucc ZeroSucc.leProof
+
+-- | @since 0.2.1
+instance (ZeroSucc.LE m n, n' ~ 'S n, SNatI n) => Absurd (LEProof n' m) where
+    absurd = ZeroSucc.leSwap' ZeroSucc.leProof . toZeroSucc
 
 -------------------------------------------------------------------------------
 -- Decidability
diff --git a/src/TrustworthyCompat.hs b/src/TrustworthyCompat.hs
--- a/src/TrustworthyCompat.hs
+++ b/src/TrustworthyCompat.hs
@@ -1,9 +1,11 @@
-{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE Trustworthy        #-}
 module TrustworthyCompat (
     (:~:) (..),
     TestEquality (..),
     coerce,
+    type (==),
 ) where
 
 import Data.Coerce        (coerce)
-import Data.Type.Equality (TestEquality (..), (:~:) (..))
+import Data.Type.Equality (TestEquality (..), type (==), (:~:) (..))