diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,19 @@
 # Revision history for natural-arithmetic
 
+## 0.2.3.0 -- 2025-06-12
+
+* Add Fin.greatest#
+* Add Plus.commutative#
+* Add substitution functions for unlifted less-than-or-equal-to
+* Add Nat.substitute#
+* Add Eq.symmetric#
+* Add nativeFrom32#
+* Add incrementL#
+* Add testLessThanEqual#
+* Add nativeTo32#
+* Add Fin.ascendFromToM_#
+* Add Fin.weaken#
+
 ## 0.2.2.0 -- 2025-04-07
 
 * Add Fin.weakenL#
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.2.2.0
+version:         0.2.3.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
@@ -7,11 +7,13 @@
 
 module Arithmetic.Equal
   ( symmetric
+  , symmetric#
   , plusR
   , plusL
   , plusR#
   , plusL#
   , lift
+  , unlift
   ) where
 
 import Arithmetic.Unsafe (type (:=:) (Eq), type (:=:#) (Eq#))
@@ -21,6 +23,10 @@
 {-# INLINE symmetric #-}
 symmetric Eq = Eq
 
+symmetric# :: (m :=:# n) -> (n :=:# m)
+{-# INLINE symmetric# #-}
+symmetric# _ = Eq# (# #)
+
 plusL :: forall c m n. (m :=: n) -> (c + m :=: c + n)
 {-# INLINE plusL #-}
 plusL Eq = Eq
@@ -40,3 +46,7 @@
 lift :: (m :=:# n) -> (m :=: n)
 {-# INLINE lift #-}
 lift _ = Eq
+
+unlift :: (m :=: n) -> (m :=:# n)
+{-# INLINE unlift #-}
+unlift _ = Eq# (# #)
diff --git a/src/Arithmetic/Fin.hs b/src/Arithmetic/Fin.hs
--- a/src/Arithmetic/Fin.hs
+++ b/src/Arithmetic/Fin.hs
@@ -13,9 +13,11 @@
 module Arithmetic.Fin
   ( -- * Modification
     incrementL
+  , incrementL#
   , incrementR
   , incrementR#
   , weaken
+  , weaken#
   , weakenL
   , weakenL#
   , weakenR
@@ -38,6 +40,7 @@
   , ascendM#
   , ascendM_
   , ascendM_#
+  , ascendFromToM_#
   , descend
   , descend#
   , descend'
@@ -62,15 +65,21 @@
 
     -- * Construct
   , construct#
+  , nativeTo32#
+  , nativeFrom32#
   , remInt#
   , remWord#
   , fromInt
   , fromInt#
   , constant#
+  , greatest#
 
     -- * Compare
   , equals#
 
+    -- * Substitute Bound
+  , substitute#
+
     -- * Lift and Unlift
   , lift
   , unlift
@@ -78,9 +87,11 @@
 
 import Prelude hiding (last, succ)
 
-import Arithmetic.Nat ((<?))
-import Arithmetic.Types (Difference (..), Fin (..), Nat, Nat#, pattern MaybeFinJust#, pattern MaybeFinNothing#, type (:=:), type (<), type (<#), type (<=))
+import Arithmetic.Nat ((<?),(<?#))
+import Arithmetic.Types (Difference (..), Fin (..), Nat, Nat#, pattern MaybeFinJust#, pattern MaybeFinNothing#, type (:=:), type (<), type (<#), type (<=), (:=:#))
+import Arithmetic.Types (type (<=#))
 import Arithmetic.Unsafe (Fin# (Fin#), MaybeFin#, Nat# (Nat#), Fin32#(Fin32#))
+import Data.Maybe.Void (pattern JustVoid#)
 import GHC.Exts (Int (I#), Int32#, Int#, Word#, (+#), (==#))
 import GHC.TypeNats (CmpNat, type (+))
 
@@ -111,6 +122,10 @@
 {-# INLINE incrementL #-}
 incrementL m (Fin i pf) = Fin (Nat.plus m i) (Lt.incrementL @m pf)
 
+incrementL# :: forall n m. Nat# m -> Fin# n -> Fin# (m + n)
+{-# INLINE incrementL# #-}
+incrementL# (Nat# n) (Fin# i) = Fin# (n +# i)
+
 {- | Weaken the bound by @m@, adding it to the left-hand side of
 the existing bound. This does not change the index.
 -}
@@ -150,6 +165,10 @@
 {-# INLINE weaken #-}
 weaken lt (Fin i pf) = Fin i (Lt.transitiveNonstrictR pf lt)
 
+weaken# :: forall n m. (n <=# m) -> Fin# n -> Fin# m
+{-# INLINE weaken# #-}
+weaken# _ (Fin# x) = Fin# x
+
 -- | A finite set of no values is impossible.
 absurd :: Fin 0 -> void
 {-# INLINE absurd #-}
@@ -362,6 +381,23 @@
     Nothing -> pure ()
     Just lt -> f (Fin m lt) *> go (Nat.succ m)
 
+ascendFromToM_# ::
+  forall m a i n.
+  (Monad m) =>
+  -- | Index to start at (inclusive)
+  Nat# i ->
+  -- | Upper bound (exclusive)
+  Nat# n ->
+  -- | Update accumulator
+  (Fin# n -> m a) ->
+  m ()
+ascendFromToM_# m0 end f = go m0
+  where
+  go :: forall k. Nat# k -> m ()
+  go m = case m <?# end of
+    JustVoid# lt -> f (construct# lt m) *> go (Nat.succ# m)
+    _ -> pure ()
+
 {- | Variant of @ascendM_@ that takes an unboxed Nat and provides
 an unboxed Fin to the callback.
 -}
@@ -624,6 +660,14 @@
   0# -> errorWithoutStackTrace "Arithmetic.Fin.remWord#: cannot divide by zero"
   _ -> Fin# (Exts.word2Int# (Exts.remWord# w (Exts.int2Word# n)))
 
+nativeTo32# :: (n <=# 2147483648) -> Fin# n -> Fin32# n
+{-# inline nativeTo32# #-}
+nativeTo32# _ (Fin# x) = Fin32# (Exts.intToInt32# x)
+
+nativeFrom32# :: Fin32# n -> Fin# n
+{-# inline nativeFrom32# #-}
+nativeFrom32# (Fin32# x) = Fin# (Exts.int32ToInt# x)
+
 {- | Create an unlifted finite number from an unlifted natural number.
 The upper bound is the first type argument so that user can use
 type applications to clarify when it is helpful. For example:
@@ -635,3 +679,9 @@
 
 equals# :: Fin# n -> Fin# n -> Bool
 equals# (Fin# a) (Fin# b) = Exts.isTrue# (a ==# b)
+
+substitute# :: (m :=:# n) -> Fin# m -> Fin# n
+substitute# _ (Fin# x) = Fin# x
+
+greatest# :: Nat# n -> Fin# (n + 1)
+greatest# (Nat# i) = Fin# i
diff --git a/src/Arithmetic/Lte.hs b/src/Arithmetic/Lte.hs
--- a/src/Arithmetic/Lte.hs
+++ b/src/Arithmetic/Lte.hs
@@ -13,7 +13,9 @@
 
     -- * Substitution
   , substituteL
+  , substituteL#
   , substituteR
+  , substituteR#
 
     -- * Increment
   , incrementL
@@ -54,6 +56,7 @@
   ) where
 
 import Arithmetic.Unsafe (type (:=:) (Eq), type (<) (Lt), type (<#), type (<=) (Lte), type (<=#) (Lte#))
+import Arithmetic.Unsafe (type (:=:#))
 import GHC.TypeNats (CmpNat, type (+))
 
 import qualified GHC.TypeNats as GHC
@@ -71,6 +74,14 @@
 substituteR :: (b :=: c) -> (a <= b) -> (a <= c)
 {-# INLINE substituteR #-}
 substituteR Eq Lte = Lte
+
+substituteL# :: (b :=:# c) -> (b <=# a) -> (c <=# a)
+{-# INLINE substituteL# #-}
+substituteL# _ _ = Lte# (# #)
+
+substituteR# :: (b :=:# c) -> (a <=# b) -> (a <=# c)
+{-# INLINE substituteR# #-}
+substituteR# _ _ = Lte# (# #)
 
 -- | Add two inequalities.
 plus :: (a <= b) -> (c <= d) -> (a + c <= b + d)
diff --git a/src/Arithmetic/Nat.hs b/src/Arithmetic/Nat.hs
--- a/src/Arithmetic/Nat.hs
+++ b/src/Arithmetic/Nat.hs
@@ -32,12 +32,14 @@
   , testLessThan
   , testLessThan#
   , testLessThanEqual
+  , testLessThanEqual#
   , testZero
   , testZero#
   , (=?)
   , (<?)
   , (<?#)
   , (<=?)
+  , (<=?#)
 
     -- * Constants
   , zero
@@ -80,12 +82,16 @@
   , lift
   , with
   , with#
+
+    -- * Substitute
+  , substitute#
   ) where
 
 import Prelude hiding (succ)
 
 import Arithmetic.Types
 import Arithmetic.Unsafe (Nat (Nat), Nat# (Nat#), (:=:) (Eq), (:=:#) (Eq#), type (<) (Lt), type (<#) (Lt#), type (<=) (Lte))
+import Arithmetic.Unsafe (type (<=#) (Lte#))
 import Data.Either.Void (EitherVoid#, pattern LeftVoid#, pattern RightVoid#)
 import Data.Maybe.Void (MaybeVoid#, pattern JustVoid#, pattern NothingVoid#)
 import GHC.Exts (Int#, Proxy#, proxy#, (+#), (<#), (==#))
@@ -113,6 +119,10 @@
 {-# INLINE (<?#) #-}
 (<?#) = testLessThan#
 
+(<=?#) :: Nat# a -> Nat# b -> MaybeVoid# (a <=# b)
+{-# INLINE (<=?#) #-}
+(<=?#) = testLessThanEqual#
+
 {- | Is the first argument strictly less than the second
 argument?
 -}
@@ -139,6 +149,12 @@
     then Just Lte
     else Nothing
 
+testLessThanEqual# :: Nat# a -> Nat# b -> MaybeVoid# (a <=# b)
+{-# INLINE testLessThanEqual# #-}
+testLessThanEqual# (Nat# x) (Nat# y) = case x <# y of
+  0# -> NothingVoid#
+  _ -> JustVoid# (Lte# (# #))
+
 -- | Are the two arguments equal to one another?
 testEqual :: Nat a -> Nat b -> Maybe (a :=: b)
 {-# INLINE testEqual #-}
@@ -345,3 +361,6 @@
 
 pattern N16384# :: Nat# 16384
 pattern N16384# = Nat# 16384#
+
+substitute# :: (m :=:# n) -> Nat# m -> Nat# n
+substitute# _ (Nat# x) = Nat# x
diff --git a/src/Arithmetic/Plus.hs b/src/Arithmetic/Plus.hs
--- a/src/Arithmetic/Plus.hs
+++ b/src/Arithmetic/Plus.hs
@@ -2,16 +2,20 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ExplicitForAll #-}
 {-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UnboxedTuples #-}
 
 module Arithmetic.Plus
   ( zeroL
   , zeroR
   , commutative
+  , commutative#
   , associative
   ) where
 
 import Arithmetic.Unsafe (type (:=:) (Eq))
+import Arithmetic.Unsafe (type (:=:#) (Eq#))
 import GHC.TypeNats (type (+))
 
 -- | Any number plus zero is equal to the original number.
@@ -25,6 +29,9 @@
 -- | Addition is commutative.
 commutative :: forall a b. a + b :=: b + a
 commutative = Eq
+
+commutative# :: forall a b. (# #) -> a + b :=:# b + a
+commutative# _ = Eq# (# #)
 
 -- | Addition is associative.
 associative :: forall a b c. (a + b) + c :=: a + (b + c)