diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,11 @@
 # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
 
+## 0.4.2 *July 8th 2016*
+* Find more unifications:
+  * `(2*e ^ d) ~ (2*e*a*c) ==> [a*c := 2*e ^ (d-1)]`
+  * `a^d * a^e ~ a^c ==> [c := d + e]`
+  * `x+5 ~ y ==> [x := y - 5]`, but only when `x+5 ~ y` is a given constraint
+
 ## 0.4.1 *February 4th 2016*
 * Find more unifications:
   * `F x y k z ~ F x y (k-1+1) z` ==> [k := k], where `F` can be any type function
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.4.1
+version:             0.4.2
 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
@@ -272,18 +272,30 @@
 zeroP (P ((I 0):_)) = True
 zeroP _             = False
 
+mkNonEmpty :: SOP v c -> SOP v c
+mkNonEmpty (S []) = S [P [(I 0)]]
+mkNonEmpty s      = s
+
 -- | Simplifies SOP terms using
 --
 -- * 'mergeS'
 -- * 'mergeP'
 -- * 'reduceExp'
 simplifySOP :: (Ord v, Ord c) => SOP v c -> SOP v c
-simplifySOP
-  = S
-  . sort . filter (not . zeroP)
-  . mergeWith mergeP
-  . map (P . sort . map reduceExp . mergeWith mergeS . unP)
-  . unS
+simplifySOP = repeatF go
+  where
+    go = mkNonEmpty
+       . S
+       . sort . filter (not . zeroP)
+       . mergeWith mergeP
+       . map (P . sort . map reduceExp . mergeWith mergeS . unP)
+       . unS
+
+    repeatF f x =
+      let x' = f x
+      in  if x' == x
+             then x
+             else repeatF f x'
 {-# INLINEABLE simplifySOP #-}
 
 -- | Merge two SOP terms by additions
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
@@ -6,6 +6,7 @@
 
 {-# LANGUAGE CPP             #-}
 {-# LANGUAGE RecordWildCards #-}
+
 {-# OPTIONS_GHC -fno-warn-unused-imports #-}
 
 module GHC.TypeLits.Normalise.Unify
@@ -30,7 +31,7 @@
 
 -- External
 import Data.Function (on)
-import Data.List     ((\\), intersect)
+import Data.List     ((\\), intersect, mapAccumL)
 
 -- GHC API
 import Outputable    (Outputable (..), (<+>), ($$), text)
@@ -85,7 +86,7 @@
 reifySOP = combineP . map negateP . unS
   where
     negateP :: CoreProduct -> Either CoreProduct CoreProduct
-    negateP (P ((I i):ps)) | i < 0 = Left  (P ps)
+    negateP (P ((I i):ps)) | i < 0 = Left  (P ((I (abs i)):ps))
     negateP ps                     = Right ps
 
     combineP :: [Either CoreProduct CoreProduct] -> Type
@@ -263,6 +264,19 @@
 unifiers' ct (S [P [E s1 p1]]) (S [P [E s2 p2]])
   | s1 == s2 = unifiers' ct (S [p1]) (S [p2])
 
+-- (2*e ^ d) ~ (2*e*a*c) ==> [a*c := 2*e ^ (d-1)]
+unifiers' ct (S [P [E (S [P s1]) p1]]) (S [P p2])
+  | all (`elem` p2) s1
+  = let base = intersect s1 p2
+        diff = p2 \\ s1
+    in  unifiers ct (S [P diff]) (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]])
+
+unifiers' ct (S [P p2]) (S [P [E (S [P s1]) p1]])
+  | all (`elem` p2) s1
+  = let base = intersect s1 p2
+        diff = p2 \\ s1
+    in  unifiers ct (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]]) (S [P diff])
+
 -- (i ^ a) ~ j ==> [a := round (logBase i j)], when `i` and `j` are integers,
 -- and `ceiling (logBase i j) == floor (logBase i j)`
 unifiers' ct (S [P [E (S [P [I i]]) p]]) (S [P [I j]])
@@ -283,6 +297,17 @@
     kC = ceiling k :: Integer
     kF = floor k :: Integer
 
+-- a^d * a^e ~ a^c ==> [c := d + e]
+unifiers' ct (S [P [E s1 p1]]) (S [p2]) = case collectBases p2 of
+  Just (b:bs,ps) | all (== s1) (b:bs) ->
+    unifiers' ct (S [p1]) (S ps)
+  _ -> []
+
+unifiers' ct (S [p2]) (S [P [E s1 p1]]) = case collectBases p2 of
+  Just (b:bs,ps) | all (== s1) (b:bs) ->
+    unifiers' ct (S ps) (S [p1])
+  _ -> []
+
 -- (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]]) =
@@ -318,7 +343,7 @@
 
 -- (a + c) ~ (b + c) ==> [a := b]
 unifiers' ct (S ps1)       (S ps2)
-    | null psx  = []
+    | null psx  = unifiers'' ct (S ps1) (S ps2)
     | otherwise = unifiers' ct (S ps1'') (S ps2'')
   where
     ps1'  = ps1 \\ psx
@@ -328,6 +353,19 @@
     ps2'' | null ps2' = [P [I 0]]
           | otherwise = ps2'
     psx = intersect ps1 ps2
+
+unifiers'' :: Ct -> CoreSOP -> CoreSOP -> CoreUnify Ct
+unifiers'' ct (S [P [I i],P [V v]]) s2
+  | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s2 (S [P [I (negate i)]])) ct]
+unifiers'' ct s1 (S [P [I i],P [V v]])
+  | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s1 (S [P [I (negate i)]])) ct]
+unifiers'' _ _ _ = []
+
+collectBases :: CoreProduct -> Maybe ([CoreSOP],[CoreProduct])
+collectBases = fmap unzip . traverse go . unP
+  where
+    go (E s1 p1) = Just (s1,p1)
+    go _         = Nothing
 
 -- | Find the 'TyVar' in a 'CoreSOP'
 fvSOP :: CoreSOP -> UniqSet TyVar