diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,11 @@
 # Revision history for natural-arithmetic
 
+## 0.2.4.0 -- 2026-07-14
+
+* Add more stuff for Fin32#
+* Add withPred#
+* Correct implementation of testLessThanEqual#
+
 ## 0.2.3.0 -- 2025-06-12
 
 * Add Fin.greatest#
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.3.0
+version:         0.2.4.0
 synopsis:        Arithmetic of natural numbers
 description:
   A search for terms like `arithmetic` and `natural` on hackage reveals
@@ -91,4 +91,4 @@
 
 source-repository head
   type:     git
-  location: git://github.com/byteverse/natural-arithmetic.git
+  location: ssh://github.com/byteverse/natural-arithmetic.git
diff --git a/src/Arithmetic/Fin.hs b/src/Arithmetic/Fin.hs
--- a/src/Arithmetic/Fin.hs
+++ b/src/Arithmetic/Fin.hs
@@ -22,8 +22,11 @@
   , weakenL#
   , weakenR
   , weakenR#
+  , weaken32R#
   , succ
   , succ#
+  , succ32#
+  , pred32#
 
     -- * Traverse
 
@@ -65,6 +68,7 @@
 
     -- * Construct
   , construct#
+  , construct32#
   , nativeTo32#
   , nativeFrom32#
   , remInt#
@@ -73,6 +77,7 @@
   , fromInt#
   , constant#
   , greatest#
+  , greatest32#
 
     -- * Compare
   , equals#
