diff --git a/modular-arithmetic.cabal b/modular-arithmetic.cabal
--- a/modular-arithmetic.cabal
+++ b/modular-arithmetic.cabal
@@ -2,16 +2,12 @@
 -- see http://haskell.org/cabal/users-guide/
 
 name:                modular-arithmetic
-version:             1.2.0.0
+version:             1.2.1.0
 synopsis:            A type for integers modulo some constant.
 
-description:         This module provides a convenient type for working with
-                     integers modulo some constant. It saves you from manually
-                     wrapping numeric operations all over the place and
-                     prevents a range of simple mistakes.
+description:         A convenient type for working with integers modulo some constant. It saves you from manually wrapping numeric operations all over the place and prevents a range of simple mistakes. @Integer `Mod` 7@ is the type of integers (mod 7) backed by @Integer@.
 
-                     It also provides some really cute syntax for these types
-                     like @ℤ/7@ for integers modulo 7.
+                     We also have some cute syntax for these types like @ℤ/7@ for integers modulo 7.
 
 license:             BSD3
 license-file:        LICENSE
diff --git a/src/Data/Modular.hs b/src/Data/Modular.hs
--- a/src/Data/Modular.hs
+++ b/src/Data/Modular.hs
@@ -2,20 +2,16 @@
 {-# LANGUAGE KindSignatures      #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE TypeFamilies #-}
 
 -- |
--- This module provides types for working with integers modulo some
--- constant.
--- 
--- This module uses some new Haskell features introduced in 7.6. In
--- particular, it needs @DataKinds@ and type literals
--- ("GHC.TypeLits"). The @TypeOperators@ extension is needed for the
--- nice infix syntax.
+-- Types for working with integers modulo some constant.
 -- 
--- These types are created with the type constructor 'Mod'
--- (or its synonym '/'). To work with integers mod 7, you could write:
+-- @'Mod'@ and its synonym @/@ let you wrap arbitrary numeric types
+-- in a modulus. To work with integers (mod 7) backed by @Integer@,
+-- you could write:
 -- 
--- > Int `Mod` 7
 -- > Integer `Mod` 7
 -- > Integer/7
 -- > ℤ/7
@@ -23,9 +19,8 @@
 -- (The last is a synonym for @Integer@ provided by this library. In
 -- Emacs, you can use the TeX input mode to type it with @\\Bbb{Z}@.)
 -- 
--- All the usual typeclasses are defined for these types. You can also
--- get the constant using @bound@ or extract the underlying value
--- using @unMod@.
+-- The usual numeric typeclasses are defined for these types. You can
+-- always extrac the underlying value with @'unMod'@.
 --
 -- Here is a quick example:
 -- 
@@ -36,8 +31,12 @@
 -- 
 -- > *Data.Modular> (-10 :: ℤ/7) * (11 :: ℤ/7)
 -- > 2
+--
+-- To us type level numeric literals you need to enable the
+-- @DataKinds@ extension and to use infix syntax for @Mod@ or the @/@
+-- synonym, you need @TypeOperators@.
 
-module Data.Modular (unMod, toMod, toMod', Mod, (/)(), ℤ) where
+module Data.Modular (unMod, toMod, toMod', Mod, inv, (/)(), ℤ, modVal, SomeMod, someModVal) where
 
 import           Control.Arrow (first)
 
@@ -107,6 +106,46 @@
 instance (Integral i, KnownNat n) => Real (i `Mod` n) where
   toRational (Mod i) = toInteger i % 1
 
+-- | Integer division uses modular inverse @'inv'@,
+-- so it is possible to divide only by numbers coprime to @n@
+-- and the remainder is always @0@.
 instance (Integral i, KnownNat n) => Integral (i `Mod` n) where
   toInteger (Mod i) = toInteger i
-  Mod i₁ `quotRem` Mod i₂ = let (q, r) = i₁ `quotRem` i₂ in (toMod q, toMod r)
+  i₁ `quotRem` i₂ = (i₁ * inv i₂, 0)
+
+-- | The modular inverse.
+-- Note that only numbers coprime to @n@ have an inverse modulo @n@.
+inv :: forall n i. (KnownNat n, Integral i) => Mod i n -> Mod i n
+inv k = toMod . snd . inv' (fromInteger (natVal (Proxy :: Proxy n))) . unMod $ k
+  where
+    -- these are only used for error message
+    modulus = show $ natVal (Proxy :: Proxy n)
+    divisor = show (toInteger k)
+
+    -- backwards Euclidean algorithm
+    inv' _ 0 = error ("divide by " ++ divisor ++ " (mod " ++ modulus ++ "), non-coprime to modulus")
+    inv' _ 1 = (0, 1)
+    inv' n x = (r', q' - r' * q)
+      where
+        (q,  r)  = n `quotRem` x
+        (q', r') = inv' x r
+
+-- | This type represents a modular number with unknown bound.
+data SomeMod i where
+  SomeMod :: forall i (n :: Nat). KnownNat n => Mod i n -> SomeMod i
+
+instance Show i => Show (SomeMod i) where
+  showsPrec p (SomeMod x) = showsPrec p x
+
+-- | Convert an integral number @i@ into a @'Mod'@ value given
+-- modular bound @n@ at type level.
+modVal :: forall i proxy n. (Integral i, KnownNat n) => i -> proxy n -> Mod i n
+modVal i _ = toMod i
+
+-- | Convert an integral number @i@ into an unknown @'Mod'@ value.
+someModVal :: Integral i => i -> Integer -> Maybe (SomeMod i)
+someModVal i n =
+  case someNatVal n of
+    Nothing -> Nothing
+    Just (SomeNat proxy) -> Just (SomeMod (modVal i proxy))
+