diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,10 @@
 # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
 
+## 0.3.1 *October 19th 2015*
+* Find more unifications:
+  * `(i * a) ~ j ==> [a := div j i]`, when `i` and `j` are integers, and `mod j i == 0`.
+  * `(i * a) + j ~ k  ==> [a := div (k-j) i]`, when `i`, `j`, and `k` are integers, and `k-j >= 0` and `mod (k-j) i == 0`.
+
 ## 0.3 *June 3rd 2015*
 * Find more unifications:
   * `<TyApp xs> + x ~ 2 + x ==> [<TyApp xs> ~ 2]`
diff --git a/ghc-typelits-natnormalise.cabal b/ghc-typelits-natnormalise.cabal
--- a/ghc-typelits-natnormalise.cabal
+++ b/ghc-typelits-natnormalise.cabal
@@ -1,5 +1,5 @@
 name:                ghc-typelits-natnormalise
-version:             0.3
+version:             0.3.1
 synopsis:            GHC typechecker plugin for types of kind GHC.TypeLits.Nat
 description:
   A type checker plugin for GHC that can solve /equalities/ of types of kind
diff --git a/src/GHC/TypeLits/Normalise/SOP.hs b/src/GHC/TypeLits/Normalise/SOP.hs
--- a/src/GHC/TypeLits/Normalise/SOP.hs
+++ b/src/GHC/TypeLits/Normalise/SOP.hs
@@ -102,7 +102,13 @@
   deriving (Eq,Ord)
 
 newtype Product v c = P { unP :: [Symbol v c] }
-  deriving (Eq,Ord)
+  deriving (Eq)
+
+instance (Ord v, Ord c) => Ord (Product v c) where
+  compare (P [x])   (P [y])   = compare x y
+  compare (P [_])   (P (_:_)) = LT
+  compare (P (_:_)) (P [_])   = GT
+  compare (P xs)    (P ys)    = compare xs ys
 
 newtype SOP v c = S { unS :: [Product v c] }
   deriving (Ord)
diff --git a/src/GHC/TypeLits/Normalise/Unify.hs b/src/GHC/TypeLits/Normalise/Unify.hs
--- a/src/GHC/TypeLits/Normalise/Unify.hs
+++ b/src/GHC/TypeLits/Normalise/Unify.hs
@@ -189,7 +189,7 @@
 -- (a + c) ~ (b + c)  ==>  \[a := b\]
 -- (2*a) ~ (2*b)      ==>  [a := b]
 -- (2 + a) ~ 5        ==>  [a := 3]
--- (3 * a) ~ 0        ==>  [a := 0]
+-- (i * a) ~ j        ==>  [a := div j i], when (mod j i == 0)
 -- @
 --
 -- However, given a wanted:
@@ -233,10 +233,18 @@
 unifiers' ct s1@(S [P [C _]]) s2               = [UnifyItem s1 s2 ct]
 unifiers' ct s1               s2@(S [P [C _]]) = [UnifyItem s1 s2 ct]
 
--- (3 * a) ~ 0 ==> [a := 0]
-unifiers' ct (S [P ((I _):ps)]) (S [P [I 0]]) = unifiers' ct (S [P ps]) (S [P [I 0]])
-unifiers' ct (S [P [I 0]]) (S [P ((I _):ps)]) = unifiers' ct (S [P ps]) (S [P [I 0]])
+-- (i * a) ~ j ==> [a := div j i]
+-- Where 'a' is a variable, 'i' and 'j' are integer literals, and j `mod` i == 0
+unifiers' ct (S [P ((I i):ps)]) (S [P [I j]]) =
+  case safeDiv j i of
+    Just k  -> unifiers' ct (S [P ps]) (S [P [I k]])
+    _       -> []
 
+unifiers' ct (S [P [I j]]) (S [P ((I i):ps)]) =
+  case safeDiv j i of
+    Just k  -> unifiers' ct (S [P ps]) (S [P [I k]])
+    _       -> []
+
 -- (2*a) ~ (2*b) ==> [a := b]
 -- unifiers' ct (S [P (p:ps1)]) (S [P (p':ps2)])
 --     | p == p'   = unifiers' ct (S [P ps1]) (S [P ps2])
@@ -289,3 +297,10 @@
 
 containsConstants :: CoreSOP -> Bool
 containsConstants = any (any (\c -> case c of {(C _) -> True; _ -> False}) . unP) . unS
+
+safeDiv :: Integer -> Integer -> Maybe Integer
+safeDiv i j
+  | j == 0    = Just 0
+  | otherwise = case divMod i j of
+                  (k,0) -> Just k
+                  _     -> Nothing
diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs
--- a/tests/ErrorTests.hs
+++ b/tests/ErrorTests.hs
@@ -26,3 +26,33 @@
   ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"
   ,"Actual type: Proxy (x + 3) -> Proxy (x + 3)"
   ]
+
+proxyFun3 :: Proxy (x + x + x) -> ()
+proxyFun3 = const ()
+
+testProxy3 :: Proxy 8 -> ()
+testProxy3 = proxyFun3
+
+testProxy3Errors =
+  ["Expected type: Proxy 8 -> ()"
+  ,"Actual type: Proxy ((x0 + x0) + x0) -> ()"
+  ]
+
+proxyFun4 :: Proxy ((2*y)+4) -> ()
+proxyFun4 = const ()
+
+testProxy4 :: Proxy 2 -> ()
+testProxy4 = proxyFun4
+
+testProxy4Errors =
+  ["Expected type: Proxy 2 -> ()"
+  ,"Actual type: Proxy ((2 * y0) + 4) -> ()"
+  ]
+
+testProxy5 :: Proxy 7 -> ()
+testProxy5 = proxyFun4
+
+testProxy5Errors =
+  ["Expected type: Proxy 7 -> ()"
+  ,"Actual type: Proxy ((2 * y1) + 4) -> ()"
+  ]
diff --git a/tests/Tests.hs b/tests/Tests.hs
--- a/tests/Tests.hs
+++ b/tests/Tests.hs
@@ -260,10 +260,19 @@
     , testCase "show (unconcat (snat :: SNat 4) (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil))" $
       show (unconcat (snat :: SNat 4) (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)) @?=
       "<<1,2,3,4>,<5,6,7,8>,<9,10,11,12>>"
+    , testCase "show (proxyFun3 (Proxy :: Proxy 9))" $
+      show (proxyFun3 (Proxy :: Proxy 9)) @?=
+      "()"
+    , testCase "show (proxyFun4 (Proxy :: Proxy 8))" $
+      show (proxyFun4 (Proxy :: Proxy 8)) @?=
+      "()"
     ]
   , testGroup "errors"
     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors
     , testCase "GCD 6 8 + x ~ x + GCD 9 6" $ testProxy2 `throws` testProxy2Errors
+    , testCase "Unify \"x + x + x\" with \"8\"" $ testProxy3 `throws` testProxy3Errors
+    , testCase "Unify \"(2*x)+4\" with \"2\"" $ testProxy4 `throws` testProxy4Errors
+    , testCase "Unify \"(2*x)+4\" with \"7\"" $ testProxy5 `throws` testProxy5Errors
     ]
   ]