diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,15 @@
 # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
 
+## 0.6.1 *May 9th 2018*
+* Stop solving `x + y ~ a + b` by asking GHC to solve `x ~ a` and `y ~ b` as
+  this leads to a situation where we find a solution that is not the most
+  general.
+* Stop using the smallest solution to an inequality to solve an equality, as
+  this leads to finding solutions that are not the most general.
+* Solve smaller inequalities from larger inequalities, e.g.
+  * `1 <= 2*x` implies `1 <= x`
+  * `x + 2 <= y` implies `x <= y` and `2 <= y`
+
 ## 0.6 *April 23rd 2018*
 * Solving constraints with `a-b` will emit `b <= a` constraints. e.g. solving
   `n-1+1 ~ n` will emit a `1 <= n` constraint.
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.6
+version:             0.6.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
@@ -67,7 +67,7 @@
                        GHC.TypeLits.Normalise.Unify
   build-depends:       base                >=4.9   && <5,
                        ghc                 >=8.0.1 && <8.6,
-                       ghc-tcplugins-extra >=0.2.5,
+                       ghc-tcplugins-extra >=0.3,
                        integer-gmp         >=1.0   && <1.1,
                        transformers        >=0.5.2.0 && < 0.6
   hs-source-dirs:      src
diff --git a/src/GHC/TypeLits/Normalise.hs b/src/GHC/TypeLits/Normalise.hs
--- a/src/GHC/TypeLits/Normalise.hs
+++ b/src/GHC/TypeLits/Normalise.hs
@@ -186,7 +186,7 @@
 import Coercion   (CoercionHole, Role (..), mkForAllCos, mkHoleCo, mkInstCo,
                    mkNomReflCo, mkUnivCo)
 import TcPluginM  (newCoercionHole, newFlexiTyVar)
-import TcRnTypes  (CtEvidence (..), CtLoc, TcEvDest (..), ctLoc)
+import TcRnTypes  (CtEvidence (..), CtLoc, TcEvDest (..), ctLoc, isGiven)
 #if MIN_VERSION_ghc(8,2,0)
 import TcRnTypes  (ShadowInfo (WDeriv))
 #endif
@@ -266,14 +266,6 @@
   ppr (Simplified evs) = text "Simplified" $$ ppr evs
   ppr (Impossible eq)  = text "Impossible" <+> ppr eq
 
-mergeSimplifyResult
-  :: SimplifyResult
-  -> SimplifyResult
-  -> SimplifyResult
-mergeSimplifyResult a@(Impossible _) _ = a
-mergeSimplifyResult _ b@(Impossible _) = b
-mergeSimplifyResult (Simplified a) (Simplified b) = Simplified (a ++ b)
-
 simplifyNats
   :: Bool
   -- ^ Allow negated numbers (potentially unsound!)
@@ -284,7 +276,7 @@
   -> TcPluginM SimplifyResult
 simplifyNats negNumbers eqsG eqsW =
     let eqs = map (second (const [])) eqsG ++ eqsW
-    in  tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs
+    in  tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] [] eqs
   where
     -- If we allow negated numbers we simply do not emit the inequalities
     -- derived from the subtractions that are converted to additions with a
@@ -294,41 +286,47 @@
 
     simples :: [CoreUnify]
             -> [((EvTerm, Ct), [Ct])]
+            -> [(CoreSOP,CoreSOP,Bool)]
             -> [(Either NatEquality NatInEquality,[(Type,Type)])]
             -> [(Either NatEquality NatInEquality,[(Type,Type)])]
             -> TcPluginM SimplifyResult
