diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,9 @@
 # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package
 
+## 0.2.2 *September 29th 2016*
+* New features:
+  * Derive smaller constraints from larger constraints when they differ by a single variable, i.e. `KnownNat (a + b), KnownNat b` implies `KnownNat a`.
+
 ## 0.2.1 *August 19th 2016*
 * Fixes bugs:
   * Source location of derived wanted constraints is, erroneously, always set to line 1, column 1
diff --git a/ghc-typelits-knownnat.cabal b/ghc-typelits-knownnat.cabal
--- a/ghc-typelits-knownnat.cabal
+++ b/ghc-typelits-knownnat.cabal
@@ -1,5 +1,5 @@
 name:                ghc-typelits-knownnat
-version:             0.2.1
+version:             0.2.2
 synopsis:            Derive KnownNat constraints from other KnownNat constraints
 description:
   A type checker plugin for GHC that can derive \"complex\" @KnownNat@
diff --git a/src/GHC/TypeLits/KnownNat/Solver.hs b/src/GHC/TypeLits/KnownNat/Solver.hs
--- a/src/GHC/TypeLits/KnownNat/Solver.hs
+++ b/src/GHC/TypeLits/KnownNat/Solver.hs
@@ -374,15 +374,17 @@
           exploded = map (normaliseNat . subWant &&& id) knowns
           -- interesting cases for us are those where
           -- wanted and given only differ by a constant
-          examineDiff (S [P [I n]]) entire  = Just (entire,n)
+          examineDiff (S [P [I n]]) entire = Just (entire,I n)
+          examineDiff (S [P [V v]]) entire = Just (entire,V v)
           examineDiff _ _ = Nothing
           interesting = mapMaybe (uncurry examineDiff) exploded
       -- convert the first suitable evidence
       ((h,corr):_) <- pure interesting
       let x = case corr of
-                0 -> h
-                _ | corr < 0  -> mkTyConApp typeNatAddTyCon [h,mkNumLitTy (negate corr)]
-                  | otherwise -> mkTyConApp typeNatSubTyCon [h,mkNumLitTy corr]
+                I 0 -> h
+                I i | i < 0     -> mkTyConApp typeNatAddTyCon [h,mkNumLitTy (negate i)]
+                    | otherwise -> mkTyConApp typeNatSubTyCon [h,mkNumLitTy i]
+                _ -> mkTyConApp typeNatSubTyCon [h,reifySOP (S [P [corr]])]
       MaybeT (go x)
 
 {- |
diff --git a/tests/Main.hs b/tests/Main.hs
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -97,6 +97,9 @@
 test20 :: forall a . (KnownNat (3 * a - a)) => Proxy a -> Integer
 test20 _ = natVal (Proxy @ (2 * a))
 
+test21 :: forall m n . (KnownNat (m+n), KnownNat m) => Proxy (m+n) -> Proxy m -> Integer
+test21 _ _ = natVal (Proxy :: Proxy n)
+
 tests :: TestTree
 tests = testGroup "ghc-typelits-natnormalise"
   [ testGroup "Basic functionality"
@@ -162,6 +165,9 @@
     , testCase "KnownNat (3 * a - a) => KnownNat (2 * a); @ a ~ 4" $
       show (test20 (Proxy @ 4)) @?=
       "8"
+    , testCase "KnownNat (a + b), KnownNat b => KnownNat a; @ (a+b) ~ 8, b ~ 6" $
+      show (test21 (Proxy @ 8) (Proxy @ 6)) @?=
+      "2"
     ],
     testGroup "Normalisation"
     [ testCase "KnownNat (m-n+n) ~ KnownNat m" $