diff --git a/finite-typelits.cabal b/finite-typelits.cabal
--- a/finite-typelits.cabal
+++ b/finite-typelits.cabal
@@ -1,6 +1,6 @@
 name:                finite-typelits
-version:             0.1.4.2
-synopsis:            A type inhabited by finitely many values, indexed by type-level naturals.
+version:             0.1.5.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
 license:             BSD3
@@ -12,8 +12,19 @@
 cabal-version:       >=1.10
 
 library
-  exposed-modules:     Data.Finite, Data.Finite.Internal
-  build-depends:       base == 4.*
+  exposed-modules:     Data.Finite
+                     , Data.Finite.Internal
+  build-depends:       base >= 4.7 && <= 4.17
                      , deepseq >= 1.4
   hs-source-dirs:      src
+  default-language:    Haskell2010
+  ghc-options:         -Wall
+
+test-Suite finite-typelits-tests
+  type:                exitcode-stdio-1.0
+  main-is:             test/Main.hs
+  build-depends:       finite-typelits
+                     , base >= 4.9 && <= 4.17
+                     , deepseq >= 1.4
+                     , QuickCheck
   default-language:    Haskell2010
diff --git a/src/Data/Finite.hs b/src/Data/Finite.hs
--- a/src/Data/Finite.hs
+++ b/src/Data/Finite.hs
@@ -1,13 +1,16 @@
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Finite
--- Copyright   :  (C) 2015 mniip
+-- Copyright   :  (C) 2015-2022 mniip
 -- License     :  BSD3
 -- Maintainer  :  mniip <mniip@mniip.com>
 -- Stability   :  experimental
 -- Portability :  portable
 --------------------------------------------------------------------------------
