diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,12 @@
 # Revision history for natural-arithmetic
 
+## 0.1.4.0 -- 2023-05-31
+
+* Add unboxed Nat type
+* Add nominal role for Fin# type constructor. Technically, this is a breaking
+  change, but if anyone was using coerce on a Fin#, they were already in a
+  bunch of trouble. So, there is not going to be a major version bump for this.
+
 ## 0.1.3.0 -- 2022-05-23
 
 * Add strict variant of descend.
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.3.0
+version: 0.1.4.0
 synopsis: Arithmetic of natural numbers
 description:
   A search for terms like `arithmetic` and `natural` on hackage reveals
diff --git a/src/Arithmetic/Equal.hs b/src/Arithmetic/Equal.hs
--- a/src/Arithmetic/Equal.hs
+++ b/src/Arithmetic/Equal.hs
@@ -13,10 +13,13 @@
 import GHC.TypeNats (type (+))
 
 symmetric :: (m :=: n) -> (n :=: m)
+{-# inline symmetric #-}
 symmetric Eq = Eq
 
 plusL :: forall c m n. (m :=: n) -> (c + m :=: c + n)
+{-# inline plusL #-}
 plusL Eq = Eq
 
 plusR :: forall c m n. (m :=: n) -> (m + c :=: n + c)
+{-# inline plusR #-}
 plusR Eq = Eq
diff --git a/src/Arithmetic/Fin.hs b/src/Arithmetic/Fin.hs
--- a/src/Arithmetic/Fin.hs
+++ b/src/Arithmetic/Fin.hs
@@ -4,6 +4,7 @@
 {-# language GADTs #-}
 {-# language KindSignatures #-}
 {-# language MagicHash #-}
+{-# language RankNTypes #-}
 {-# language ScopedTypeVariables #-}
 {-# language TypeApplications #-}
 {-# language TypeOperators #-}
@@ -22,8 +23,12 @@
     -- pair the initial accumulator with the last index.
   , ascend
   , ascend'
+  , ascendFrom'
+  , ascendFrom'#
   , ascendM
+  , ascendM#
   , ascendM_
+  , ascendM_#
   , descend
   , descend'
   , descendM
@@ -36,6 +41,11 @@
   , absurd
     -- * Demote
   , demote
+    -- * Deconstruct
+  , with
+  , with#
+    -- * Construct
+  , construct#
     -- * Lift and Unlift
   , lift
   , unlift
@@ -44,7 +54,7 @@
 import Prelude hiding (last)
 
 import Arithmetic.Nat ((<?))
-import Arithmetic.Types (Fin(..),Difference(..),Nat,type (<), type (<=), type (:=:))
+import Arithmetic.Types (Fin(..),Fin#,Difference(..),Nat,Nat#,type (<), type (<=), type (:=:))
 import GHC.Exts (Int(I#))
 import GHC.TypeNats (type (+))
 
@@ -169,6 +179,34 @@
     Nothing -> b
     Just lt -> go (Nat.succ m) (f (Fin m lt) b)
 
+-- | Generalization of @ascend'@ that lets the caller pick the starting index:
+--
+-- > ascend' === ascendFrom' 0
+ascendFrom' :: forall a m n.
+     Nat m -- ^ Index to start at
+  -> Nat n -- ^ Number of steps to take
+  -> a -- ^ Initial accumulator
+  -> (Fin (m + n) -> a -> a) -- ^ Update accumulator
+  -> a
+{-# inline ascendFrom' #-}
+ascendFrom' !m0 !n !b0 f = go m0 b0
+  where
+  end = Nat.plus m0 n
+  go :: Nat k -> a -> a
+  go !m !b = case m <? end of
+    Nothing -> b
+    Just lt -> go (Nat.succ m) (f (Fin m lt) b)
+
+-- | Variant of @ascendFrom'@ with unboxed arguments.
+ascendFrom'# :: forall a m n.
+     Nat# m -- ^ Index to start at
+  -> Nat# n -- ^ Number of steps to take
+  -> a -- ^ Initial accumulator
+  -> (Fin# (m + n) -> a -> a) -- ^ Update accumulator
+  -> a
+{-# inline ascendFrom'# #-}
+ascendFrom'# !m0 !n !b0 f = ascendFrom' (Nat.lift m0) (Nat.lift n) b0 (\ix -> f (unlift ix))
+
 -- | Strict monadic left fold over the numbers bounded by @n@
 -- in ascending order. Roughly:
 --
@@ -190,6 +228,16 @@
     Nothing -> pure b
     Just lt -> go (Nat.succ m) =<< f (Fin m lt) b
 
+-- | Variant of @ascendM@ that takes an unboxed Nat and provides
+-- an unboxed Fin to the callback.
+ascendM# :: forall m a n. Monad m
+  => Nat# n -- ^ Upper bound
+  -> a -- ^ Initial accumulator
+  -> (Fin# n -> a -> m a) -- ^ Update accumulator
+  -> m a
+{-# inline ascendM# #-}
+ascendM# n !a0 f = ascendM (Nat.lift n) a0 (\ix a -> f (unlift ix) a)
+
 -- | Monadic traversal of the numbers bounded by @n@
 -- in ascending order.
 --
@@ -206,6 +254,15 @@
     Nothing -> pure ()
     Just lt -> f (Fin m lt) *> go (Nat.succ m)
 
+-- | Variant of @ascendM_@ that takes an unboxed Nat and provides
+-- an unboxed Fin to the callback.
+ascendM_# :: forall m a n. Monad m
+  => Nat# n -- ^ Upper bound
+  -> (Fin# n -> m a) -- ^ Update accumulator
+  -> m ()
+{-# inline ascendM_# #-}
+ascendM_# n f = ascendM_ (Nat.lift n) (\ix -> f (unlift ix))
+
 descendLemma :: forall a b c. a + 1 :=: b -> b <= c -> a < c
 {-# inline descendLemma #-}
 descendLemma !aPlusOneEqB !bLteC = id
@@ -347,3 +404,17 @@
 unlift :: Fin n -> Unsafe.Fin# n
 {-# inline unlift #-}
 unlift (Fin (Unsafe.Nat (I# i)) _) = Unsafe.Fin# i
+
+-- | Consume the natural number and the proof in the Fin.
+with :: Fin n -> (forall i. (i < n) -> Nat i -> a) -> a
+{-# inline with #-}
+with (Fin i lt) f = f lt i
+
+-- | Variant of 'with' for unboxed argument and result types.
+with# :: Fin# n -> (forall i. (i < n) -> Nat# i -> a) -> a
+{-# inline with# #-}
+with# (Unsafe.Fin# i) f = f Unsafe.Lt (Unsafe.Nat# i)
+
+construct# :: (i < n) -> Nat# i -> Fin# n
+{-# inline construct# #-}
+construct# _ (Unsafe.Nat# x) = Unsafe.Fin# x
diff --git a/src/Arithmetic/Lt.hs b/src/Arithmetic/Lt.hs
--- a/src/Arithmetic/Lt.hs
+++ b/src/Arithmetic/Lt.hs
@@ -1,3 +1,4 @@
+{-# language AllowAmbiguousTypes #-}
 {-# language DataKinds #-}
 {-# language ExplicitForAll #-}
 {-# language KindSignatures #-}
@@ -13,6 +14,9 @@
     -- * Increment
   , incrementL
   , incrementR
+    -- * Decrement
+  , decrementL
+  , decrementR
     -- * Weaken
   , weakenL
   , weakenR
@@ -21,6 +25,9 @@
   , transitive
   , transitiveNonstrictL
   , transitiveNonstrictR
+    -- * Multiplication and Division
+  , reciprocalA
+  , reciprocalB
     -- * Convert to Inequality
   , toLteL
   , toLteR
@@ -37,72 +44,112 @@
 import qualified GHC.TypeNats as GHC
 
 toLteR :: (a < b) -> (a + 1 <= b)
+{-# inline toLteR #-}
 toLteR Lt = Lte
 
 toLteL :: (a < b) -> (1 + a <= b)
+{-# inline toLteL #-}
 toLteL Lt = Lte
 
 -- | Replace the left-hand side of a strict inequality
 -- with an equal number.
 substituteL :: (b :=: c) -> (b < a) -> (c < a)
+{-# inline substituteL #-}
 substituteL Eq Lt = Lt
 
 -- | Replace the right-hand side of a strict inequality
 -- with an equal number.
 substituteR :: (b :=: c) -> (a < b) -> (a < c)
+{-# inline substituteR #-}
 substituteR Eq Lt = Lt
 
 -- | Add a strict inequality to a nonstrict inequality.
 plus :: (a < b) -> (c <= d) -> (a + c < b + d)
+{-# inline plus #-}
 plus Lt Lte = Lt
 
 -- | Add a constant to the left-hand side of both sides of
 -- the strict inequality.
 incrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
   (a < b) -> (c + a < c + b)
+{-# inline incrementL #-}
 incrementL Lt = Lt
 
 -- | Add a constant to the right-hand side of both sides of
 -- the strict inequality.
 incrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
   (a < b) -> (a + c < b + c)
+{-# inline incrementR #-}
 incrementR Lt = Lt
 
+-- | Subtract a constant from the left-hand side of both sides of
+-- the inequality. This is the opposite of 'incrementL'.
+decrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (c + a < c + b) -> (a < b)
+{-# inline decrementL #-}
+decrementL Lt = Lt
+
+-- | Subtract a constant from the right-hand side of both sides of
+-- the inequality. This is the opposite of 'incrementR'.
+decrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a + c < b + c) -> (a < b)
+{-# inline decrementR #-}
+decrementR Lt = Lt
+
 -- | Add a constant to the left-hand side of the right-hand side of
 -- the strict inequality.
 weakenL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
   (a < b) -> (a < c + b)
+{-# inline weakenL #-}
 weakenL Lt = Lt
 
 -- | Add a constant to the right-hand side of the right-hand side of
 -- the strict inequality.
 weakenR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
   (a < b) -> (a < b + c)
+{-# inline weakenR #-}
 weakenR Lt = Lt
 
 -- | Compose two strict inequalities using transitivity.
 transitive :: (a < b) -> (b < c) -> (a < c)
+{-# inline transitive #-}
 transitive Lt Lt = Lt
 
 -- | Compose a strict inequality (the first argument) with a nonstrict
 -- inequality (the second argument).
 transitiveNonstrictR :: (a < b) -> (b <= c) -> (a < c)
+{-# inline transitiveNonstrictR #-}
 transitiveNonstrictR Lt Lte = Lt
 
 transitiveNonstrictL :: (a <= b) -> (b < c) -> (a < c)
+{-# inline transitiveNonstrictL #-}
 transitiveNonstrictL Lte Lt = Lt
 
 -- | Zero is less than one.
 zero :: 0 < 1
+{-# inline zero #-}
 zero = Lt
 
 -- | Nothing is less than zero.
 absurd :: n < 0 -> void
-absurd Lt = error "Arithmetic.Nat.absurd: n < 0"
+{-# inline absurd #-}
+absurd Lt = errorWithoutStackTrace "Arithmetic.Nat.absurd: n < 0"
 
 -- | Use GHC's built-in type-level arithmetic to prove
 -- that one number is less than another. The type-checker
 -- only reduces 'CmpNat' if both arguments are constants.
 constant :: forall a b. (CmpNat a b ~ 'LT) => (a < b)
+{-# inline constant #-}
 constant = Lt
 
+-- | Given that @m < n/p@, we know that @p*m < n@.
+reciprocalA :: forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat).
+  (m < GHC.Div n p) -> (p GHC.* m) < n
+{-# inline reciprocalA #-}
+reciprocalA _ = Lt
+
+-- | Given that @m < roundUp(n/p)@, we know that @p*m < n@.
+reciprocalB :: forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat).
+  (m < GHC.Div (n GHC.- 1) p + 1) -> (p GHC.* m) < n
+{-# inline reciprocalB #-}
+reciprocalB _ = Lt
diff --git a/src/Arithmetic/Lte.hs b/src/Arithmetic/Lte.hs
--- a/src/Arithmetic/Lte.hs
+++ b/src/Arithmetic/Lte.hs
@@ -38,73 +38,87 @@
 -- | Replace the left-hand side of a strict inequality
 -- with an equal number.
 substituteL :: (b :=: c) -> (b <= a) -> (c <= a)
+{-# inline substituteL #-}
 substituteL Eq Lte = Lte
 
 -- | Replace the right-hand side of a strict inequality
 -- with an equal number.
 substituteR :: (b :=: c) -> (a <= b) -> (a <= c)
+{-# inline substituteR #-}
 substituteR Eq Lte = Lte
 
 -- | Add two inequalities.
 plus :: (a <= b) -> (c <= d) -> (a + c <= b + d)
+{-# inline plus #-}
 plus Lte Lte = Lte
 
 -- | Compose two inequalities using transitivity.
 transitive :: (a <= b) -> (b <= c) -> (a <= c)
+{-# inline transitive #-}
 transitive Lte Lte = Lte
 
 -- | Any number is less-than-or-equal-to itself.
 reflexive :: a <= a
+{-# inline reflexive #-}
 reflexive = Lte
 
 -- | Add a constant to the left-hand side of both sides of
 -- the inequality.
 incrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
   (a <= b) -> (c + a <= c + b)
+{-# inline incrementL #-}
 incrementL Lte = Lte
 
 -- | Add a constant to the right-hand side of both sides of
 -- the inequality.
 incrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
   (a <= b) -> (a + c <= b + c)
+{-# inline incrementR #-}
 incrementR Lte = Lte
 
 -- | Add a constant to the left-hand side of the right-hand side of
 -- the inequality.
 weakenL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
   (a <= b) -> (a <= c + b)
+{-# inline weakenL #-}
 weakenL Lte = Lte
 
 -- | Add a constant to the right-hand side of the right-hand side of
 -- the inequality.
 weakenR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
   (a <= b) -> (a <= b + c)
+{-# inline weakenR #-}
 weakenR Lte = Lte
 
 -- | Subtract a constant from the left-hand side of both sides of
 -- the inequality. This is the opposite of 'incrementL'.
 decrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
   (c + a <= c + b) -> (a <= b)
+{-# inline decrementL #-}
 decrementL Lte = Lte
 
 -- | Subtract a constant from the right-hand side of both sides of
 -- the inequality. This is the opposite of 'incrementR'.
 decrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
   (a + c <= b + c) -> (a <= b)
+{-# inline decrementR #-}
 decrementR Lte = Lte
 
 -- | Weaken a strict inequality to a non-strict inequality.
 fromStrict :: (a < b) -> (a <= b)
+{-# inline fromStrict #-}
 fromStrict Lt = Lte
 
 -- | Zero is less-than-or-equal-to any number.
 zero :: 0 <= a
+{-# inline zero #-}
 zero = Lte
 
 -- | Use GHC's built-in type-level arithmetic to prove
 -- that one number is less-than-or-equal-to another. The type-checker
 -- only reduces 'CmpNat' if both arguments are constants.
 constant :: forall a b. (IsLte (CmpNat a b) ~ 'True) => (a <= b)
+{-# inline constant #-}
 constant = Lte
 
 type family IsLte (o :: Ordering) :: Bool where
diff --git a/src/Arithmetic/Nat.hs b/src/Arithmetic/Nat.hs
--- a/src/Arithmetic/Nat.hs
+++ b/src/Arithmetic/Nat.hs
@@ -5,12 +5,19 @@
 {-# language RankNTypes #-}
 {-# language ScopedTypeVariables #-}
 {-# language TypeOperators #-}
+{-# language UnboxedTuples #-}
 
 module Arithmetic.Nat
   ( -- * Addition
     plus
+  , plus#
     -- * Subtraction
   , monus
+    -- * Division
+  , divide
+  , divideRoundingUp
+    -- * Multiplication
+  , times
     -- * Successor
   , succ
     -- * Compare
@@ -27,8 +34,12 @@
   , two
   , three
   , constant
+    -- * Unboxed Constants
+  , zero#
     -- * Convert
   , demote
+  , unlift
+  , lift
   , with
   ) where
 
@@ -36,10 +47,13 @@
 
 import Arithmetic.Types
 import Arithmetic.Unsafe ((:=:)(Eq), type (<=)(Lte))
-import Arithmetic.Unsafe (Nat(Nat),type (<)(Lt))
-import GHC.Exts (Proxy#,proxy#)
-import GHC.TypeNats (type (+),KnownNat,natVal')
+import Arithmetic.Unsafe (Nat(Nat),Nat#(Nat#),type (<)(Lt))
+import GHC.Exts (Proxy#,proxy#,(+#))
+import GHC.TypeNats (type (+),type (-),Div,KnownNat,natVal')
+import GHC.Int (Int(I#))
 
+import qualified GHC.TypeNats as GHC
+
 -- | Infix synonym of 'testLessThan'.
 (<?) :: Nat a -> Nat b -> Maybe (a < b)
 {-# inline (<?) #-}
@@ -90,6 +104,29 @@
 {-# inline plus #-}
 plus (Nat x) (Nat y) = Nat (x + y)
 
+-- | Variant of 'plus' for unboxed nats.
+plus# :: Nat# a -> Nat# b -> Nat# (a + b)
+{-# inline plus# #-}
+plus# (Nat# x) (Nat# y) = Nat# (x +# y)
+
+-- | Divide two numbers. Rounds down (towards zero)
+divide :: Nat a -> Nat b -> Nat (Div a b)
+{-# inline divide #-}
+divide (Nat x) (Nat y) = Nat (div x y)
+
+-- | Divide two numbers. Rounds up (away from zero)
+divideRoundingUp :: Nat a -> Nat b -> Nat (Div (a - 1) b + 1)
+{-# inline divideRoundingUp #-}
+divideRoundingUp (Nat x) (Nat y) =
+  -- Implementation note. We must use div so that when x=0,
+  -- the result is (-1) and not 0. Then when we add 1, we get 0.
+  Nat (1 + (div (x - 1) y))
+
+-- | Multiply two numbers.
+times :: Nat a -> Nat b -> Nat (a GHC.* b)
+{-# inline times #-}
+times (Nat x) (Nat y) = Nat (x * y)
+
 -- | The successor of a number.
 succ :: Nat a -> Nat (a + 1)
 {-# inline succ #-}
@@ -129,6 +166,10 @@
 {-# inline constant #-}
 constant = Nat (fromIntegral (natVal' (proxy# :: Proxy# n)))
 
+-- | The number zero. Unboxed.
+zero# :: (# #) -> Nat# 0
+zero# _ = Nat# 0#
+
 -- | Extract the 'Int' from a 'Nat'. This is intended to be used
 -- at a boundary where a safe interface meets the unsafe primitives
 -- on top of which it is built.
@@ -143,3 +184,11 @@
 with :: Int -> (forall n. Nat n -> a) -> a
 {-# inline with #-}
 with i f = f (Nat i)
+
+unlift :: Nat n -> Nat# n
+{-# inline unlift #-}
+unlift (Nat (I# i)) = Nat# i
+
+lift :: Nat# n -> Nat n
+{-# inline lift #-}
+lift (Nat# i) = Nat (I# i)
diff --git a/src/Arithmetic/Types.hs b/src/Arithmetic/Types.hs
--- a/src/Arithmetic/Types.hs
+++ b/src/Arithmetic/Types.hs
@@ -1,4 +1,5 @@
 {-# language DataKinds #-}
+{-# language MagicHash #-}
 {-# language ExplicitNamespaces #-}
 {-# language GADTs #-}
 {-# language KindSignatures #-}
@@ -7,15 +8,17 @@
 
 module Arithmetic.Types
   ( Nat
+  , Nat#
   , WithNat(..)
   , Difference(..)
   , Fin(..)
+  , Fin#
   , type (<)
   , type (<=)
   , type (:=:)
   ) where
 
-import Arithmetic.Unsafe (Nat(getNat), type (<=))
+import Arithmetic.Unsafe (Fin#,Nat#,Nat(getNat), type (<=))
 import Arithmetic.Unsafe (type (<), type (:=:))
 import Data.Kind (type Type)
 import GHC.TypeNats (type (+))
diff --git a/src/Arithmetic/Unsafe.hs b/src/Arithmetic/Unsafe.hs
--- a/src/Arithmetic/Unsafe.hs
+++ b/src/Arithmetic/Unsafe.hs
@@ -12,6 +12,7 @@
 
 module Arithmetic.Unsafe
   ( Nat(..)
+  , Nat#(..)
   , Fin#(..)
   , type (<)(Lt)
   , type (<=)(Lte)
@@ -43,9 +44,15 @@
 
 deriving newtype instance Show (Nat n)
 
+-- | Unboxed variant of Nat.
+newtype Nat# :: GHC.Nat -> TYPE 'IntRep where
+  Nat# :: Int# -> Nat# n
+type role Nat# nominal
+
 -- | Finite numbers without the overhead of carrying around a proof.
 newtype Fin# :: GHC.Nat -> TYPE 'IntRep where
   Fin# :: Int# -> Fin# n
+type role Fin# nominal
 
 -- | Proof that the first argument is strictly less than the
 -- second argument.