diff --git a/Crypto/ECC.hs b/Crypto/ECC.hs
index 34a911f..8391b5a 100644
--- a/Crypto/ECC.hs
+++ b/Crypto/ECC.hs
@@ -31,7 +31,6 @@ import qualified Crypto.ECC.Simple.Types as Simple
 import qualified Crypto.ECC.Simple.Prim as Simple
 import           Crypto.Random
 import           Crypto.Error
-import           Crypto.Internal.Proxy
 import           Crypto.Internal.Imports
 import           Crypto.Internal.ByteArray (ByteArray, ByteArrayAccess, ScrubbedBytes)
 import qualified Crypto.Internal.ByteArray as B
@@ -41,6 +40,7 @@ import qualified Crypto.PubKey.Curve448 as X448
 import           Data.ByteArray (convert)
 import           Data.Data (Data())
 import           Data.Kind (Type)
+import           Data.Proxy
 
 -- | An elliptic curve key pair composed of the private part (a scalar), and
 -- the associated point.
diff --git a/Crypto/ECC/Simple/Prim.hs b/Crypto/ECC/Simple/Prim.hs
index 25d8fe1..48e94cb 100644
--- a/Crypto/ECC/Simple/Prim.hs
+++ b/Crypto/ECC/Simple/Prim.hs
@@ -17,7 +17,7 @@ module Crypto.ECC.Simple.Prim
     ) where
 
 import Data.Maybe
-import Crypto.Internal.Proxy
+import Data.Proxy
 import Crypto.Number.ModArithmetic
 import Crypto.Number.F2m
 import Crypto.Number.Generate (generateBetween)
diff --git a/Crypto/Internal/Nat.hs b/Crypto/Internal/Nat.hs
index dfa3a4d..03b75c0 100644
--- a/Crypto/Internal/Nat.hs
+++ b/Crypto/Internal/Nat.hs
@@ -9,6 +9,7 @@ module Crypto.Internal.Nat
     , type IsAtMost, type IsAtLeast
     , byteLen
     , integralNatVal
+    , type IsDiv8
     , type Div8
     , type Mod8
     ) where
@@ -207,4 +208,6 @@ type family Mod8 (n :: Nat) where
     Mod8 63 = 7
     Mod8 n = Mod8 (n - 64)
 
+-- | ensure the given `bitlen` is divisible by 8
+--
 type IsDivisibleBy8 bitLen = IsDiv8 bitLen bitLen ~ 'True
diff --git a/Crypto/Internal/Proxy.hs b/Crypto/Internal/Proxy.hs
deleted file mode 100644
index 1873b2b..0000000
--- a/Crypto/Internal/Proxy.hs
+++ /dev/null
@@ -1,13 +0,0 @@
--- |
--- Module      : Crypto.Internal.Proxy
--- License     : BSD-style
--- Maintainer  : Vincent Hanquez <vincent@snarc.org>
--- Stability   : experimental
--- Portability : Good
---
-module Crypto.Internal.Proxy
-    ( Proxy(..)
-    ) where
-
--- | A type witness for 'a' as phantom type
-data Proxy a = Proxy
diff --git a/Crypto/Number/Nat.hs b/Crypto/Number/Nat.hs
new file mode 100644
index 0000000..8620bf4
--- /dev/null
+++ b/Crypto/Number/Nat.hs
@@ -0,0 +1,63 @@
+-- |
+-- Module      : Crypto.Number.Nat
+-- License     : BSD-style
+-- Maintainer  : Vincent Hanquez <vincent@snarc.org>
+-- Stability   : experimental
+-- Portability : Good
+--
+-- Numbers at type level.
+--
+-- This module provides extensions to "GHC.TypeLits" and "GHC.TypeNats" useful
+-- to work with cryptographic algorithms parameterized with a variable bit
+-- length.  Constraints like @'IsDivisibleBy8' n@ ensure that the type-level
+-- parameter is applicable to the algorithm.
+--
+-- Functions are also provided to test whether constraints are satisfied from
+-- values known at runtime.  The following example shows how to discharge
+-- 'IsDivisibleBy8' in a computation @fn@ requiring this constraint:
+--
+-- > withDivisibleBy8 :: Integer
+-- >                  -> (forall proxy n . (KnownNat n, IsDivisibleBy8 n) => proxy n -> a)
+-- >                  -> Maybe a
+-- > withDivisibleBy8 len fn = do
+-- >     SomeNat p <- someNatVal len
+-- >     Refl <- isDivisibleBy8 p
+-- >     pure (fn p)
+--
+-- Function @withDivisibleBy8@ above returns 'Nothing' when the argument @len@
+-- is negative or not divisible by 8.
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+module Crypto.Number.Nat
+    ( type IsDivisibleBy8
+    , type IsAtMost, type IsAtLeast
+    , isDivisibleBy8
+    , isAtMost
+    , isAtLeast
+    ) where
+
+import           Data.Type.Equality
+import           GHC.TypeLits
+import           Unsafe.Coerce (unsafeCoerce)
+
+import           Crypto.Internal.Nat
+
+-- | get a runtime proof that the constraint @'IsDivisibleBy8' n@ is satified
+isDivisibleBy8 :: KnownNat n => proxy n -> Maybe (IsDiv8 n n :~: 'True)
+isDivisibleBy8 n
+    | mod (natVal n) 8 == 0 = Just (unsafeCoerce Refl)
+    | otherwise             = Nothing
+
+-- | get a runtime proof that the constraint @'IsAtMost' value bound@ is
+-- satified
+isAtMost :: (KnownNat value, KnownNat bound)
+         => proxy value -> proxy' bound -> Maybe ((value <=? bound) :~: 'True)
+isAtMost x y
+    | natVal x <= natVal y  = Just (unsafeCoerce Refl)
+    | otherwise             = Nothing
+
+-- | get a runtime proof that the constraint @'IsAtLeast' value bound@ is
+-- satified
+isAtLeast :: (KnownNat value, KnownNat bound)
+          => proxy value -> proxy' bound -> Maybe ((bound <=? value) :~: 'True)
+isAtLeast = flip isAtMost
diff --git a/Crypto/Random/Entropy/Backend.hs b/Crypto/Random/Entropy/Backend.hs
index eb2a92e..ca2acc2 100644
--- a/Crypto/Random/Entropy/Backend.hs
+++ b/Crypto/Random/Entropy/Backend.hs
@@ -14,8 +14,8 @@ module Crypto.Random.Entropy.Backend
     ) where
 
 import Foreign.Ptr
+import Data.Proxy
 import Data.Word (Word8)
-import Crypto.Internal.Proxy
 import Crypto.Random.Entropy.Source
 #ifdef SUPPORT_RDRAND
 import Crypto.Random.Entropy.RDRand
diff --git a/cryptonite.cabal b/cryptonite.cabal
index 2c09c5c..7bb1c5c 100644
--- a/cryptonite.cabal
+++ b/cryptonite.cabal
@@ -130,6 +130,7 @@ Library
                      Crypto.Number.F2m
                      Crypto.Number.Generate
                      Crypto.Number.ModArithmetic
+                     Crypto.Number.Nat
                      Crypto.Number.Prime
                      Crypto.Number.Serialize
                      Crypto.Number.Serialize.Internal
@@ -220,7 +221,6 @@ Library
                      Crypto.PubKey.ElGamal
                      Crypto.ECC.Simple.Types
                      Crypto.ECC.Simple.Prim
-                     Crypto.Internal.Proxy
                      Crypto.Internal.ByteArray
                      Crypto.Internal.Compat
                      Crypto.Internal.CompatPrim