diff --git a/finite-typelits.cabal b/finite-typelits.cabal
--- a/finite-typelits.cabal
+++ b/finite-typelits.cabal
@@ -1,5 +1,5 @@
 name:                finite-typelits
-version:             0.1.3.0
+version:             0.1.4.0
 synopsis:            A type inhabited by finitely many values, indexed by type-level naturals.
 description:         A type inhabited by finitely many values, indexed by type-level naturals.
 homepage:            https://github.com/mniip/finite-typelits
diff --git a/src/Data/Finite.hs b/src/Data/Finite.hs
--- a/src/Data/Finite.hs
+++ b/src/Data/Finite.hs
@@ -14,6 +14,7 @@
         packFinite, packFiniteProxy,
         finite, finiteProxy,
         getFinite, finites, finitesProxy,
+        modulo, moduloProxy,
         equals, cmp,
         natToFinite,
         weaken, strengthen, shift, unshift,
@@ -57,6 +58,18 @@
 finitesProxy :: KnownNat n => proxy n -> [Finite n]
 finitesProxy _ = finites
 
+-- | Produce the 'Finite' that is congruent to the given integer modulo @n@.
+modulo :: KnownNat n => Integer -> Finite n
+modulo x = result
+    where
+        result = if natVal result == 0
+            then error "modulo: division by zero"
+            else Finite (x `mod` natVal result)
+
+-- | Same as 'modulo' but with a proxy argument to avoid type signatures.
+moduloProxy :: KnownNat n => proxy n -> Integer -> Finite n
+moduloProxy _ = modulo
+
 -- | Test two different types of finite numbers for equality.
 equals :: Finite n -> Finite m -> Bool
 equals (Finite x) (Finite y) = x == y
@@ -147,7 +160,7 @@
     else Left $ Finite $ y - x
 
 -- | Multiply two 'Finite's.
-multiply :: Finite n -> Finite m -> Finite (n * m)
+multiply :: Finite n -> Finite m -> Finite (n GHC.TypeLits.* m)
 multiply (Finite x) (Finite y) = Finite $ x * y
 
 getLeftType :: Either a b -> a
@@ -159,7 +172,7 @@
 combineSum efx@(Right (Finite x)) = Finite $ x + natVal (getLeftType efx)
 
 -- | 'fst'-biased (fst is the inner, and snd is the outer iteratee) product of finite sets.
-combineProduct :: KnownNat n => (Finite n, Finite m) -> Finite (n * m)
+combineProduct :: KnownNat n => (Finite n, Finite m) -> Finite (n GHC.TypeLits.* m)
 combineProduct (fx@(Finite x), Finite y) = Finite $ x + y * natVal fx
 
 -- | Take a 'Left'-biased disjoint union apart.
@@ -171,7 +184,7 @@
             else Left $ Finite x
 
 -- | Take a 'fst'-biased product apart.
-separateProduct :: KnownNat n => Finite (n * m) -> (Finite n, Finite m)
+separateProduct :: KnownNat n => Finite (n GHC.TypeLits.* m) -> (Finite n, Finite m)
 separateProduct (Finite x) = result
     where
         result = (Finite $ x `mod` natVal (fst result), Finite $ x `div` natVal (fst result))
diff --git a/src/Data/Finite/Internal.hs b/src/Data/Finite/Internal.hs
--- a/src/Data/Finite/Internal.hs
+++ b/src/Data/Finite/Internal.hs
@@ -74,7 +74,7 @@
                  guard (x >= 0 && x < natVal result) 
                  return result
 
--- | Modulo arithmetic. Only the 'fromInteger' function is supposed to be useful.
+-- | Modular arithmetic. Only the 'fromInteger' function is supposed to be useful.
 instance KnownNat n => Num (Finite n) where
     fx@(Finite x) + Finite y = Finite $ (x + y) `mod` natVal fx
     fx@(Finite x) - Finite y = Finite $ (x - y) `mod` natVal fx
@@ -90,6 +90,7 @@
 instance KnownNat n => Real (Finite n) where
     toRational (Finite x) = x % 1
 
+-- | __Not__ modular arithmetic.
 instance KnownNat n => Integral (Finite n) where
     quotRem (Finite x) (Finite y) = (Finite $ x `quot` y, Finite $ x `rem` y)
     toInteger (Finite x) = x