@@ -88,9 +93,9 @@
 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.Types (Difference (..), Fin (..), Nat, Nat#, pattern MaybeFinJust#, pattern MaybeFinNothing#, pattern MaybeFin32Nothing#, pattern MaybeFin32Just#, type (:=:), type (<), type (<#), type (<=), (:=:#))
 import Arithmetic.Types (type (<=#))
-import Arithmetic.Unsafe (Fin# (Fin#), MaybeFin#, Nat# (Nat#), Fin32#(Fin32#))
+import Arithmetic.Unsafe (Fin# (Fin#), MaybeFin#, Nat# (Nat#), Fin32#(Fin32#), MaybeFin32#(MaybeFin32#))
 import Data.Maybe.Void (pattern JustVoid#)
 import GHC.Exts (Int (I#), Int32#, Int#, Word#, (+#), (==#))
 import GHC.TypeNats (CmpNat, type (+))
@@ -158,6 +163,12 @@
 {-# INLINE weakenR# #-}
 weakenR# (Fin# i) = Fin# i
 
+{- | Unboxed variant of 'weakenR'.
+-}
+weaken32R# :: forall n m. Fin32# n -> Fin32# (n + m)
+{-# INLINE weaken32R# #-}
+weaken32R# (Fin32# i) = Fin32# i
+
 {- | Weaken the bound, replacing it by another number greater than
 or equal to itself. This does not change the index.
 -}
@@ -595,6 +606,10 @@
 {-# INLINE construct# #-}
 construct# _ (Unsafe.Nat# x) = Unsafe.Fin# x
 
+construct32# :: (n <=# 2147483648) -> (i <# n) -> Nat# i -> Fin32# n
+{-# INLINE construct32# #-}
+construct32# _ _ (Unsafe.Nat# x) = Unsafe.Fin32# (Exts.intToInt32# x)
+
 {- | Return the successor of the Fin or return nothing if the
 argument is the greatest inhabitant.
 -}
@@ -615,6 +630,25 @@
  where
   !ix' = ix +# 1#
 
+-- | Variant of 'succ' for unlifted 32-bit finite numbers.
+--
+-- The implementation of this is kind of weird because we have to
+-- worry about overflow.
+succ32# :: (n <=# 2147483648) -> Nat# n -> Fin32# n -> MaybeFin32# n
+{-# INLINE succ32# #-}
+succ32# _ (Nat# n) (Fin32# ix) =
+  case ix' Exts.<# n of
+    0# -> MaybeFin32Nothing#
+    _ -> MaybeFin32Just# (Fin32# (Exts.intToInt32# ix'))
+ where
+  !ix' = Exts.int32ToInt# ix +# 1#
+
+pred32# :: Fin32# n -> MaybeFin32# n
+{-# inline pred32# #-}
+pred32# (Fin32# x) = case Exts.int32ToInt# x of
+  0# -> MaybeFin32Nothing#
+  _ -> MaybeFin32# (Exts.subInt32# x (Exts.intToInt32# 1# ))
+
 {- | Convert an Int to a finite number, testing that it is
 less than the upper bound. This crashes with an uncatchable
 exception when given a negative number.
@@ -685,3 +719,6 @@
 
 greatest# :: Nat# n -> Fin# (n + 1)
 greatest# (Nat# i) = Fin# i
+
+greatest32# :: (n <# 2147483648) -> Nat# n -> Fin32# (n + 1)
+greatest32# _ (Nat# i) = Fin32# (Exts.intToInt32# i)
diff --git a/src/Arithmetic/Nat.hs b/src/Arithmetic/Nat.hs
--- a/src/Arithmetic/Nat.hs
+++ b/src/Arithmetic/Nat.hs
@@ -25,6 +25,8 @@
     -- * Successor
   , succ
   , succ#
+    -- * Predecessor
+  , withPred#
 
     -- * Compare
   , testEqual
@@ -74,6 +76,8 @@
   , pattern N4096#
   , pattern N8192#
   , pattern N16384#
+  , pattern N32768#
+  , pattern N65536#
 
     -- * Convert
   , demote
@@ -94,7 +98,7 @@
 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#, (+#), (<#), (==#))
+import GHC.Exts (Int#, Proxy#, proxy#, (+#), (<#), (==#), (-#), (<=#))
 import GHC.Int (Int (I#))
 import GHC.TypeNats (Div, KnownNat, natVal', type (+), type (-))
 
@@ -151,7 +155,7 @@
 
 testLessThanEqual# :: Nat# a -> Nat# b -> MaybeVoid# (a <=# b)
 {-# INLINE testLessThanEqual# #-}
-testLessThanEqual# (Nat# x) (Nat# y) = case x <# y of
+testLessThanEqual# (Nat# x) (Nat# y) = case x <=# y of
   0# -> NothingVoid#
   _ -> JustVoid# (Lte# (# #))
 
@@ -219,6 +223,15 @@
 {-# INLINE succ# #-}
 succ# n = plus# n (one# (# #))
 
+-- | If a natural number is greater than zero, we can operate on its
+-- predecessor.
+withPred# ::
+     Nat# a
+  -> (0 <# a)
+  -> (forall b. Nat# b -> (a :=:# b + 1) -> t)
+  -> t
+withPred# (Nat# i) _ f = f (Nat# (i -# 1#)) (Eq# (# #))
+
 -- | Subtract the second argument from the first argument.
 monus :: Nat a -> Nat b -> Maybe (Difference a b)
 {-# INLINE monus #-}
@@ -361,6 +374,12 @@
 
 pattern N16384# :: Nat# 16384
 pattern N16384# = Nat# 16384#
+
+pattern N32768# :: Nat# 32768
+pattern N32768# = Nat# 32768#
+
+pattern N65536# :: Nat# 65536
+pattern N65536# = Nat# 65536#
 
 substitute# :: (m :=:# n) -> Nat# m -> Nat# n
 substitute# _ (Nat# x) = Nat# x
diff --git a/src/Arithmetic/Types.hs b/src/Arithmetic/Types.hs
--- a/src/Arithmetic/Types.hs
+++ b/src/Arithmetic/Types.hs
@@ -21,6 +21,9 @@
   , MaybeFin#
   , pattern MaybeFinJust#
   , pattern MaybeFinNothing#
+  , MaybeFin32#
+  , pattern MaybeFin32Just#
+  , pattern MaybeFin32Nothing#
 
     -- * Either Fin
   , EitherFin#
@@ -36,12 +39,13 @@
   , type (:=:#)
   ) where
 
-import Arithmetic.Unsafe (EitherFin# (..), Fin# (Fin#), Fin32#, MaybeFin# (..), Nat (getNat), Nat#, (:=:#), type (:=:), type (<), type (<#), type (<=), type (<=#))
+import Arithmetic.Unsafe (EitherFin# (..), Fin# (Fin#), Fin32# (Fin32#), MaybeFin# (..), MaybeFin32# (..), Nat (getNat), Nat#, (:=:#), type (:=:), type (<), type (<#), type (<=), type (<=#))
 import Data.Kind (type Type)
 import GHC.Exts ((-#), (<#))
 import GHC.TypeNats (type (+))
 
 import qualified GHC.TypeNats as GHC
+import qualified GHC.Exts as Exts
 
 data WithNat :: (GHC.Nat -> Type) -> Type where
   WithNat ::
@@ -99,8 +103,30 @@
 pattern MaybeFinNothing# :: MaybeFin# n
 pattern MaybeFinNothing# = MaybeFin# (-1#)
 
+pattern MaybeFin32Just# :: Fin32# n -> MaybeFin32# n
+pattern MaybeFin32Just# f <- (maybeFin32ToFin32# -> (# | f #))
+  where
+    MaybeFin32Just# (Fin32# i) = MaybeFin32# i
+
+pattern MaybeFin32Nothing# :: MaybeFin32# n
+pattern MaybeFin32Nothing# <- (isNegativeOne32 -> True)
+  where
+    MaybeFin32Nothing# = MaybeFin32# (Exts.intToInt32# (-1#))
+
+isNegativeOne32 :: MaybeFin32# n -> Bool
+{-# INLINE isNegativeOne32 #-}
+isNegativeOne32 (MaybeFin32# x) = case Exts.int32ToInt# x of
+  (-1#) -> True
+  _ -> False
+
 maybeFinToFin# :: MaybeFin# n -> (# (# #) | Fin# n #)
 {-# INLINE maybeFinToFin# #-}
 maybeFinToFin# (MaybeFin# i) = case i of
   -1# -> (# (# #) | #)
   _ -> (# | Fin# i #)
+
+maybeFin32ToFin32# :: MaybeFin32# n -> (# (# #) | Fin32# n #)
+{-# INLINE maybeFin32ToFin32# #-}
+maybeFin32ToFin32# (MaybeFin32# i) = case Exts.int32ToInt# i of
+  -1# -> (# (# #) | #)
+  _ -> (# | Fin32# i #)
diff --git a/src/Arithmetic/Unsafe.hs b/src/Arithmetic/Unsafe.hs
--- a/src/Arithmetic/Unsafe.hs
+++ b/src/Arithmetic/Unsafe.hs
@@ -15,6 +15,7 @@
   , Nat# (..)
   , Fin# (..)
   , MaybeFin# (..)
+  , MaybeFin32# (..)
   , EitherFin# (..)
   , Fin32# (..)
   , type (<#) (Lt#)
@@ -71,6 +72,9 @@
 -}
 newtype MaybeFin# :: GHC.Nat -> TYPE 'IntRep where
   MaybeFin# :: Int# -> MaybeFin# n
+
+newtype MaybeFin32# :: GHC.Nat -> TYPE 'Int32Rep where
+  MaybeFin32# :: Int32# -> MaybeFin32# n
 
 type role MaybeFin# nominal