diff --git a/opentheory-prime.cabal b/opentheory-prime.cabal
--- a/opentheory-prime.cabal
+++ b/opentheory-prime.cabal
@@ -1,16 +1,16 @@
 name: opentheory-prime
-version: 1.9
+version: 1.21
 category: Number Theory
 synopsis: Prime numbers
 license: MIT
 license-file: LICENSE
 cabal-version: >= 1.8.0.6
 build-type: Simple
-author: Joe Hurd <joe@gilith.com>
-maintainer: Joe Hurd <joe@gilith.com>
+author: Joe Leslie-Hurd <joe@gilith.com>
+maintainer: Joe Leslie-Hurd <joe@gilith.com>
 description:
-  Prime numbers
-  Automatically generated from the opentheory package haskell-prime-1.9
+  Prime numbers - automatically generated from the opentheory package
+  haskell-prime-1.21
 
 library
   build-depends:
@@ -18,7 +18,7 @@
     random >= 1.0.1.1 && < 2.0,
     QuickCheck >= 2.4.0.1 && < 3.0,
     opentheory-primitive >= 1.0 && < 2.0,
-    opentheory >= 1.56 && <= 1.61
+    opentheory >= 1.73 && <= 1.74
 
   hs-source-dirs: src
 
@@ -34,7 +34,7 @@
     random >= 1.0.1.1 && < 2.0,
     QuickCheck >= 2.4.0.1 && < 3.0,
     opentheory-primitive >= 1.0 && < 2.0,
-    opentheory >= 1.56 && <= 1.61
+    opentheory >= 1.73 && <= 1.74
 
   hs-source-dirs: src, testsrc
 
diff --git a/src/OpenTheory/Number/Natural/Prime.hs b/src/OpenTheory/Number/Natural/Prime.hs
--- a/src/OpenTheory/Number/Natural/Prime.hs
+++ b/src/OpenTheory/Number/Natural/Prime.hs
@@ -3,7 +3,7 @@
 description: Prime numbers
 license: MIT
 
-maintainer: Joe Hurd <joe@gilith.com>
+maintainer: Joe Leslie-Hurd <joe@gilith.com>
 stability: provisional
 portability: portable
 -}
diff --git a/src/OpenTheory/Number/Natural/Prime/Sieve.hs b/src/OpenTheory/Number/Natural/Prime/Sieve.hs
--- a/src/OpenTheory/Number/Natural/Prime/Sieve.hs
+++ b/src/OpenTheory/Number/Natural/Prime/Sieve.hs
@@ -3,7 +3,7 @@
 description: Prime numbers
 license: MIT
 
-maintainer: Joe Hurd <joe@gilith.com>
+maintainer: Joe Leslie-Hurd <joe@gilith.com>
 stability: provisional
 portability: portable
 -}
diff --git a/testsrc/Test.hs b/testsrc/Test.hs
--- a/testsrc/Test.hs
+++ b/testsrc/Test.hs
@@ -3,7 +3,7 @@
 description: Prime numbers - testing
 license: MIT
 
-maintainer: Joe Hurd <joe@gilith.com>
+maintainer: Joe Leslie-Hurd <joe@gilith.com>
 stability: provisional
 portability: portable
 -}
@@ -12,12 +12,16 @@
 where
 
 import qualified OpenTheory.Data.Stream as Data.Stream
+import qualified OpenTheory.Number.Natural as Number.Natural
 import qualified OpenTheory.Number.Natural.Geometric
   as Number.Natural.Geometric
 import qualified OpenTheory.Number.Natural.Prime as Number.Natural.Prime
 import qualified OpenTheory.Primitive.Random as Primitive.Random
 import qualified OpenTheory.Primitive.Test as Primitive.Test
 
+assertion0 :: Bool
+assertion0 = not (Data.Stream.nth Number.Natural.Prime.all 0 == 0)
+
 proposition0 :: Primitive.Random.Random -> Bool
 proposition0 r =
   let (i, r') = Number.Natural.Geometric.fromRandom r in
@@ -29,12 +33,22 @@
 proposition1 r =
   let (i, r') = Number.Natural.Geometric.fromRandom r in
   let (j, _) = Number.Natural.Geometric.fromRandom r' in
-  0 <
-  Data.Stream.nth Number.Natural.Prime.all (i + j + 1) `mod`
-  Data.Stream.nth Number.Natural.Prime.all i
+  not
+    (Number.Natural.divides (Data.Stream.nth Number.Natural.Prime.all i)
+       (Data.Stream.nth Number.Natural.Prime.all (i + j + 1)))
 
+proposition2 :: Primitive.Random.Random -> Bool
+proposition2 r =
+  let (n, r') = Number.Natural.fromRandom r in
+  let (i, _) = Number.Natural.Geometric.fromRandom r' in
+  any (\p -> Number.Natural.divides p (n + 2))
+    (Data.Stream.take' Number.Natural.Prime.all i) ||
+  Data.Stream.nth Number.Natural.Prime.all i <= n + 2
+
 main :: IO ()
 main =
-    do Primitive.Test.check "Proposition 0:\n  !r.\n    let (i, r') <- H.Geometric.fromRandom r in\n    let (j, r'') <- H.Geometric.fromRandom r' in\n    H.nth H.Prime.all i <= H.nth H.Prime.all j <=> i <= j\n  " proposition0
-       Primitive.Test.check "Proposition 1:\n  !r.\n    let (i, r') <- H.Geometric.fromRandom r in\n    let (j, r'') <- H.Geometric.fromRandom r' in\n    0 < H.nth H.Prime.all (i + j + 1) mod H.nth H.Prime.all i\n  " proposition1
+    do Primitive.Test.assert "Assertion 0:\n  ~(H.nth H.Prime.all 0 = 0)\n  " assertion0
+       Primitive.Test.check "Proposition 0:\n  !r.\n    let (i, r') <- H.Geometric.fromRandom r in\n    let (j, r'') <- H.Geometric.fromRandom r' in\n    H.nth H.Prime.all i <= H.nth H.Prime.all j <=> i <= j\n  " proposition0
+       Primitive.Test.check "Proposition 1:\n  !r.\n    let (i, r') <- H.Geometric.fromRandom r in\n    let (j, r'') <- H.Geometric.fromRandom r' in\n    ~H.divides (H.nth H.Prime.all i) (H.nth H.Prime.all (i + j + 1))\n  " proposition1
+       Primitive.Test.check "Proposition 2:\n  !r.\n    let (n, r') <- H.fromRandom r in\n    let (i, r'') <- H.Geometric.fromRandom r' in\n    any (\\p. H.divides p (n + 2)) (H.take' H.Prime.all i) \\/\n    H.nth H.Prime.all i <= n + 2\n  " proposition2
        return ()