diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,8 @@
 # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
 
+## 0.5.7 *November 7th 2017*
+* Solve inequalities such as: `1 <= a + 3`
+
 ## 0.5.6 *October 31st 2017*
 * Fixes bugs:
   * `(x + 1) ~ (2 * y)` no longer implies `((2 * (y - 1)) + 1) ~ x`
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.5.6
+version:             0.5.7
 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/Unify.hs b/src/GHC/TypeLits/Normalise/Unify.hs
--- a/src/GHC/TypeLits/Normalise/Unify.hs
+++ b/src/GHC/TypeLits/Normalise/Unify.hs
@@ -469,4 +469,15 @@
 --
 -- > (1 <=? a^b) ~ True
 isNatural (S [P [I (-1)],P [E s p]]) = (&&) <$> isNatural s <*> isNatural (S [p])
-isNatural _ = Nothing
+-- We give up for all other products for now
+isNatural (S [P _]) = Nothing
+-- Adding two natural numbers is also a natural number
+isNatural (S (p:ps)) = do
+  pN <- isNatural (S [p])
+  pK <- isNatural (S ps)
+  case (pN,pK) of
+    (True,True)   -> return True  -- both are natural
+    (False,False) -> return False -- both are non-natural
+    _             -> Nothing
+    -- if one is natural and the other isn't, then their sum *might* be natural,
+    -- but we simply cant be sure.
diff --git a/tests/Tests.hs b/tests/Tests.hs
--- a/tests/Tests.hs
+++ b/tests/Tests.hs
@@ -3,7 +3,9 @@
 {-# LANGUAGE KindSignatures      #-}
 {-# LANGUAGE TypeOperators       #-}
 {-# LANGUAGE NoImplicitPrelude   #-}
+{-# LANGUAGE Rank2Types          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
 
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
 
@@ -233,6 +235,16 @@
 at :: SNat m -> Vec (m + (n + 1)) a -> a
 at n xs = head $ snd $ splitAt n xs
 
+leToPlus
+  :: forall (k :: Nat) (n :: Nat) f r
+   . (k <= n)
+  => 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
+
 proxyInEq1 :: Proxy a -> Proxy (a+1) -> ()
 proxyInEq1 = proxyInEq
 
@@ -248,6 +260,9 @@
 proxyInEq5 :: Proxy 1 -> Proxy (2^a) -> ()
 proxyInEq5 = proxyInEq
 
+proxyInEq6 :: Proxy 1 -> Proxy (a + 3) -> ()
+proxyInEq6 = proxyInEq
+
 proxyEq1 :: Proxy ((2 ^ x) * (2 ^ (x + x))) -> Proxy (2 * (2 ^ ((x + (x + x)) - 1)))
 proxyEq1 = id
 
@@ -344,6 +359,9 @@
     , testCase "`(2 <= (2 ^ (n + d)))` implies `(2 <= (2 ^ (d + n)))`" $
       show (proxyInEqImplication (Proxy :: Proxy 3) (Proxy :: Proxy 4)) @?=
       "Proxy"
+    , testCase "1 <= a+3" $
+      show (proxyInEq6 (Proxy :: Proxy 1) (Proxy :: Proxy 8)) @?=
+      "()"
     ]
   , testGroup "errors"
     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors