diff --git a/opentheory-divides.cabal b/opentheory-divides.cabal
--- a/opentheory-divides.cabal
+++ b/opentheory-divides.cabal
@@ -1,5 +1,5 @@
 name: opentheory-divides
-version: 1.57
+version: 1.61
 category: Number Theory
 synopsis: The divides relation on natural numbers
 license: MIT
@@ -10,14 +10,14 @@
 maintainer: Joe Leslie-Hurd <joe@gilith.com>
 description:
   The divides relation on natural numbers - this package was automatically
-  generated from the OpenTheory package natural-divides-1.57
+  generated from the OpenTheory package natural-divides-1.61
 
 library
   build-depends:
     base >= 4.0 && < 5.0,
     QuickCheck >= 2.4.0.1 && < 3.0,
     opentheory-primitive >= 1.5 && < 2.0,
-    opentheory >= 1.195 && < 1.198
+    opentheory >= 1.198 && < 1.199
   hs-source-dirs: src
   ghc-options: -Wall
   exposed-modules:
@@ -29,7 +29,7 @@
     base >= 4.0 && < 5.0,
     QuickCheck >= 2.4.0.1 && < 3.0,
     opentheory-primitive >= 1.5 && < 2.0,
-    opentheory >= 1.195 && < 1.198
+    opentheory >= 1.198 && < 1.199
   hs-source-dirs: src
   ghc-options: -Wall
   main-is: Test.hs
diff --git a/src/OpenTheory/Natural/Divides.hs b/src/OpenTheory/Natural/Divides.hs
--- a/src/OpenTheory/Natural/Divides.hs
+++ b/src/OpenTheory/Natural/Divides.hs
@@ -13,9 +13,6 @@
 
 import qualified OpenTheory.Primitive.Natural as Natural
 
-divides :: Natural.Natural -> Natural.Natural -> Bool
-divides a b = if a == 0 then b == 0 else b `mod` a == 0
-
 egcd ::
   Natural.Natural -> Natural.Natural ->
     (Natural.Natural, (Natural.Natural, Natural.Natural))
@@ -28,3 +25,16 @@
       let (g, (s, t)) = egcd c (b `mod` c) in
       let u = s + b `div` c * t in
       (g, (u, t + a `div` b * u))
+
+chineseRemainder ::
+  Natural.Natural -> Natural.Natural -> Natural.Natural ->
+    Natural.Natural -> Natural.Natural
+chineseRemainder a b =
+  let (_, (s, t)) = egcd a b in
+  let ab = a * b in
+  let sa = s * a in
+  let tb = (a - t) * b in
+  \x y -> (x * tb + y * sa) `mod` ab
+
+divides :: Natural.Natural -> Natural.Natural -> Bool
+divides a b = if a == 0 then b == 0 else b `mod` a == 0
diff --git a/src/Test.hs b/src/Test.hs
--- a/src/Test.hs
+++ b/src/Test.hs
@@ -38,9 +38,60 @@
 
 proposition6 ::
   Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool
-proposition6 a b =
-  let (g, (s, t)) = Divides.egcd (a + 1) b in t * b + g == s * (a + 1)
+proposition6 ap b =
+  let a = ap + 1 in let (_, (_, t)) = Divides.egcd a b in t < a
 
+proposition7 ::
+  Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool
+proposition7 ap b =
+  let a = ap + 1 in let (_, (s, _)) = Divides.egcd a b in s < max b 2
+
+proposition8 ::
+  Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool
+proposition8 ap b =
+  let a = ap + 1 in
+  let (g, (s, t)) = Divides.egcd a b in
+  t * b + g == s * a
+
+proposition9 ::
+  Primitive.Natural.Natural -> Primitive.Natural.Natural ->
+    Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool
+proposition9 ap bp xp yp =
+  let aq = ap + 1 in
+  let bq = bp + 1 in
+  let g = fst (Divides.egcd aq bq) in
+  let a = aq `div` g in
+  let b = bq `div` g in
+  let x = xp `mod` a in
+  let y = yp `mod` b in
+  Divides.chineseRemainder a b x y < a * b
+
+proposition10 ::
+  Primitive.Natural.Natural -> Primitive.Natural.Natural ->
+    Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool
+proposition10 ap bp xp yp =
+  let aq = ap + 1 in
+  let bq = bp + 1 in
+  let g = fst (Divides.egcd aq bq) in
+  let a = aq `div` g in
+  let b = bq `div` g in
+  let x = xp `mod` a in
+  let y = yp `mod` b in
+  Divides.chineseRemainder a b x y `mod` a == x
+
+proposition11 ::
+  Primitive.Natural.Natural -> Primitive.Natural.Natural ->
+    Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool
+proposition11 ap bp xp yp =
+  let aq = ap + 1 in
+  let bq = bp + 1 in
+  let g = fst (Divides.egcd aq bq) in
+  let a = aq `div` g in
+  let b = bq `div` g in
+  let x = xp `mod` a in
+  let y = yp `mod` b in
+  Divides.chineseRemainder a b x y `mod` b == y
+
 main :: IO ()
 main =
     do check "Proposition 0:\n  !a. divides a 0\n  " proposition0
@@ -49,5 +100,10 @@
        check "Proposition 3:\n  !a b. divides (fst (egcd a b)) a\n  " proposition3
        check "Proposition 4:\n  !a b. divides (fst (egcd a b)) b\n  " proposition4
        check "Proposition 5:\n  !a. divides 2 a <=> even a\n  " proposition5
-       check "Proposition 6:\n  !a b. let (g, s, t) <- egcd (a + 1) b in t * b + g = s * (a + 1)\n  " proposition6
+       check "Proposition 6:\n  !ap b. let a <- ap + 1 in let (g, s, t) <- egcd a b in t < a\n  " proposition6
+       check "Proposition 7:\n  !ap b. let a <- ap + 1 in let (g, s, t) <- egcd a b in s < max b 2\n  " proposition7
+       check "Proposition 8:\n  !ap b. let a <- ap + 1 in let (g, s, t) <- egcd a b in t * b + g = s * a\n  " proposition8
+       check "Proposition 9:\n  !ap bp xp yp.\n    let aq <- ap + 1 in\n    let bq <- bp + 1 in\n    let g <- fst (egcd aq bq) in\n    let a <- aq div g in\n    let b <- bq div g in\n    let x <- xp mod a in\n    let y <- yp mod b in\n    chineseRemainder a b x y < a * b\n  " proposition9
+       check "Proposition 10:\n  !ap bp xp yp.\n    let aq <- ap + 1 in\n    let bq <- bp + 1 in\n    let g <- fst (egcd aq bq) in\n    let a <- aq div g in\n    let b <- bq div g in\n    let x <- xp mod a in\n    let y <- yp mod b in\n    chineseRemainder a b x y mod a = x\n  " proposition10
+       check "Proposition 11:\n  !ap bp xp yp.\n    let aq <- ap + 1 in\n    let bq <- bp + 1 in\n    let g <- fst (egcd aq bq) in\n    let a <- aq div g in\n    let b <- bq div g in\n    let x <- xp mod a in\n    let y <- yp mod b in\n    chineseRemainder a b x y mod b = y\n  " proposition11
        return ()