-    simples _subst evs _xs [] = return (Simplified evs)
-    simples subst evs xs (eq@(Left (ct,u,v),k):eqs') = do
-      ur <- unifyNats ct (substsSOP subst u) (substsSOP subst v)
+    simples _subst evs _leqsG _xs [] = return (Simplified evs)
+    simples subst evs leqsG xs (eq@(Left (ct,u,v),k):eqs') = do
+      let u' = substsSOP subst u
+          v' = substsSOP subst v
+      ur <- unifyNats ct u' v'
       tcPluginTrace "unifyNats result" (ppr ur)
       case ur of
         Win -> do
           evs' <- maybe evs (:evs) <$> evMagic ct (subToPred k)
-          simples subst evs' [] (xs ++ eqs')
+          simples subst evs' leqsG [] (xs ++ eqs')
         Lose -> return (Impossible (fst eq))
-        Draw [] -> simples subst evs (eq:xs) eqs'
+        Draw [] -> simples subst evs [] (eq:xs) eqs'
         Draw subst' -> do
           evM <- evMagic ct (map unifyItemToPredType subst' ++
                              subToPred k)
+          let leqsG' | isGiven (ctEvidence ct) = eqToLeq u' v' ++ leqsG
+                     | otherwise  = leqsG
           case evM of
-            Nothing -> simples subst evs xs eqs'
+            Nothing -> simples subst evs leqsG' xs eqs'
             Just ev ->
               simples (substsSubst subst' subst ++ subst')
-                      (ev:evs) [] (xs ++ eqs')
-    simples subst evs xs (eq@(Right (ct,u),k):eqs') = do
+                      (ev:evs) leqsG' [] (xs ++ eqs')
+    simples subst evs leqsG xs (eq@(Right (ct,u@(x,y,b)),k):eqs') = do
       let u'    = substsSOP subst (subtractIneq u)
-          ineqs = map snd (rights (map fst eqsG))
-      tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u'))
+          x'    = substsSOP subst x
+          y'    = substsSOP subst y
+          leqsG' | isGiven (ctEvidence ct) = (x',y',b):leqsG
+                 | otherwise               = leqsG
+          ineqs = concat [ leqsG
+                         , map (substLeq subst) leqsG
+                         , map snd (rights (map fst eqsG))
+                         ]
+      tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs))
       case isNatural u' of
         Just True  -> do
           evs' <- maybe evs (:evs) <$> evMagic ct (subToPred k)
-          case ineqToSubst u of
-            Just s
-              | u `elem` ineqs
-              -> mergeSimplifyResult
-                  <$> simples (substsSubst [s] subst ++ [s]) evs' [] (xs ++ eqs')
-                  <*> simples subst evs' xs eqs'
-            _ -> simples subst evs' xs eqs'
+          simples subst evs' leqsG' xs eqs'
 
         Just False -> return (Impossible (fst eq))
         Nothing
@@ -338,15 +336,12 @@
           | or (mapMaybe (solveIneq 5 u) ineqs)
           -> do
             evs' <- maybe evs (:evs) <$> evMagic ct (subToPred k)
-            case ineqToSubst u of
-              Just s
-                | u `elem` ineqs
-                -> mergeSimplifyResult
-                    <$> simples (substsSubst [s] subst ++ [s]) evs' [] (xs ++ eqs')
-                    <*> simples subst evs' xs eqs'
-              _ -> simples subst evs' xs eqs'
+            simples subst evs' leqsG' xs eqs'
           | otherwise
-          -> simples subst evs (eq:xs) eqs'
+          -> simples subst evs leqsG (eq:xs) eqs'
+
+    eqToLeq x y = [(x,y,True),(y,x,True)]
+    substLeq s (x,y,b) = (substsSOP s x, substsSOP s y, b)
 
 -- Extract the Nat equality constraints
 toNatEquality :: Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)])
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
@@ -458,9 +458,16 @@
     , fromMaybe True (isNatural s2')
     -> unifiers' ct s1' s2'
   _ | null psx
-    -> case concat (zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2) of
-        [] -> unifiers'' ct (S ps1) (S ps2)
-        ks -> nub ks
+    , length ps1 == length ps2
+    -> case nub (concat (zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2)) of
+        []  -> unifiers'' ct (S ps1) (S ps2)
+        [k] | length ps1 == length ps2 -> [k]
+        _   -> []
+    | null psx
+    , isGiven (ctEvidence ct)
+    -> unifiers'' ct (S ps1) (S ps2)
+    | null psx
+    -> []
   _ -> unifiers' ct (S ps1'') (S ps2'')
   where
     k1 = subtractIneq (s1,s2,True)
@@ -585,11 +592,11 @@
   = Just (or solved)
   where
     solved = mapMaybe (uncurry (solveIneq (k - 1))) new
-    new    = mapMaybe (\f -> f want have) ineqRules
+    new    = concatMap (\f -> f want have) ineqRules
 solveIneq _ _ _ = Just False
 
 type Ineq = (CoreSOP, CoreSOP, Bool)
-type IneqRule = Ineq -> Ineq  -> Maybe (Ineq,Ineq)
+type IneqRule = Ineq -> Ineq  -> [(Ineq,Ineq)]
 
 ineqRules
   :: [IneqRule]
@@ -599,6 +606,7 @@
   , timesMonotone
   , powMonotone
   , pow2MonotoneSpecial
+  , haveSmaller
   ]
 
 -- | Transitivity of inequality
@@ -612,7 +620,7 @@
   | S [P [I a']] <- a
   , S [P [I x']] <- x
   , x' >= a'
-  = Just (want,(a,y,le))
+  = [(want,(a,y,le))]
   -- want: y <=? 10 ~ True
   -- have: y <=? 9 ~ True
   --
@@ -621,8 +629,8 @@
   | S [P [I b']] <- b
   , S [P [I y']] <- y
   , y' < b'
-  = Just (want,(x,b,le))
-leTrans _ _ = Nothing
+  = [(want,(x,b,le))]
+leTrans _ _ = []
 
 -- | Monotonicity of addition
 --
@@ -636,12 +644,23 @@
 plusMonotone want have
   | Just want' <- sopToIneq (subtractIneq want)
   , want' /= want
-  = Just (want',have)
+  = [(want',have)]
   | Just have' <- sopToIneq (subtractIneq have)
   , have' /= have
-  = Just (want,have')
-plusMonotone _ _ = Nothing
+  = [(want,have')]
+plusMonotone _ _ = []
 
+-- | Make the `a` of a given `a <= b` smaller
+haveSmaller :: IneqRule
+haveSmaller want have
+  | (S (x:y:ys),us,True) <- have
+  = [(want,(S (x:ys),us,True))
+    ,(want,(S (y:ys),us,True))
+    ]
+  | (S [P [I 1]], S [P (I _:p@(_:_))],True) <- have
+  = [(want,(S [P [I 1]],S [P p],True))]
+haveSmaller _ _ = []
+
 -- | Monotonicity of multiplication
 timesMonotone :: IneqRule
 timesMonotone want@(a,b,le) have@(x,y,_)
@@ -660,7 +679,7 @@
   , not (null ay)
   -- Pick the smallest product
   , let az = if length ax <= length ay then S [P ax] else S [P ay]
-  = Just (want,(mergeSOPMul az x, mergeSOPMul az y,le))
+  = [(want,(mergeSOPMul az x, mergeSOPMul az y,le))]
 
   -- want: a <=? C*b ~ True
   -- have: x <=? y ~ True
@@ -677,7 +696,7 @@
   , not (null by)
   -- Pick the smallest product
   , let bz = if length bx <= length by then S [P bx] else S [P by]
-  = Just (want,(mergeSOPMul bz x, mergeSOPMul bz y,le))
+  = [(want,(mergeSOPMul bz x, mergeSOPMul bz y,le))]
 
   -- want: a <=? b ~ True
   -- have: C*x <=? y ~ True
@@ -694,7 +713,7 @@
   , not (null xb)
   -- Pick the smallest product
   , let xz = if length xa <= length xb then S [P xa] else S [P xb]
-  = Just ((mergeSOPMul xz a, mergeSOPMul xz b,le),have)
+  = [((mergeSOPMul xz a, mergeSOPMul xz b,le),have)]
 
   -- want: a <=? b ~ True
   -- have: x <=? C*y ~ True
@@ -711,9 +730,9 @@
   , not (null yb)
   -- Pick the smallest product
   , let yz = if length ya <= length yb then S [P ya] else S [P yb]
-  = Just ((mergeSOPMul yz a, mergeSOPMul yz b,le),have)
+  = [((mergeSOPMul yz a, mergeSOPMul yz b,le),have)]
 
-timesMonotone _ _ = Nothing
+timesMonotone _ _ = []
 
 -- | Monotonicity of exponentiation
 powMonotone :: IneqRule
@@ -726,22 +745,22 @@
         -- new want: want
         -- new have: x <=? y ~ True
         | xS == yS
-        -> Just (want,(S [xP],S [yP],le))
+        -> [(want,(S [xP],S [yP],le))]
         -- want: XXX
         -- have: x^2 <=? y^2 ~ True
         --
         -- new want: want
         -- new have: x <=? y ~ True
         | xP == yP
-        -> Just (want,(xS,yS,le))
+        -> [(want,(xS,yS,le))]
         -- want: XXX
         -- have: 2 <=? 2 ^ x ~ True
         --
         -- new want: want
         -- new have: 1 <=? x ~ True
       _ | x == yS
-        -> Just (want,(S [P [I 1]],S [yP],le))
-      _ -> Nothing
+        -> [(want,(S [P [I 1]],S [yP],le))]
+      _ -> []
 
 powMonotone (a,S [P [E bS bP]],le) have
   = case a of
@@ -752,24 +771,24 @@
         -- new want: x <=? y ~ True
         -- new have: have
         | aS == bS
-        -> Just ((S [aP],S [bP],le),have)
+        -> [((S [aP],S [bP],le),have)]
         -- want: x^2 <=? y^2 ~ True
         -- have: XXX
         --
         -- new want: x <=? y ~ True
         -- new have: have
         | aP == bP
-        -> Just ((aS,bS,le),have)
+        -> [((aS,bS,le),have)]
         -- want: 2 <=? 2 ^ x ~ True
         -- have: XXX
         --
         -- new want: 1 <=? x ~ True
         -- new have: XXX
       _ | a == bS
-        -> Just ((S [P [I 1]],S [bP],le),have)
-      _ -> Nothing
+        -> [((S [P [I 1]],S [bP],le),have)]
+      _ -> []
 
-powMonotone _ _ = Nothing
+powMonotone _ _ = []
 
 -- | Try to get the power-of-2 factors, and apply the monotonicity of
 -- exponentiation rule.
@@ -787,7 +806,7 @@
   -- new have: have
   | Just a' <- facSOP 2 a
   , Just b' <- facSOP 2 b
-  = Just ((a',b',le),have)
+  = [((a',b',le),have)]
 pow2MonotoneSpecial want (x,y,le)
   -- want: XXX
   -- have:4 * 4^x <=? 8^x ~ True
@@ -798,8 +817,8 @@
   -- new have: 2+2*x <=? 3*x ~ True
   | Just x' <- facSOP 2 x
   , Just y' <- facSOP 2 y
-  = Just (want,(x',y',le))
-pow2MonotoneSpecial _ _ = Nothing
+  = [(want,(x',y',le))]
+pow2MonotoneSpecial _ _ = []
 
 -- | Get the power of /N/ factors of a SOP term
 facSOP
diff --git a/tests/Tests.hs b/tests/Tests.hs
--- a/tests/Tests.hs
+++ b/tests/Tests.hs
@@ -99,6 +99,13 @@
 head :: Vec (n + 1) a -> a
 head (x :> _) = x
 
+head'
+  :: forall n a
+   . (1 <= n)
+  => Vec n a
+  -> a
+head' = head @(n-1)
+
 -- | Extract the elements after the head of a vector
 --
 -- >>> tail (1:>2:>3:>Nil)
@@ -106,6 +113,9 @@
 tail :: Vec (n + 1) a -> Vec n a
 tail (_ :> xs) = xs
 
+tail' :: (1 <= m) => Vec m a -> Vec (m-1) a
+tail' = tail
+
 -- | Extract all the elements of a vector except the last element
 --
 -- >>> init (1:>2:>3:>Nil)
@@ -114,6 +124,9 @@
 init (_ :> Nil)      = Nil
 init (x :> y :> ys) = x :> init (y :> ys)
 
+init' :: (1 <= m) => Vec m a -> Vec (m-1) a
+init' = init
+
 infixr 5 ++
 -- | Append two vectors
 --
@@ -223,6 +236,9 @@
 drop :: SNat m -> Vec (m + n) a -> Vec n a
 drop n = snd . splitAt n
 
+drop' :: (m <= k) => SNat m -> Vec k a -> Vec (k - m) a
+drop' = drop
+
 -- | 'at' @n xs@ returns @n@'th element of @xs@
 --
 -- __NB__: vector elements have an __ASCENDING__ subscript starting from 0 and
@@ -235,16 +251,39 @@
 at :: SNat m -> Vec (m + (n + 1)) a -> a
 at n xs = head $ snd $ splitAt n xs
 
+at'
+  :: forall k m a
+   . (1 <= k, m <= (k-1))
+   => SNat m
+   -> Vec k a
+   -> a
+at' = at @m @(k - 1 - m)
+
 leToPlus
   :: forall (k :: Nat) (n :: Nat) f r
    . (k <= n)
-  => f n
+  => Proxy k
+  -> f n
   -- ^ Argument with the @(k <= n)@ constraint
   -> (forall m . f (m + k) -> r)
   -- ^ Function with the @(n + k)@ constraint
   -> r
-leToPlus a f = f @ (n-k) a
+leToPlus _ a f = f @ (n-k) a
 
+data BNat :: Nat -> * where
+  BT :: BNat 0
+  B0 :: BNat n -> BNat (2*n)
+  B1 :: BNat n -> BNat ((2*n) + 1)
+
+instance KnownNat n => Show (BNat n) where
+  show x = 'b':show (natVal x)
+
+predBNat :: (1 <= n) => BNat n -> BNat (n-1)
+predBNat (B1 a) = case a of
+  BT -> BT
+  a' -> B0 a'
+predBNat (B0 x)  = B1 (predBNat x)
+
 proxyInEq1 :: Proxy a -> Proxy (a+1) -> ()
 proxyInEq1 = proxyInEq
 
@@ -307,6 +346,16 @@
   -> Proxy n1
 proxyEqSubst _ _ _ _ _ = id
 
+proxyInEqImplication2
+  :: forall n n1 n2
+   . (n1 ~ (n2 + 1), (2^n) ~ (n1 + 1))
+  => Proxy n1
+  -> Proxy n2
+  -> Proxy n
+  -> Proxy ((n - 1) + 1)
+  -> Proxy n
+proxyInEqImplication2 _ _ _ x = x
+
 main :: IO ()
 main = defaultMain tests
 
@@ -383,6 +432,12 @@
     , testCase "1 <= a+3" $
       show (proxyInEq6 (Proxy :: Proxy 1) (Proxy :: Proxy 8)) @?=
       "()"
+    , testCase "`1 <= 2*x` implies `1 <= x`" $
+      show (predBNat (B1 (B1 BT))) @?=
+      "b2"
+    , testCase "`x + 2 <= y` implies `x <= y` and `2 <= y`" $
+      show (proxyInEqImplication2 (Proxy :: Proxy 3) (Proxy :: Proxy 2) (Proxy :: Proxy 2) Proxy) @?=
+      "Proxy"
     ]
   , testGroup "errors"
     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors