diff --git a/natural-arithmetic.cabal b/natural-arithmetic.cabal
--- a/natural-arithmetic.cabal
+++ b/natural-arithmetic.cabal
@@ -1,6 +1,6 @@
 cabal-version: 2.2
 name: natural-arithmetic
-version: 0.1.0.0
+version: 0.1.1.0
 synopsis: Arithmetic of natural numbers
 description:
   A search for terms like `arithmetic` and `natural` on hackage reveals
diff --git a/src/Arithmetic/Fin.hs b/src/Arithmetic/Fin.hs
--- a/src/Arithmetic/Fin.hs
+++ b/src/Arithmetic/Fin.hs
@@ -10,15 +10,26 @@
   ( -- * Modification
     incrementL
   , incrementR
+  , weaken
   , weakenL
   , weakenR
     -- * Traverse
+    -- | These use the terms @ascend@ and @descend@ rather than the
+    -- more popular @l@ (left) and @r@ (right) that pervade the Haskell
+    -- ecosystem. The general rule is that ascending functions pair
+    -- the initial accumulator with zero with descending functions
+    -- pair the initial accumulator with the last index.
   , ascend
+  , ascend'
   , ascendM
   , ascendM_
+  , descend
+  , descendM
+  , descendM_
   , ascending
   , descending
   , ascendingSlice
+  , descendingSlice
     -- * Absurdities
   , absurd
     -- * Demote
@@ -33,6 +44,7 @@
 
 import qualified Arithmetic.Lt as Lt
 import qualified Arithmetic.Lte as Lte
+import qualified Arithmetic.Equal as Eq
 import qualified Arithmetic.Nat as Nat
 import qualified Arithmetic.Plus as Plus
 
@@ -46,7 +58,8 @@
 incrementL :: forall n m. Nat m -> Fin n -> Fin (m + n)
 incrementL m (Fin i pf) = Fin (Nat.plus m i) (Lt.incrementL @m pf)
 
--- | Weaken the bound by one. This does not change the index.
+-- | Weaken the bound by @m@, adding it to the left-hand side of
+-- the existing bound. This does not change the index.
 weakenL :: forall n m. Fin n -> Fin (m + n)
 weakenL (Fin i pf) = Fin i
   ( Lt.substituteR
@@ -54,26 +67,69 @@
     (Lt.plus pf (Lte.zero @m))
   )
 
--- side of @n@. This does not change the index.
+-- | Weaken the bound by @m@, adding it to the right-hand side of
+-- the existing bound. This does not change the index.
 weakenR :: forall n m. Fin n -> Fin (n + m)
 weakenR (Fin i pf) = Fin i (Lt.plus pf Lte.zero)
 
+-- | Weaken the bound, replacing it by another number greater than
+-- or equal to itself. This does not change the index.
+weaken :: forall n m. (n <= m) -> Fin n -> Fin m
+weaken lt (Fin i pf) = Fin i (Lt.transitiveNonstrictR pf lt)
+
 -- | A finite set of no values is impossible.
 absurd :: Fin 0 -> void
 absurd (Fin _ pf) = Lt.absurd pf
 
--- | Strict fold over the numbers bounded by @n@ in ascending
--- order. For convenince, this differs from @foldl'@ in the
--- order of the parameters differs from @foldl@. Roughly:
+-- | Fold over the numbers bounded by @n@ in descending
+-- order. This is lazy in the accumulator. For convenince,
+-- this differs from @foldr@ in the order of the parameters.
 --
+-- > descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))
+descend :: forall a n.
+     Nat n -- ^ Upper bound
+  -> a -- ^ Initial accumulator
+  -> (Fin n -> a -> a) -- ^ Update accumulator
+  -> a
+{-# inline descend #-}
+descend !n b0 f = go Nat.zero
+  where
+  go :: Nat m -> a
+  go !m = case m <? n of
+    Nothing -> b0
+    Just lt -> f (Fin m lt) (go (Nat.succ m))
+
+-- | Fold over the numbers bounded by @n@ in ascending order. This
+-- is lazy in the accumulator.
+--
 -- > ascend 4 z f = f 3 (f 2 (f 1 (f 0 z)))
 ascend :: forall a n.
+     Nat n
+  -> a
+  -> (Fin n -> a -> a)
+  -> a
+{-# inline ascend #-}
+ascend !n !b0 f = go n Lte.reflexive
+  where
+    go :: Nat p -> (p <= n) -> a
+    go !m pLteEn = case Nat.monus m Nat.one of
+      Nothing -> b0
+      Just (Difference (mpred :: Nat c) cPlusOneEqP) ->
+        let !cLtEn = descendLemma cPlusOneEqP pLteEn
+        in f (Fin mpred cLtEn) (go mpred (Lte.fromStrict cLtEn))
+
+-- | Strict fold over the numbers bounded by @n@ in ascending
+-- order. For convenince, this differs from @foldl'@ in the
+-- order of the parameters.
+--
+-- > ascend' 4 z f = f 3 (f 2 (f 1 (f 0 z)))
+ascend' :: forall a n.
      Nat n -- ^ Upper bound
   -> a -- ^ Initial accumulator
   -> (Fin n -> a -> a) -- ^ Update accumulator
   -> a
-{-# inline ascend #-}
-ascend !n !b0 f = go Nat.zero b0
+{-# inline ascend' #-}
+ascend' !n !b0 f = go Nat.zero b0
   where
   go :: Nat m -> a -> a
   go !m !b = case m <? n of
@@ -83,7 +139,7 @@
 -- | Strict monadic left fold over the numbers bounded by @n@
 -- in ascending order. Roughly:
 --
--- > ascendM 4 z f =
+-- > ascendM 4 z0 f =
 -- >   f 0 z0 >>= \z1 ->
 -- >   f 1 z1 >>= \z2 ->
 -- >   f 2 z2 >>= \z3 ->
@@ -117,10 +173,59 @@
     Nothing -> pure ()
     Just lt -> f (Fin m lt) *> go (Nat.succ m)
 
+descendLemma :: forall a b c. a + 1 :=: b -> b <= c -> a < c
+{-# inline descendLemma #-}
+descendLemma !aPlusOneEqB !bLteC = id
+  $ Lt.transitiveNonstrictR
+      (Lt.substituteR (Plus.commutative @1 @a)
+      (Lt.plus Lt.zero Lte.reflexive))
+  $ Lte.substituteL (Eq.symmetric aPlusOneEqB) bLteC
+
+-- | Strict monadic left fold over the numbers bounded by @n@
+-- in descending order. Roughly:
+--
+-- > descendM 4 z f =
+-- >   f 3 z0 >>= \z1 ->
+-- >   f 2 z1 >>= \z2 ->
+-- >   f 1 z2 >>= \z3 ->
+-- >   f 0 z3
+descendM :: forall m a n. Monad m
+  => Nat n
+  -> a
+  -> (Fin n -> a -> m a)
+  -> m a
+{-# inline descendM #-}
+descendM !n !b0 f = go n Lte.reflexive b0
+  where
+    go :: Nat p -> p <= n -> a -> m a
+    go !m pLteEn !b = case Nat.monus m Nat.one of
+      Nothing -> pure b
+      Just (Difference (mpred :: Nat c) cPlusOneEqP) ->
+        let !cLtEn = descendLemma cPlusOneEqP pLteEn
+        in go mpred (Lte.fromStrict cLtEn) =<< f (Fin mpred cLtEn) b
+
+-- | Monadic traversal of the numbers bounded by @n@
+-- in descending order.
+--
+-- > descendM_ 4 f = f 3 *> f 2 *> f 1 *> f 0
+descendM_ :: forall m a n. Applicative m
+  => Nat n -- ^ Upper bound
+  -> (Fin n -> m a) -- ^ Effectful interpretion
+  -> m ()
+{-# inline descendM_ #-}
+descendM_ !n f = go n Lte.reflexive
+  where
+  go :: Nat p -> p <= n -> m ()
+  go !m !pLteEn = case Nat.monus m Nat.one of
+    Nothing -> pure ()
+    Just (Difference (mpred :: Nat c) cPlusOneEqP) ->
+      let !cLtEn = descendLemma cPlusOneEqP pLteEn
+      in f (Fin mpred cLtEn) *> go mpred (Lte.fromStrict cLtEn)
+
 -- | Generate all values of a finite set in ascending order.
 --
 -- >>> ascending (Nat.constant @3)
--- [0, 1, 2]
+-- [Fin 0,Fin 1,Fin 2]
 ascending :: forall n. Nat n -> [Fin n]
 ascending !n = go Nat.zero
   where
@@ -132,42 +237,68 @@
 -- | Generate all values of a finite set in descending order.
 --
 -- >>> descending (Nat.constant @3)
--- [2, 1, 0]
+-- [Fin 2,Fin 1,Fin 0]
 descending :: forall n. Nat n -> [Fin n]
-descending n = go n Lte.reflexive
+descending !n = go n Lte.reflexive
   where
-    go :: forall m. Nat m -> (m <= n) -> [Fin n]
-    go !m !lt = case Nat.monus m Nat.one of
+    go :: Nat p -> (p <= n) -> [Fin n]
+    go !m !pLteEn = case Nat.monus m Nat.one of
       Nothing -> []
-      Just (Difference mpred eq) -> go2 lt mpred eq
-    go2 :: forall m c. (m <= n) -> Nat c -> (c + 1 :=: m) -> [Fin n]
-    go2 !lt !c !eq = 
-        let ceeLtEm :: c < m
-            ceeLtEm = id
-              $ Lt.substituteR eq
-              $ Lt.substituteL Plus.zeroL
-              $ Lt.incrementL @c Lt.zero
-         in Fin c (Lt.transitiveNonstrictR ceeLtEm lt) : go c
-              (Lte.transitive (Lte.substituteR eq (Lte.weakenR @1 (Lte.reflexive @c))) lt)
+      Just (Difference (mpred :: Nat c) cPlusOneEqP) ->
+        let !cLtEn = descendLemma cPlusOneEqP pLteEn
+        in Fin mpred cLtEn : go mpred (Lte.fromStrict cLtEn)
 
--- | Generate 'len' values starting from 'off'.
+-- | Generate 'len' values starting from 'off' in ascending order.
 --
--- >>> slice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6)
--- [2, 3, 4]
-ascendingSlice :: forall n off len.
-     Nat off
+-- >>> ascendingSlice (Nat.constant @2) (Nat.constant @3) (Lte.constant @_ @6)
+-- [Fin 2,Fin 3,Fin 4]
+ascendingSlice
+  :: forall n off len
+  .  Nat off
   -> Nat len
-  -> (off + len < n)
+  -> off + len <= n
   -> [Fin n]
-ascendingSlice off len !offPlusLenLtEn = go Nat.zero
+{-# inline ascendingSlice #-}
+ascendingSlice off len !offPlusLenLteEn = go Nat.zero
   where
     go :: Nat m -> [Fin n]
     go !m = case m <? len of
       Nothing -> []
       Just emLtLen ->
         let !offPlusEmLtOffPlusLen = Lt.incrementL @off emLtLen
-            !offPlusEmLtEn = Lt.transitive offPlusEmLtOffPlusLen offPlusLenLtEn
+            !offPlusEmLtEn = Lt.transitiveNonstrictR offPlusEmLtOffPlusLen offPlusLenLteEn
          in Fin (Nat.plus off m) offPlusEmLtEn : go (Nat.succ m)
+
+-- | Generate 'len' values starting from 'off + len - 1' in descending order.
+--
+-- >>> descendingSlice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6)
+-- [Fin 4,Fin 3,Fin 2]
+descendingSlice
+  :: forall n off len
+  .  Nat off
+  -> Nat len
+  -> off + len <= n
+  -> [Fin n]
+{-# inline descendingSlice #-}
+descendingSlice !off !len !offPlusLenLteEn =
+  go len Lte.reflexive
+  where
+    go :: Nat m -> m <= len -> [Fin n]
+    go !m !mLteEn = case Nat.monus m Nat.one of
+      Nothing -> []
+      Just (Difference (mpred :: Nat c) cPlusOneEqEm) ->
+        let !cLtLen = Lt.transitiveNonstrictR
+              (Lt.substituteR (Plus.commutative @1 @c) (Lt.plus Lt.zero Lte.reflexive))
+              -- c < c + 1
+              (Lte.substituteL (Eq.symmetric cPlusOneEqEm) mLteEn)
+              -- c + 1 <= len
+            !cPlusOffLtEn = Lt.transitiveNonstrictR
+              (Lt.substituteR
+                (Plus.commutative @len @off)
+                (Lt.plus cLtLen (Lte.reflexive @off)))
+              -- c + off < off + len
+              offPlusLenLteEn
+        in Fin (mpred `Nat.plus` off) cPlusOffLtEn : go mpred (Lte.fromStrict cLtLen)
 
 -- | Extract the 'Int' from a 'Fin n'. This is intended to be used
 -- at a boundary where a safe interface meets the unsafe primitives
diff --git a/src/Arithmetic/Lt.hs b/src/Arithmetic/Lt.hs
--- a/src/Arithmetic/Lt.hs
+++ b/src/Arithmetic/Lt.hs
@@ -21,6 +21,9 @@
   , transitive
   , transitiveNonstrictL
   , transitiveNonstrictR
+    -- * Convert to Inequality
+  , toLteL
+  , toLteR
     -- * Absurdities
   , absurd
     -- * Integration with GHC solver
@@ -33,9 +36,15 @@
 
 import qualified GHC.TypeNats as GHC
 
--- | Replace the right-hand side of a strict inequality
+toLteR :: (a < b) -> (a + 1 <= b)
+toLteR Lt = Lte
+
+toLteL :: (a < b) -> (1 + a <= b)
+toLteL Lt = Lte
+
+-- | Replace the left-hand side of a strict inequality
 -- with an equal number.
-substituteL :: (b :=: c) -> (a < b) -> (a < c)
+substituteL :: (b :=: c) -> (b < a) -> (c < a)
 substituteL Eq Lt = Lt
 
 -- | Replace the right-hand side of a strict inequality
diff --git a/src/Arithmetic/Lte.hs b/src/Arithmetic/Lte.hs
--- a/src/Arithmetic/Lte.hs
+++ b/src/Arithmetic/Lte.hs
@@ -35,9 +35,9 @@
 
 import qualified GHC.TypeNats as GHC
 
--- | Replace the right-hand side of a strict inequality
+-- | Replace the left-hand side of a strict inequality
 -- with an equal number.
-substituteL :: (b :=: c) -> (a <= b) -> (a <= c)
+substituteL :: (b :=: c) -> (b <= a) -> (c <= a)
 substituteL Eq Lte = Lte
 
 -- | Replace the right-hand side of a strict inequality
diff --git a/src/Arithmetic/Nat.hs b/src/Arithmetic/Nat.hs
--- a/src/Arithmetic/Nat.hs
+++ b/src/Arithmetic/Nat.hs
@@ -2,6 +2,7 @@
 {-# language ExplicitForAll #-}
 {-# language KindSignatures #-}
 {-# language MagicHash #-}
+{-# language RankNTypes #-}
 {-# language ScopedTypeVariables #-}
 {-# language TypeOperators #-}
 
@@ -16,15 +17,19 @@
   , testEqual
   , testLessThan
   , testLessThanEqual
+  , testZero
   , (=?)
   , (<?)
   , (<=?)
     -- * Constants
   , zero
   , one
+  , two
+  , three
   , constant
-    -- * Demote
+    -- * Convert
   , demote
+  , with
   ) where
 
 import Prelude hiding (succ)
@@ -67,6 +72,12 @@
   then Just Eq
   else Nothing
 
+-- | Is zero equal to this number or less than it?
+testZero :: Nat a -> Either (0 :=: a) (0 < a)
+testZero (Nat x) = case x of
+  0 -> Left Eq
+  _ -> Right Lt
+
 -- | Add two numbers.
 plus :: Nat a -> Nat b -> Nat (a + b)
 plus (Nat x) (Nat y) = Nat (x + y)
@@ -90,6 +101,14 @@
 one :: Nat 1
 one = Nat 1
 
+-- | The number two.
+two :: Nat 2
+two = Nat 2
+
+-- | The number three.
+three :: Nat 3
+three = Nat 3
+
 -- | Use GHC's built-in type-level arithmetic to create a witness
 -- of a type-level number. This only reduces if the number is a
 -- constant.
@@ -101,3 +120,10 @@
 -- on top of which it is built.
 demote :: Nat n -> Int
 demote (Nat n) = n
+
+-- | Run a computation on a witness of a type-level number. The
+-- argument 'Int' must be greater than or equal to zero. This is
+-- not checked. Failure to upload this invariant will lead to a
+-- segfault.
+with :: Int -> (forall n. Nat n -> a) -> a
+with i f = f (Nat i)
diff --git a/src/Arithmetic/Types.hs b/src/Arithmetic/Types.hs
--- a/src/Arithmetic/Types.hs
+++ b/src/Arithmetic/Types.hs
@@ -7,6 +7,7 @@
 
 module Arithmetic.Types
   ( Nat
+  , WithNat(..)
   , Difference(..)
   , Fin(..)
   , type (<)
@@ -20,6 +21,9 @@
 import GHC.TypeNats (type (+))
 
 import qualified GHC.TypeNats as GHC
+
+data WithNat :: (GHC.Nat -> Type) -> Type where
+  WithNat :: Nat n -> f n -> WithNat f
 
 -- | A finite set of 'n' elements. 'Fin n = { 0 .. n - 1 }'
 data Fin :: GHC.Nat -> Type where
diff --git a/src/Arithmetic/Unsafe.hs b/src/Arithmetic/Unsafe.hs
--- a/src/Arithmetic/Unsafe.hs
+++ b/src/Arithmetic/Unsafe.hs
@@ -1,8 +1,11 @@
 {-# language DataKinds #-}
+{-# language DerivingStrategies #-}
 {-# language ExplicitNamespaces #-}
 {-# language GADTSyntax #-}
+{-# language GeneralizedNewtypeDeriving #-}
 {-# language KindSignatures #-}
 {-# language RoleAnnotations #-}
+{-# language StandaloneDeriving #-}
 {-# language TypeOperators #-}
 
 module Arithmetic.Unsafe
@@ -33,6 +36,8 @@
 -- | A value-level representation of a natural number @n@.
 newtype Nat (n :: GHC.Nat) = Nat { getNat :: Int }
 type role Nat nominal
+
+deriving newtype instance Show (Nat n)
 
 -- | Proof that the first argument is strictly less than the
 -- second argument.