-{-# LANGUAGE TypeOperators, DataKinds, TypeFamilies, FlexibleContexts #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 module Data.Finite
     (
         Finite,
@@ -32,7 +35,8 @@
 
 import Data.Finite.Internal
 
--- | Convert an 'Integer' into a 'Finite', returning 'Nothing' if the input is out of bounds.
+-- | Convert an 'Integer' into a 'Finite', returning 'Nothing' if the input is
+-- out of bounds.
 packFinite :: KnownNat n => Integer -> Maybe (Finite n)
 packFinite x = result
     where
@@ -87,7 +91,8 @@
 weaken :: Finite n -> Finite (n + 1)
 weaken (Finite x) = Finite x
 
--- | Remove one inhabitant from the end. Returns 'Nothing' if the input was the removed inhabitant.
+-- | Remove one inhabitant from the end. Returns 'Nothing' if the input was the
+-- removed inhabitant.
 strengthen :: KnownNat n => Finite (n + 1) -> Maybe (Finite n)
 strengthen (Finite x) = result
     where
@@ -99,7 +104,8 @@
 shift :: Finite n -> Finite (n + 1)
 shift (Finite x) = Finite (x + 1)
 
--- | Remove one inhabitant from the beginning, shifting everything down by one. Returns 'Nothing' if the input was the removed inhabitant.
+-- | Remove one inhabitant from the beginning, shifting everything down by one.
+-- Returns 'Nothing' if the input was the removed inhabitant.
 unshift :: Finite (n + 1) -> Maybe (Finite n)
 unshift (Finite x) = if x < 1
     then Nothing
@@ -109,7 +115,8 @@
 weakenN :: (n <= m) => Finite n -> Finite m
 weakenN (Finite x) = Finite x
 
--- | Remove multiple inhabitants from the end. Returns 'Nothing' if the input was one of the removed inhabitants.
+-- | Remove multiple inhabitants from the end. Returns 'Nothing' if the input
+-- was one of the removed inhabitants.
 strengthenN :: (KnownNat n, n <= m) => Finite m -> Maybe (Finite n)
 strengthenN (Finite x) = result
     where
@@ -117,13 +124,16 @@
             then Just $ Finite x
             else Nothing
 
--- | Add multiple inhabitant in the beginning, shifting everything up by the amount of inhabitants added.
+-- | Add multiple inhabitant in the beginning, shifting everything up by the
+-- amount of inhabitants added.
 shiftN :: (KnownNat n, KnownNat m, n <= m) => Finite n -> Finite m
 shiftN fx@(Finite x) = result
     where
         result = Finite $ x + natVal result - natVal fx
 
--- | Remove multiple inhabitants from the beginning, shifting everything down by the amount of inhabitants removed. Returns 'Nothing' if the input was one of the removed inhabitants.
+-- | Remove multiple inhabitants from the beginning, shifting everything down by
+-- the amount of inhabitants removed. Returns 'Nothing' if the input was one of
+-- the removed inhabitants.
 unshiftN :: (KnownNat n, KnownNat m, n <= m) => Finite m -> Maybe (Finite n)
 unshiftN fx@(Finite x) = result
     where
@@ -135,7 +145,7 @@
 weakenProxy _ (Finite x) = Finite x
 
 strengthenProxy :: KnownNat n => proxy k -> Finite (n + k) -> Maybe (Finite n)
-strengthenProxy p (Finite x) = result
+strengthenProxy _ (Finite x) = result
     where
         result = if x < natVal (fromJust result)
             then Just $ Finite x
@@ -153,7 +163,8 @@
 add :: Finite n -> Finite m -> Finite (n + m)
 add (Finite x) (Finite y) = Finite $ x + y
 
--- | Subtract two 'Finite's. Returns 'Left' for negative results, and 'Right' for positive results. Note that this function never returns @'Left' 0@.
+-- | Subtract two 'Finite's. Returns 'Left' for negative results, and 'Right'
+-- for positive results. Note that this function never returns @'Left' 0@.
 sub :: Finite n -> Finite m -> Either (Finite m) (Finite n)
 sub (Finite x) (Finite y) = if x >= y
     then Right $ Finite $ x - y
@@ -171,7 +182,8 @@
 combineSum (Left (Finite x)) = Finite x
 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.
+-- | '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 GHC.TypeLits.* m)
 combineProduct (fx@(Finite x), Finite y) = Finite $ x + y * natVal fx
 
@@ -189,6 +201,8 @@
     where
         result = (Finite $ x `mod` natVal (fst result), Finite $ x `div` natVal (fst result))
 
--- | Verifies that a given 'Finite' is valid. Should always return 'True' unles you bring the @Data.Finite.Internal.Finite@ constructor into the scope, or use 'Unsafe.Coerce.unsafeCoerce' or other nasty hacks
+-- | Verifies that a given 'Finite' is valid. Should always return 'True' unless
+-- you bring the @Data.Finite.Internal.Finite@ constructor into the scope, or
+-- use 'Unsafe.Coerce.unsafeCoerce' or other nasty hacks.
 isValidFinite :: KnownNat n => Finite n -> Bool
 isValidFinite fx@(Finite x) = x < natVal fx && x >= 0
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
@@ -1,13 +1,15 @@
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Finite.Internal
--- Copyright   :  (C) 2015 mniip
+-- Copyright   :  (C) 2015-2022 mniip
 -- License     :  BSD3
 -- Maintainer  :  mniip <mniip@mniip.com>
 -- Stability   :  experimental
 -- Portability :  portable
 --------------------------------------------------------------------------------
-{-# LANGUAGE KindSignatures, DataKinds, DeriveGeneric #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE KindSignatures #-}
 module Data.Finite.Internal
     (
         Finite(Finite),
@@ -16,23 +18,25 @@
     )
     where
 
-import GHC.Read
-import GHC.TypeLits
-import GHC.Generics
 import Control.DeepSeq
 import Control.Monad
 import Data.Ratio
-import Text.Read.Lex
+import GHC.Generics
+import GHC.Read
+import GHC.TypeLits
 import Text.ParserCombinators.ReadPrec
+import Text.Read.Lex
 
--- | Finite number type. @'Finite' n@ is inhabited by exactly @n@ values. Invariants:
+-- | Finite number type. @'Finite' n@ is inhabited by exactly @n@ values
+-- the range @[0, n)@ including @0@ but excluding @n@. Invariants:
 --
 -- prop> getFinite x < natVal x
 -- prop> getFinite x >= 0
 newtype Finite (n :: Nat) = Finite Integer
                           deriving (Eq, Ord, Generic)
 
--- | Convert an 'Integer' into a 'Finite', throwing an error if the input is out of bounds.
+-- | Convert an 'Integer' into a 'Finite', throwing an error if the input is out
+-- of bounds.
 finite :: KnownNat n => Integer -> Finite n
 finite x = result
     where
@@ -58,29 +62,38 @@
                 else error "minBound: Finite 0 is uninhabited"
 
 instance KnownNat n => Enum (Finite n) where
+    succ fx@(Finite x) = if x == natVal fx - 1
+        then error "succ: bad argument"
+        else Finite $ succ x
+    pred (Finite x) = if x == 0
+        then error "pred: bad argument"
+        else Finite $ pred x
     fromEnum = fromEnum . getFinite
     toEnum = finite . toEnum
     enumFrom x = enumFromTo x maxBound
+    enumFromTo (Finite x) (Finite y) = Finite `fmap` enumFromTo x y
     enumFromThen x y = enumFromThenTo x y (if x >= y then minBound else maxBound)
+    enumFromThenTo (Finite x) (Finite y) (Finite z) = Finite `fmap` enumFromThenTo x y z
 
 instance Show (Finite n) where
     showsPrec d (Finite x) = showParen (d > 9) $ showString "finite " . showsPrec 10 x
 
 instance KnownNat n => Read (Finite n) where
-    readPrec = parens $ Text.ParserCombinators.ReadPrec.prec 10 $ do 
+    readPrec = parens $ Text.ParserCombinators.ReadPrec.prec 10 $ do
                  expectP (Ident "finite")
                  x <- readPrec
                  let result = finite x
-                 guard (x >= 0 && x < natVal result) 
+                 guard (x >= 0 && x < natVal result)
                  return result
 
--- | Modular arithmetic. Only the 'fromInteger' function is supposed to be useful.
+-- | 'Prelude.+', 'Prelude.-', and 'Prelude.*' implement arithmetic modulo @n@.
+-- The 'fromInteger' function raises an error for inputs outside of bounds.
 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
     fx@(Finite x) * Finite y = Finite $ (x * y) `mod` natVal fx
     abs fx = fx
-    signum _ = fromInteger 1
+    signum (Finite x) = fromInteger $ if x == 0 then 0 else 1
     fromInteger x = result
         where
             result = if x < natVal result && x >= 0
@@ -90,7 +103,8 @@
 instance KnownNat n => Real (Finite n) where
     toRational (Finite x) = x % 1
 
--- | __Not__ modular arithmetic.
+-- | 'quot' and 'rem' are the same as 'div' and 'mod' and they implement regular
+-- division of numbers in the range @[0, n)@, __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
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,548 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+module Main where
+
+import Control.Exception
+import Control.DeepSeq
+import Data.List
+import Data.Maybe
+import Data.Proxy
+import Data.Type.Equality
+import GHC.TypeLits
+import System.Exit
+import Test.QuickCheck
+import Unsafe.Coerce
+
+import Data.Finite
+import Data.Finite.Internal
+
+instance KnownNat n => Arbitrary (Finite n) where
+    arbitrary
+        | natVal @n Proxy == 0 = discard
+        | otherwise = oneof
+            [ pure (Finite 0)
+            , pure (Finite $ natVal @n Proxy - 1)
+            , Finite . (`mod` natVal @n Proxy) <$> arbitrary
+            ]
+    shrink (Finite x) = mapMaybe packFinite $ shrink x
+
+withNat' :: forall prop. Testable prop => Gen Integer -> (Integer -> [Integer]) -> (forall n. KnownNat n => (forall i. Num i => i) -> Proxy n -> prop) -> Property
+withNat' gen shr prop = forAllShrinkBlind gen shr $ \n -> case someNatVal n of
+    Nothing -> counterexample "withNat" False
+    Just (SomeNat p) -> counterexample ("@" ++ show n) $ prop (fromInteger (natVal p)) p
+
+withNat :: forall prop. Testable prop => (forall n. KnownNat n => (forall i. Num i => i) -> Proxy n -> prop) -> Property
+withNat = withNat' (getNonNegative <$> arbitrary) (map getNonNegative . shrink . NonNegative)
+
+withNatPos :: forall prop. Testable prop => (forall n. KnownNat n => (forall i. Num i => i) -> Proxy n -> prop) -> Property
+withNatPos = withNat' (getPositive <$> arbitrary) (map getPositive . shrink . Positive)
+
+unsafeWithKnownNat :: forall n prop. Testable prop => Integer -> (KnownNat n => prop) -> Property
+unsafeWithKnownNat n prop = case someNatVal n of
+    Nothing -> counterexample "unsafeWithKnownNat: someNatVal" False
+    Just (SomeNat (_ :: Proxy n')) -> case unsafeCoerce Refl :: n :~: n' of
+        Refl -> property prop
+
+newtype IneqCond (n :: Nat) (m :: Nat) = IneqCond ((n <= m) => Property)
+unsafeWithInequality :: forall (n :: Nat) (m :: Nat) prop. Testable prop => ((n <= m) => prop) -> Property
+unsafeWithInequality prop =
+    case unsafeCoerce (IneqCond @n @m $ property prop) :: IneqCond 0 1 of
+        IneqCond prop' -> prop'
+
+prop_isvalid_under = withNat $ \_ (_ :: Proxy n) x ->
+    x < 0 ==> expectFailure $ isValidFinite @n (Finite x)
+prop_isvalid_over = withNat $ \n (_ :: Proxy n) x ->
+    x >= n ==> expectFailure $ isValidFinite @n (Finite x)
+
+prop_valid_finite = withNat $ \_ (_ :: Proxy n) x -> ioProperty $
+    evaluate (isValidFinite $ finite @n x)
+        `catch` \(_ :: ErrorCall) -> pure True
+prop_getFinite_finite = withNat $ \_ (_ :: Proxy n) x -> ioProperty $
+    evaluate (getFinite (finite @n x) == x)
+        `catch` \(_ :: ErrorCall) -> pure True
+prop_finite_getFinite = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x ->
+        finite (getFinite @n x) === x
+
+prop_valid_maxBound = withNat $ \n (_ :: Proxy n) ->
+    n > 0 ==> isValidFinite (maxBound @(Finite n))
+prop_maxBound_max = withNat $ \n (_ :: Proxy n) ->
+    property $ \x ->
+        n > 0 ==> maxBound @(Finite n) >= x
+
+prop_valid_minBound = withNat $ \n (_ :: Proxy n) ->
+    n > 0 ==> isValidFinite (minBound @(Finite n))
+prop_minBound_min = withNat $ \n (_ :: Proxy n) ->
+    property $ \x ->
+        n > 0 ==> minBound @(Finite n) <= x
+
+prop_valid_toEnum = withNat $ \_ (_ :: Proxy n) x -> ioProperty $
+    evaluate (isValidFinite $ toEnum @(Finite n) x)
+        `catch` \(_ :: ErrorCall) -> pure True
+prop_fromEnum_toEnum = withNat $ \_ (_ :: Proxy n) x -> ioProperty $
+    evaluate (fromEnum (toEnum @(Finite n) x) == x)
+        `catch` \(_ :: ErrorCall) -> pure True
+prop_toEnum_fromEnum = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x ->
+        toEnum @(Finite n) (fromEnum x) == x
+
+prop_valid_enumFrom = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x ->
+        all isValidFinite $ enumFrom @(Finite n) x
+prop_getFinite_enumFrom = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x ->
+        map getFinite (enumFrom @(Finite n) x)
+            === takeWhile (isJust . packFinite @n) (enumFrom (getFinite x))
+
+prop_valid_enumFromTo = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y ->
+        all isValidFinite $ enumFromTo @(Finite n) x y
+prop_getFinite_enumFromTo = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y ->
+        map getFinite (enumFromTo @(Finite n) x y)
+            === enumFromTo (getFinite x) (getFinite y)
+
+prop_valid_enumFromThen = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y ->
+        x /= y ==> all isValidFinite $ enumFromThen @(Finite n) x y
+prop_getFinite_enumFromThen = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y ->
+        x /= y ==> map getFinite (enumFromThen @(Finite n) x y)
+            === takeWhile (isJust . packFinite @n) (enumFromThen (getFinite x) (getFinite y))
+
+prop_valid_enumFromThenTo = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y z ->
+        x /= y ==> all isValidFinite $ enumFromThenTo @(Finite n) x y z
+prop_getFinite_enumFromThenTo = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y z ->
+        x /= y ==> map getFinite (enumFromThenTo @(Finite n) x y z)
+            === enumFromThenTo (getFinite x) (getFinite y) (getFinite z)
+
+prop_nonint_succ = withNat' genBig shrinkBig $ \_ (_ :: Proxy n) ->
+    forAllShrink genBig shrinkBig $ \x ->
+        case packFinite @n $ succ x of
+            Nothing -> discard
+            Just y -> y === succ (finite x)
+    where
+        big = toInteger (maxBound :: Int)
+        genBig = (big +) . getNonNegative <$> arbitrary
+        shrinkBig = map ((big +) . getNonNegative) . shrink . NonNegative . subtract big
+
+prop_valid_read = withNatPos $ \_ (_ :: Proxy n) ->
+    withNatPos $ \_ (_ :: Proxy m) ->
+        property $ \x -> ioProperty $
+            evaluate (isValidFinite $ read @(Finite n) (show @(Finite m) x))
+                `catch` \(_ :: ErrorCall) -> pure True
+prop_read_show = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x ->
+        read (show @(Finite n) x) === x
+
+prop_valid_plus = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y ->
+        isValidFinite @n $ x + y
+prop_getFinite_plus = withNatPos $ \n (_ :: Proxy n) ->
+    property $ \x y ->
+        (getFinite @n (x + y) - (getFinite x + getFinite y)) `mod` n === 0
+
+prop_valid_minus = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y ->
+        isValidFinite @n $ x - y
+prop_getFinite_minus = withNatPos $ \n (_ :: Proxy n) ->
+    property $ \x y ->
+        (getFinite @n (x - y) - (getFinite x - getFinite y)) `mod` n === 0
+
+prop_valid_times = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y ->
+        isValidFinite @n $ x * y
+prop_getFinite_times = withNatPos $ \n (_ :: Proxy n) ->
+    property $ \x y ->
+        (getFinite @n (x * y) - (getFinite x * getFinite y)) `mod` n === 0
+
+prop_valid_negate = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x ->
+        isValidFinite @n $ -x
+prop_getFinite_negate = withNatPos $ \n (_ :: Proxy n) ->
+    property $ \x ->
+        (getFinite @n (-x) - (- getFinite x)) `mod` n === 0
+
+prop_valid_abs = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x ->
+        isValidFinite @n $ abs x
+prop_getFinite_abs = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x ->
+        getFinite @n (abs x) === abs (getFinite x)
+
+prop_valid_signum = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x -> ioProperty $
+        evaluate (isValidFinite @n $ signum x)
+            `catch` \(_ :: ErrorCall) -> pure True
+
+prop_getFinite_signum = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x -> ioProperty $
+        evaluate (getFinite @n (signum x) == signum (getFinite x))
+            `catch` \(_ :: ErrorCall) -> pure True
+
+prop_valid_fromInteger = withNatPos $ \_ (_ :: Proxy n) x -> ioProperty $
+    evaluate (isValidFinite $ fromInteger @(Finite n) x)
+        `catch` \(_ :: ErrorCall) -> pure True
+prop_toInteger_fromInteger = withNat $ \_ (_ :: Proxy n) x -> ioProperty $
+    evaluate (toInteger (fromInteger @(Finite n) x) == x)
+        `catch` \(_ :: ErrorCall) -> pure True
+prop_fromInteger_toInteger = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x ->
+        fromInteger (toInteger @(Finite n) x) === x
+
+prop_valid_quot = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y ->
+        y /= 0 ==> isValidFinite @n $ x `quot` y
+prop_getFinite_quot = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y ->
+        y /= 0 ==> getFinite @n (x `quot` y) === getFinite x `quot` getFinite y
+
+prop_valid_rem = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y ->
+        y /= 0 ==> isValidFinite @n $ x `rem` y
+prop_getFinite_rem = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y ->
+        y /= 0 ==> getFinite @n (x `rem` y) === getFinite x `rem` getFinite y
+
+prop_valid_div = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y ->
+        y /= 0 ==> isValidFinite @n $ x `div` y
+prop_getFinite_div = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y ->
+        y /= 0 ==> getFinite @n (x `div` y) === getFinite x `div` getFinite y
+
+prop_valid_mod = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y ->
+        y /= 0 ==> isValidFinite @n $ x `mod` y
+prop_getFinite_mod = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x y ->
+        y /= 0 ==> getFinite @n (x `mod` y) === getFinite x `mod` getFinite y
+
+prop_force = withNat $ \_ (_ :: Proxy n) ->
+    expectFailure $ rnf @(Finite n) (error "Expected exception") `seq` True
+
+prop_valid_packFinite = withNat $ \_ (_ :: Proxy n) x ->
+    maybe True isValidFinite $ packFinite @n x
+prop_getFinite_packFinite = withNat $ \_ (_ :: Proxy n) x ->
+    maybe (property True) ((x ===) . getFinite) $ packFinite @n x
+prop_finite_packFinite = withNat $ \_ (_ :: Proxy n) x -> ioProperty $
+    case packFinite @n x of
+        Nothing -> (evaluate (finite @n x) >> pure False)
+            `catch` \(_ :: ErrorCall) -> pure True
+        Just y -> evaluate (y == finite x)
+
+prop_valid_finites = withNat $ \_ (_ :: Proxy n) ->
+    all isValidFinite $ finites @n
+prop_finites_minMax = withNatPos $ \_ (_ :: Proxy n) ->
+    minBound `elem` finites @n .&&. maxBound `elem` finites @n
+prop_finites_ordered = withNat $ \_ (_ :: Proxy n) ->
+    finites @n === sort finites
+prop_finites_all = withNat $ \_ (_ :: Proxy n) ->
+    property $ \x ->
+        x {- could be discard -} `seq` x `elem` finites @n
+
+prop_valid_modulo = withNatPos $ \_ (_ :: Proxy n) x ->
+    isValidFinite $ modulo @n x
+prop_getFinite_modulo = withNatPos $ \n (_ :: Proxy n) x ->
+    (getFinite (modulo @n x) - x) `mod` n === 0
+
+
+prop_getFinite_equals = withNatPos $ \_ (_ :: Proxy n) ->
+    withNatPos $ \_ (_ :: Proxy m) ->
+        property $ \x y ->
+            (x `equals` y) === (getFinite @n x == getFinite @m y)
+
+prop_getFinite_cmp = withNatPos $ \_ (_ :: Proxy n) ->
+    withNatPos $ \_ (_ :: Proxy m) ->
+        property $ \x y ->
+            (x `cmp` y) === (getFinite @n x `compare` getFinite @m y)
+
+prop_valid_natToFinite = withNat $ \n (_ :: Proxy n) ->
+    withNatPos $ \m (_ :: Proxy m) ->
+        n + 1 <= m ==> unsafeWithInequality @(n + 1) @m @Bool $
+            isValidFinite $ natToFinite @n @m Proxy
+prop_getFinite_natToFinite = withNat $ \n (_ :: Proxy n) ->
+    withNatPos $ \m (_ :: Proxy m) ->
+        n + 1 <= m ==> unsafeWithInequality @(n + 1) @m @Property $
+            getFinite (natToFinite @n @m Proxy) === natVal @n Proxy
+
+prop_valid_weaken = withNatPos $ \n (_ :: Proxy n) ->
+    unsafeWithKnownNat @(n + 1) (n + 1) $
+        property $ \x ->
+            isValidFinite $ weaken @n x
+prop_finites_weaken = withNat $ \n (_ :: Proxy n) ->
+    unsafeWithKnownNat @(n + 1) (n + 1) $
+        map (weaken @n) finites === init finites
+
+prop_valid_strengthen = withNat $ \n (_ :: Proxy n) ->
+    unsafeWithKnownNat @(n + 1) (n + 1) $
+        property $ \x ->
+            maybe True isValidFinite $ strengthen @n x
+prop_finites_strengthen = withNat $ \n (_ :: Proxy n) ->
+    unsafeWithKnownNat @(n + 1) (n + 1) $
+        map (strengthen @n) finites === map Just finites ++ [Nothing]
+
+prop_valid_shift = withNatPos $ \n (_ :: Proxy n) ->
+    unsafeWithKnownNat @(n + 1) (n + 1) $
+        property $ \x ->
+            isValidFinite $ shift @n x
+prop_finites_shift = withNat $ \n (_ :: Proxy n) ->
+    unsafeWithKnownNat @(n + 1) (n + 1) $
+        map (shift @n) finites === tail finites
+
+prop_valid_unshift = withNat $ \n (_ :: Proxy n) ->
+    unsafeWithKnownNat @(n + 1) (n + 1) $
+        property $ \x ->
+            maybe True isValidFinite $ unshift @n x
+prop_finites_unshift = withNat $ \n (_ :: Proxy n) ->
+    unsafeWithKnownNat @(n + 1) (n + 1) $
+        map (unshift @n) finites === [Nothing] ++ map Just finites
+
+prop_valid_weakenN = withNatPos $ \n (_ :: Proxy n) ->
+    withNatPos $ \m (_ :: Proxy m) ->
+        n <= m ==> unsafeWithInequality @n @m @Property $
+            property $ \x ->
+                isValidFinite $ weakenN @n @m x
+prop_finites_weakenN = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        n <= m ==> unsafeWithInequality @n @m @Property $
+            map (weakenN @n @m) finites === take n finites
+
+prop_valid_strengthenN = withNat $ \n (_ :: Proxy n) ->
+    withNatPos $ \m (_ :: Proxy m) ->
+        n <= m ==> unsafeWithInequality @n @m @Property $
+            property $ \x ->
+                maybe True isValidFinite $ strengthenN @n @m x
+prop_finites_strengthenN = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        n <= m ==> unsafeWithInequality @m @n @Property $
+            map (strengthenN @m @n) finites === take n (map Just finites) ++ replicate (n - m) Nothing
+
+prop_valid_shiftN = withNatPos $ \n (_ :: Proxy n) ->
+    withNatPos $ \m (_ :: Proxy m) ->
+        n <= m ==> unsafeWithInequality @n @m @Property $
+            property $ \x ->
+                isValidFinite $ shiftN @n @m x
+prop_finites_shiftN = withNat $ \n (_ :: Proxy n) ->
+    withNatPos $ \m (_ :: Proxy m) ->
+        n <= m ==> unsafeWithInequality @n @m @Property $
+            map (shiftN @n @m) finites === drop (m - n) finites
+
+prop_valid_unshiftN = withNatPos $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        n <= m ==> unsafeWithInequality @n @m @Property $
+            property $ \x ->
+                maybe True isValidFinite $ unshiftN @n @m x
+prop_finites_unshiftN = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        m <= n ==> unsafeWithInequality @m @n @Property $
+            map (unshiftN @m @n) finites === replicate (n - m) Nothing ++ drop (m - n) (map Just finites)
+
+prop_valid_weakenProxy = withNatPos $ \n (_ :: Proxy n) ->
+    withNat $ \k (_ :: Proxy k) ->
+        unsafeWithKnownNat @(n + k) (n + k) $
+            property $ \x ->
+                isValidFinite $ weakenProxy @Proxy @k @n Proxy x
+prop_finites_weakenProxy = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \k (_ :: Proxy k) ->
+        unsafeWithKnownNat @(n + k) (n + k) $
+            map (weakenProxy @Proxy @k @n Proxy) finites === take n finites
+
+prop_valid_strengthenProxy = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \k (_ :: Proxy k) ->
+        unsafeWithKnownNat @(n + k) (n + k) $
+            property $ \x ->
+                maybe True isValidFinite $ strengthenProxy @n @Proxy @k Proxy x
+prop_finites_strengthenProxy = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \k (_ :: Proxy k) ->
+        unsafeWithKnownNat @(n + k) (n + k) $
+            map (strengthenProxy @n @Proxy @k Proxy) finites === take n (map Just finites) ++ replicate k Nothing
+
+prop_valid_shiftProxy = withNatPos $ \n (_ :: Proxy n) ->
+    withNat $ \k (_ :: Proxy k) ->
+        unsafeWithKnownNat @(n + k) (n + k) $
+            property $ \x ->
+                isValidFinite $ shiftProxy @k @Proxy @n Proxy x
+prop_finites_shiftProxy = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \k (_ :: Proxy k) ->
+        unsafeWithKnownNat @(n + k) (n + k) $
+            map (shiftProxy @k @Proxy @n Proxy) finites === drop k finites
+
+prop_valid_unshiftProxy = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \k (_ :: Proxy k) ->
+        unsafeWithKnownNat @(n + k) (n + k) $
+            property $ \x ->
+                maybe True isValidFinite $ unshiftProxy @k @Proxy @n Proxy  x
+prop_finites_unshiftProxy = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \k (_ :: Proxy k) ->
+        unsafeWithKnownNat @(n + k) (n + k) $
+            map (unshiftProxy @k @Proxy @n Proxy) finites === replicate k Nothing ++ map Just finites
+
+prop_strengthen_weaken = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x ->
+        strengthen @n (weaken x) === Just x
+prop_weaken_strengthen = withNat $ \n (_ :: Proxy n) ->
+    unsafeWithKnownNat @(n + 1) (n + 1) $
+        property $ \x ->
+            maybe True (== x) (weaken @n <$> strengthen x)
+
+prop_unshift_shift = withNatPos $ \_ (_ :: Proxy n) ->
+    property $ \x ->
+        unshift @n (shift x) === Just x
+prop_shift_unshift = withNat $ \n (_ :: Proxy n) ->
+    unsafeWithKnownNat @(n + 1) (n + 1) $
+        property $ \x ->
+            maybe True (== x) (shift @n <$> unshift x)
+
+prop_strengthenN_weakenN = withNatPos $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        m <= n ==> unsafeWithInequality @m @n @Property $
+            property $ \x ->
+                strengthenN @m @n (weakenN x) === Just x
+prop_weakenN_strengthenN = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        n <= m ==> unsafeWithInequality @n @m @Property $
+            property $ \x ->
+                maybe True (== x) (weakenN @n @m <$> strengthenN x)
+
+prop_unshiftN_shiftN = withNatPos $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        m <= n ==> unsafeWithInequality @m @n @Property $
+            property $ \x ->
+                unshiftN @m @n (shiftN x) === Just x
+prop_shiftN_unshiftN = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        n <= m ==> unsafeWithInequality @n @m @Property $
+            property $ \x ->
+                maybe True (== x) (shiftN @n @m <$> unshiftN x)
+
+prop_strengthenProxy_weakenProxy = withNatPos $ \_ (_ :: Proxy n) ->
+    withNat $ \_ (_ :: Proxy k) ->
+        property $ \x ->
+            strengthenProxy @n @Proxy @k Proxy (weakenProxy Proxy x) === Just x
+prop_weakenProxy_strengthenProxy = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \k (_ :: Proxy k) ->
+        unsafeWithKnownNat @(n + k) (n + k) $
+            property $ \x ->
+                maybe True (== x) (weakenProxy @Proxy @k @n Proxy <$> strengthenProxy Proxy x)
+
+prop_unshiftProxy_shiftProxy = withNatPos $ \_ (_ :: Proxy n) ->
+    withNat $ \_ (_ :: Proxy k) ->
+        property $ \x ->
+            unshiftProxy @k @Proxy @n Proxy (shiftProxy Proxy x) === Just x
+prop_shiftProxy_unshiftProxy = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \k (_ :: Proxy k) ->
+        unsafeWithKnownNat @(n + k) (n + k) $
+            property $ \x ->
+                maybe True (== x) (shiftProxy @k @Proxy @n Proxy <$> unshiftProxy Proxy x)
+
+prop_valid_add = withNatPos $ \n (_ :: Proxy n) ->
+    withNatPos $ \m (_ :: Proxy m) ->
+        unsafeWithKnownNat @(n + m) (n + m) $
+            property $ \x y ->
+                isValidFinite $ add @n @m x y
+prop_getFinite_add = withNatPos $ \_ (_ :: Proxy n) ->
+    withNatPos $ \_ (_ :: Proxy m) ->
+        property $ \x y ->
+            getFinite (add @n @m x y) === getFinite x + getFinite y
+
+prop_valid_sub = withNatPos $ \_ (_ :: Proxy n) ->
+    withNatPos $ \_ (_ :: Proxy m) ->
+        property $ \x y ->
+            either isValidFinite isValidFinite $ sub @n @m x y
+prop_getFinite_sub = withNatPos $ \_ (_ :: Proxy n) ->
+    withNatPos $ \_ (_ :: Proxy m) ->
+        property $ \x y ->
+            either (negate . getFinite) getFinite (sub @n @m x y) === getFinite x - getFinite y
+prop_sub_Left_0 = withNatPos $ \_ (_ :: Proxy n) ->
+    withNatPos $ \_ (_ :: Proxy m) ->
+        property $ \x y ->
+            sub @n @m x y =/= Left 0
+
+prop_valid_multiply = withNatPos $ \n (_ :: Proxy n) ->
+    withNatPos $ \m (_ :: Proxy m) ->
+        unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $
+            property $ \x y ->
+                isValidFinite $ multiply @n @m x y
+prop_getFinite_multiply = withNatPos $ \_ (_ :: Proxy n) ->
+    withNatPos $ \_ (_ :: Proxy m) ->
+        property $ \x y ->
+            getFinite (multiply @n @m x y) === getFinite x * getFinite y
+
+prop_valid_combineSum = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        unsafeWithKnownNat @(n + m) (n + m) $
+            property $ \x ->
+                isValidFinite $ combineSum @n @m x
+prop_finites_combineSum = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        unsafeWithKnownNat @(n + m) (n + m) $
+            map (combineSum @n @m) (map Left finites ++ map Right finites) === finites
+
+prop_valid_combineProduct = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $
+            property $ \x ->
+                isValidFinite (combineProduct @n @m x)
+prop_finites_combineProduct = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $
+            map (combineProduct @n @m) [(x, y) | y <- finites, x <- finites] === finites
+
+prop_valid_separateSum = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        unsafeWithKnownNat @(n + m) (n + m) $
+            property $ \x ->
+                either isValidFinite isValidFinite $ separateSum @n @m x
+prop_finites_separateSum = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        unsafeWithKnownNat @(n + m) (n + m) $
+            map (separateSum @n @m) finites === map Left finites ++ map Right finites
+
+prop_valid_separateProduct = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $
+            property $ \x ->
+                x {- could be discard -} `seq` isValidFinite (fst $ separateProduct @n @m x)
+                    .&&. isValidFinite (snd $ separateProduct @n @m x)
+prop_finites_separateProduct = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $
+            map (separateProduct @n @m) finites === [(x, y) | y <- finites, x <- finites]
+
+prop_combineSum_separateSum = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        unsafeWithKnownNat @(n + m) (n + m) $
+            property $ \x ->
+                combineSum @n @m (separateSum x) === x
+prop_separateSum_combineSum = withNat $ \_ (_ :: Proxy n) ->
+    withNat $ \_ (_ :: Proxy m) ->
+        property $ \x ->
+            separateSum @n @m (combineSum x) === x
+
+prop_combineProduct_separateProduct = withNat $ \n (_ :: Proxy n) ->
+    withNat $ \m (_ :: Proxy m) ->
+        unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $
+            property $ \x ->
+                x {- could be discard -} `seq` combineProduct @n @m (separateProduct x) === x
+prop_separateProduct_combineProduct = withNat $ \_ (_ :: Proxy n) ->
+    withNat $ \_ (_ :: Proxy m) ->
+        property $ \x ->
+            force x {- could be discard -} `seq` separateProduct @n @m (combineProduct x) === x
+
+return []
+main = $quickCheckAll >>= \case
+    True -> pure ()
+    False -> exitFailure