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.5 *August 17th 2016*
+* Solve simple inequalities, i.e.:
+  * `a  <= a + 1`
+  * `2a <= 3a`
+  * `1  <= a^b`
+
 ## 0.4.6 *July 21th 2016*
 * Reduce "x^(-y) * x^y" to 1
 * Fixes bugs:
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
 # ghc-typelits-natnormalise
 
-[![Build Status](https://secure.travis-ci.org/clash-lang/ghc-typelits-natnormalise.png?branch=master)](http://travis-ci.org/clash-lang/ghc-typelits-natnormalise)
+[![Build Status](https://secure.travis-ci.org/clash-lang/ghc-typelits-natnormalise.svg?branch=master)](http://travis-ci.org/clash-lang/ghc-typelits-natnormalise)
 [![Hackage](https://img.shields.io/hackage/v/ghc-typelits-natnormalise.svg)](https://hackage.haskell.org/package/ghc-typelits-natnormalise)
 [![Hackage Dependencies](https://img.shields.io/hackage-deps/v/ghc-typelits-natnormalise.svg?style=flat)](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-natnormalise)
 
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.6
+version:             0.5
 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
@@ -62,11 +62,10 @@
   exposed-modules:     GHC.TypeLits.Normalise,
                        GHC.TypeLits.Normalise.SOP,
                        GHC.TypeLits.Normalise.Unify
-  Other-Modules:       GHC.Extra.Instances
-  build-depends:       base >=4.8  && <5,
-                       ghc  >=7.10 && <8.2,
-                       ghc-tcplugins-extra >= 0.2,
-                       integer-gmp >= 1.0 && < 1.1
+  build-depends:       base                >=4.9   && <5,
+                       ghc                 >=8.0.1 && <8.2,
+                       ghc-tcplugins-extra >=0.2,
+                       integer-gmp         >=1.0   && <1.1
   hs-source-dirs:      src
   default-language:    Haskell2010
   other-extensions:    CPP
diff --git a/src/GHC/Extra/Instances.hs b/src/GHC/Extra/Instances.hs
deleted file mode 100644
--- a/src/GHC/Extra/Instances.hs
+++ /dev/null
@@ -1,27 +0,0 @@
-{-|
-Copyright  :  (C) 2015-2016, University of Twente
-License    :  BSD2 (see the file LICENSE)
-Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
-
-* 'Eq' instance for 'Ct'
-
-* 'Ord' instance for 'Type' and 'Ct'
--}
-
-{-# LANGUAGE CPP #-}
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-
-module GHC.Extra.Instances where
-
-import Type (Type,cmpType)
-#if __GLASGOW_HASKELL__ >= 711
-import Type (eqType)
-#endif
-
-#if __GLASGOW_HASKELL__ >= 711
-instance Eq Type where
-  (==) = eqType
-#endif
-
-instance Ord Type where
-  compare = cmpType
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
@@ -38,17 +38,12 @@
 To the header of your file.
 -}
 
-{-# LANGUAGE CPP             #-}
 {-# LANGUAGE LambdaCase      #-}
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE TupleSections   #-}
 
 {-# OPTIONS_HADDOCK show-extensions #-}
 
-#if __GLASGOW_HASKELL__ < 711
-{-# OPTIONS_GHC -fno-warn-deprecations #-}
-#endif
-
 module GHC.TypeLits.Normalise
   ( plugin )
 where
@@ -59,9 +54,6 @@
 import Data.List           (intersect)
 import Data.Maybe          (catMaybes, mapMaybe)
 import GHC.TcPluginM.Extra (tracePlugin)
-#if __GLASGOW_HASKELL__ < 711
-import GHC.TcPluginM.Extra (evByFiat)
-#endif
 
 -- GHC API
 import Outputable (Outputable (..), (<+>), ($$), text)
@@ -70,11 +62,10 @@
 import TcPluginM  (TcPluginM, tcPluginIO, tcPluginTrace, zonkCt)
 import TcRnTypes  (Ct, TcPlugin (..), TcPluginResult(..), ctEvidence, ctEvPred,
                    ctPred, isWanted, mkNonCanonical)
-import Type       (EqRel (NomEq), Kind, PredTree (EqPred), PredType, Type, TyVar,
-                   classifyPredType, getEqPredTys, mkTyVarTy)
+import Type       (EqRel (NomEq), Kind, PredTree (EqPred), PredType, TyVar,
+                   classifyPredType, eqType, getEqPredTys, mkTyVarTy)
 import TysWiredIn (typeNatKind)
 
-#if __GLASGOW_HASKELL__ >= 711
 import Coercion   (CoercionHole, Role (..), mkForAllCos, mkHoleCo, mkInstCo,
                    mkNomReflCo, mkUnivCo)
 import TcPluginM  (newCoercionHole, newFlexiTyVar)
@@ -82,21 +73,15 @@
 import TyCoRep    (UnivCoProvenance (..))
 import Type       (mkPrimEqPred)
 import TcType     (typeKind)
-#else
-import TcType              (mkEqPred, typeKind)
-import GHC.TcPluginM.Extra (newWantedWithProvenance, failWithProvenace)
-#endif
-#if __GLASGOW_HASKELL__ >= 711
-import TyCoRep       (Type (..))
-#else
-import TypeRep       (Type (..))
-#endif
-import TcTypeNats    (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,
-                      typeNatSubTyCon)
+import TyCoRep    (Type (..))
+import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,
+                   typeNatSubTyCon)
 
+import TcTypeNats (typeNatLeqTyCon)
+import Type       (mkNumLitTy,mkTyConApp)
+import TysWiredIn (promotedFalseDataCon, promotedTrueDataCon)
 
 -- internal
-import GHC.Extra.Instances () -- Ord instance for Ct
 import GHC.TypeLits.Normalise.Unify
 
 -- | To use the plugin, add
@@ -141,11 +126,7 @@
             tcPluginIO (modifyIORef discharged (++ newWanteds))
             -- return
             return (TcPluginOk solved' newWanteds)
-#if __GLASGOW_HASKELL__ >= 711
           Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])
-#else
-          Impossible eq -> failWithProvenace (fromNatEquality eq)
-#endif
 
 evItemToCt :: [Ct] -- ^ Existing wanteds
            -> (EvTerm,Ct,CoreUnify CoreNote)
@@ -160,45 +141,27 @@
            then return (Just ((ev,ct),newWanteds'))
            else return Nothing
   where
-#if __GLASGOW_HASKELL__ >= 711
     newWanteds = filter (isWanted . ctEvidence . snd . siNote) subst
-#else
-    newWanteds = filter (isWanted . ctEvidence . siNote) subst
-#endif
 
-
 substItemToCt :: [Ct] -- ^ Existing wanteds wanted
-              -> UnifyItem TyVar Type CoreNote
+              -> UnifyItem TyVar CType CoreNote
               -> TcPluginM (Maybe Ct)
 substItemToCt existingWanteds si
-  | predicate  `notElem` wantedPreds
-  , predicateS `notElem` wantedPreds
-#if __GLASGOW_HASKELL__ >= 711
+  | CType predicate  `notElem` wantedPreds
+  , CType predicateS `notElem` wantedPreds
   = return (Just (mkNonCanonical (CtWanted predicate (HoleDest ev) (ctLoc ct))))
-#else
-  = Just <$> mkNonCanonical <$> newWantedWithProvenance (ctEvidence ct) predicate
-#endif
   | otherwise
   = return Nothing
   where
-    predicate   = unifyItemToPredType si
-    (ty1,ty2)   = getEqPredTys predicate
-#if __GLASGOW_HASKELL__ >= 711
+    predicate     = unifyItemToPredType si
+    (ty1,ty2)     = getEqPredTys predicate
     predicateS    = mkPrimEqPred ty2 ty1
     ((ev,_,_),ct) = siNote si
-#else
-    predicateS  = mkEqPred ty2 ty1
-    ct          = siNote si
-#endif
-    wantedPreds = map ctPred existingWanteds
+    wantedPreds   = map (CType . ctPred) existingWanteds
 
-unifyItemToPredType :: UnifyItem TyVar Type a -> PredType
+unifyItemToPredType :: UnifyItem TyVar CType a -> PredType
 unifyItemToPredType ui =
-#if __GLASGOW_HASKELL__ >= 711
     mkPrimEqPred ty1 ty2
-#else
-    mkEqPred ty1 ty2
-#endif
   where
     ty1 = case ui of
             SubstItem {..} -> mkTyVarTy siVar
@@ -207,38 +170,38 @@
             SubstItem {..} -> reifySOP siSOP
             UnifyItem {..} -> reifySOP siRHS
 
-type NatEquality = (Ct,CoreSOP,CoreSOP)
+type NatEquality   = (Ct,CoreSOP,CoreSOP)
+type NatInEquality = (Ct,CoreSOP)
 
-fromNatEquality :: NatEquality -> Ct
-fromNatEquality (ct, _, _) = ct
+fromNatEquality :: Either NatEquality NatInEquality -> Ct
+fromNatEquality (Left  (ct, _, _)) = ct
+fromNatEquality (Right (ct, _))    = ct
 
-#if __GLASGOW_HASKELL__ >= 711
 type CoreNote = ((CoercionHole,TyVar,PredType), Ct)
-#else
-type CoreNote = Ct
-#endif
 
 data SimplifyResult
   = Simplified (CoreUnify CoreNote) [(EvTerm,Ct,CoreUnify CoreNote)]
-  | Impossible NatEquality
+  | Impossible (Either NatEquality NatInEquality)
 
 instance Outputable SimplifyResult where
   ppr (Simplified subst evs) = text "Simplified" $$ ppr subst $$ ppr evs
   ppr (Impossible eq)  = text "Impossible" <+> ppr eq
 
-simplifyNats :: [NatEquality]
+simplifyNats :: [Either NatEquality NatInEquality]
              -> TcPluginM SimplifyResult
 simplifyNats eqs =
     tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs
   where
-    simples :: CoreUnify CoreNote -> [Maybe (EvTerm, Ct, CoreUnify CoreNote)] -> [NatEquality]
-            -> [NatEquality] -> TcPluginM SimplifyResult
+    simples :: CoreUnify CoreNote
+            -> [Maybe (EvTerm, Ct, CoreUnify CoreNote)]
+            -> [Either NatEquality NatInEquality]
+            -> [Either NatEquality NatInEquality]
+            -> TcPluginM SimplifyResult
     simples subst evs _xs [] = return (Simplified subst (catMaybes evs))
-    simples subst evs xs (eq@(ct,u,v):eqs') = do
+    simples subst evs xs (eq@(Left (ct,u,v)):eqs') = do
       ur <- unifyNats ct (substsSOP subst u) (substsSOP subst v)
       tcPluginTrace "unifyNats result" (ppr ur)
       case ur of
-#if __GLASGOW_HASKELL__ >= 711
         Win         -> simples subst (((,,) <$> evMagic ct [] <*> pure ct <*> pure []):evs) []
                                (xs ++ eqs')
         Lose        -> return (Impossible eq)
@@ -253,20 +216,14 @@
           simples (substsSubst subst'' subst ++ subst'')
             (((,,) <$> evMagic ct newEvs <*> pure ct <*> pure subst''):evs)
             [] (xs ++ eqs')
-#else
-        Win         -> simples subst (((,,) <$> evMagic ct <*> pure ct <*> pure []):evs) []
-                               (xs ++ eqs')
-        Lose        -> return (Impossible eq)
-        Draw []     -> simples subst evs (eq:xs) eqs'
-        Draw subst' -> do
-          simples (substsSubst subst' subst ++ subst')
-                  (((,,) <$> evMagic ct <*> pure ct <*> pure subst'):evs)
-                  [] (xs ++ eqs')
-
-#endif
+    simples subst evs xs (eq@(Right (ct,u)):eqs') =
+      case isNatural u of
+        Just True  -> simples subst (((,,) <$> evMagic ct [] <*> pure ct <*> pure []):evs) xs eqs'
+        Just False -> return (Impossible eq)
+        Nothing    -> simples subst evs (eq:xs) eqs'
 
 -- Extract the Nat equality constraints
-toNatEquality :: Ct -> Maybe NatEquality
+toNatEquality :: Ct -> Maybe (Either NatEquality NatInEquality)
 toNatEquality ct = case classifyPredType $ ctEvPred $ ctEvidence ct of
     EqPred NomEq t1 t2
       -> go t1 t2
@@ -276,20 +233,27 @@
       | tc == tc'
       , null ([tc,tc'] `intersect` [typeNatAddTyCon,typeNatSubTyCon
                                    ,typeNatMulTyCon,typeNatExpTyCon])
-      = case filter (uncurry (/=)) (zip xs ys) of
+      = case filter (not . uncurry eqType) (zip xs ys) of
           [(x,y)] | isNatKind (typeKind x) &&  isNatKind (typeKind y)
-                  -> Just (ct, normaliseNat x, normaliseNat y)
+                  -> Just (Left (ct, normaliseNat x, normaliseNat y))
           _ -> Nothing
+      | tc == typeNatLeqTyCon
+      , [x,y] <- xs
+      = if tc' == promotedTrueDataCon
+           then Just (Right (ct,normaliseNat (mkTyConApp typeNatSubTyCon [y,x])))
+           else if tc' == promotedFalseDataCon
+                then Just (Right (ct,normaliseNat (mkTyConApp typeNatSubTyCon [x,mkTyConApp typeNatAddTyCon [y,mkNumLitTy 1]])))
+                else Nothing
+
     go x y
       | isNatKind (typeKind x) && isNatKind (typeKind y)
-      = Just (ct,normaliseNat x,normaliseNat y)
+      = Just (Left (ct,normaliseNat x,normaliseNat y))
       | otherwise
       = Nothing
 
     isNatKind :: Kind -> Bool
-    isNatKind = (== typeNatKind)
+    isNatKind = (`eqType` typeNatKind)
 
-#if __GLASGOW_HASKELL__ >= 711
 evMagic :: Ct -> [(CoercionHole, TyVar, PredType)] -> Maybe EvTerm
 evMagic ct evs = case classifyPredType $ ctEvPred $ ctEvidence ct of
   EqPred NomEq t1 t2 ->
@@ -302,9 +266,3 @@
         finalEv = foldl mkInstCo forallEv holeEvs
     in  Just (EvCoercion finalEv)
   _ -> Nothing
-#else
-evMagic :: Ct -> Maybe EvTerm
-evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of
-  EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-natnormalise" t1 t2)
-  _                  -> Nothing
-#endif
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
@@ -4,15 +4,20 @@
 Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
 -}
 
-{-# LANGUAGE CPP             #-}
-{-# LANGUAGE MagicHash       #-}
-{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE CPP                        #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MagicHash                  #-}
+{-# LANGUAGE RecordWildCards            #-}
 
 {-# OPTIONS_GHC -fno-warn-unused-imports #-}
+#if __GLASGOW_HASKELL__ < 801
+#define nonDetCmpType cmpType
+#endif
 
 module GHC.TypeLits.Normalise.Unify
   ( -- * 'Nat' expressions \<-\> 'SOP' terms
-    CoreSOP
+    CType (..)
+  , CoreSOP
   , normaliseNat
   , reifySOP
     -- * Substitution on 'SOP' terms
@@ -27,6 +32,8 @@
   , unifiers
     -- * Free variables in 'SOP' terms
   , fvSOP
+    -- * Properties
+  , isNatural
   )
 where
 
@@ -46,26 +53,31 @@
 import TcTypeNats    (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,
                       typeNatSubTyCon)
 import Type          (EqRel (NomEq), PredTree (EqPred), TyVar, classifyPredType,
-                      coreView, mkNumLitTy, mkTyConApp, mkTyVarTy)
-#if __GLASGOW_HASKELL__ >= 711
+                      coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy,
+                      nonDetCmpType)
 import TyCoRep       (Type (..), TyLit (..))
-#else
-import TypeRep       (Type (..), TyLit (..))
-#endif
 import UniqSet       (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets,
                       unitUniqSet)
 
 -- Internal
-import GHC.Extra.Instances () -- Ord instance for Type
 import GHC.TypeLits.Normalise.SOP
 
 -- Used for haddock
 import GHC.TypeLits (Nat)
 
+newtype CType = CType { unCType :: Type }
+  deriving Outputable
+
+instance Eq CType where
+  (CType ty1) == (CType ty2) = eqType ty1 ty2
+
+instance Ord CType where
+  compare (CType ty1) (CType ty2) = nonDetCmpType ty1 ty2
+
 -- | 'SOP' with 'TyVar' variables
-type CoreSOP     = SOP TyVar Type
-type CoreProduct = Product TyVar Type
-type CoreSymbol  = Symbol TyVar Type
+type CoreSOP     = SOP TyVar CType
+type CoreProduct = Product TyVar CType
+type CoreSymbol  = Symbol TyVar CType
 
 -- | Convert a type of /kind/ 'GHC.TypeLits.Nat' to an 'SOP' term, but
 -- only when the type is constructed out of:
@@ -84,7 +96,7 @@
                                                      (normaliseNat y))
   | tc == typeNatMulTyCon = mergeSOPMul (normaliseNat x) (normaliseNat y)
   | tc == typeNatExpTyCon = normaliseExp (normaliseNat x) (normaliseNat y)
-normaliseNat t = S [P [C t]]
+normaliseNat t = S [P [C (CType t)]]
 
 -- | Convert a 'SOP' term back to a type of /kind/ 'GHC.TypeLits.Nat'
 reifySOP :: CoreSOP -> Type
@@ -145,7 +157,7 @@
 
 reifySymbol :: Either CoreSymbol (CoreSOP,[CoreProduct]) -> Type
 reifySymbol (Left (I i)  )  = mkNumLitTy i
-reifySymbol (Left (C c)  )  = c
+reifySymbol (Left (C c)  )  = unCType c
 reifySymbol (Left (V v)  )  = mkTyVarTy v
 reifySymbol (Left (E s p))  = mkTyConApp typeNatExpTyCon [reifySOP s,reifyProduct p]
 reifySymbol (Right (s1,s2)) = mkTyConApp typeNatExpTyCon
@@ -156,7 +168,7 @@
 -- | A substitution is essentially a list of (variable, 'SOP') pairs,
 -- but we keep the original 'Ct' that lead to the substitution being
 -- made, for use when turning the substitution back into constraints.
-type CoreUnify a = TyUnify TyVar Type a
+type CoreUnify a = TyUnify TyVar CType a
 
 type TyUnify v c n = [UnifyItem v c n]
 
@@ -272,22 +284,22 @@
 unifiers ct u@(S [P [V x]]) v
   = case classifyPredType $ ctEvPred $ ctEvidence ct of
       EqPred NomEq t1 _
-        | reifySOP u /= t1 || isGiven (ctEvidence ct) -> [SubstItem x v ct]
+        | CType (reifySOP u) /= CType t1 || isGiven (ctEvidence ct) -> [SubstItem x v ct]
       _ -> []
 unifiers ct u v@(S [P [V x]])
   = case classifyPredType $ ctEvPred $ ctEvidence ct of
       EqPred NomEq _ t2
-        | reifySOP v /= t2 || isGiven (ctEvidence ct) -> [SubstItem x u ct]
+        | CType (reifySOP v) /= CType t2 || isGiven (ctEvidence ct) -> [SubstItem x u ct]
       _ -> []
 unifiers ct u@(S [P [C _]]) v
   = case classifyPredType $ ctEvPred $ ctEvidence ct of
       EqPred NomEq t1 t2
-        | reifySOP u /= t1 || reifySOP v /= t2 -> [UnifyItem u v ct]
+        | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2 -> [UnifyItem u v ct]
       _ -> []
 unifiers ct u v@(S [P [C _]])
   = case classifyPredType $ ctEvPred $ ctEvidence ct of
       EqPred NomEq t1 t2
-        | reifySOP u /= t1 || reifySOP v /= t2 -> [UnifyItem u v ct]
+        | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2 -> [UnifyItem u v ct]
       _ -> []
 unifiers ct u v             = unifiers' ct u v
 
@@ -438,3 +450,21 @@
          then Nothing
          else Just (smallInteger z1)
 integerLogBase _ _ = Nothing
+
+isNatural :: CoreSOP -> Maybe Bool
+isNatural (S [])           = return True
+isNatural (S [P []])       = return True
+isNatural (S [P (I i:ps)])
+  | i >= 0    = isNatural (S [P ps])
+  | otherwise = return False
+isNatural (S [P (V _:ps)]) = isNatural (S [P ps])
+-- This is a quick hack, it determines that
+--
+-- > a^b - 1
+--
+-- is a natural number as long as 'a' and 'b' are natural numbers.
+-- This used to assert that:
+--
+-- > (1 <=? a^b) ~ True
+isNatural (S [P [I (-1)],P [E s p]]) = (&&) <$> isNatural s <*> isNatural (S [p])
+isNatural _ = Nothing
diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs
--- a/tests/ErrorTests.hs
+++ b/tests/ErrorTests.hs
@@ -78,3 +78,51 @@
   ["Expected type: Proxy x -> Proxy (y + x)"
   ,"Actual type: Proxy x -> Proxy x"
   ]
+
+proxyInEq :: (a <= b) => Proxy a -> Proxy b -> ()
+proxyInEq _ _ = ()
+
+proxyInEq' :: ((a <=? b) ~ 'False) => Proxy a -> Proxy b -> ()
+proxyInEq' _ _ = ()
+
+testProxy9 :: Proxy (a + 1) -> Proxy a -> ()
+testProxy9 = proxyInEq
+
+testProxy9Errors =
+  ["Couldn't match type ‘(a + 1) <=? a’ with ‘'True’"
+  ]
+
+testProxy10 :: Proxy (a :: Nat) -> Proxy (a + 2) -> ()
+testProxy10 = proxyInEq'
+
+testProxy10Errors =
+  ["Couldn't match type ‘a <=? (a + 2)’ with ‘'False’"
+  ]
+
+testProxy11 :: Proxy (a :: Nat) -> Proxy a -> ()
+testProxy11 = proxyInEq'
+
+testProxy11Errors =
+  ["Couldn't match type ‘'True’ with ‘'False’"
+  ]
+
+testProxy12 :: Proxy (a + b) -> Proxy (a + c) -> ()
+testProxy12 = proxyInEq
+
+testProxy12Errors =
+  ["Couldn't match type ‘(a + b) <=? (a + c)’ with ‘'True’"
+  ]
+
+testProxy13 :: Proxy (4*a) -> Proxy (2*a) ->()
+testProxy13 = proxyInEq
+
+testProxy13Errors =
+  ["Couldn't match type ‘(4 * a) <=? (2 * a)’ with ‘'True’"
+  ]
+
+testProxy14 :: Proxy (2*a) -> Proxy (4*a) -> ()
+testProxy14 = proxyInEq'
+
+testProxy14Errors =
+  ["Couldn't match type ‘(2 * a) <=? (4 * a)’ with ‘'False’"
+  ]
diff --git a/tests/Tests.hs b/tests/Tests.hs
--- a/tests/Tests.hs
+++ b/tests/Tests.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE CPP                 #-}
 {-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE GADTs               #-}
 {-# LANGUAGE KindSignatures      #-}
@@ -234,6 +233,21 @@
 at :: SNat m -> Vec (m + (n + 1)) a -> a
 at n xs = head $ snd $ splitAt n xs
 
+proxyInEq1 :: Proxy a -> Proxy (a+1) -> ()
+proxyInEq1 = proxyInEq
+
+proxyInEq2 :: Proxy ((a+1) :: Nat) -> Proxy a -> ()
+proxyInEq2 = proxyInEq'
+
+proxyInEq3 :: Proxy (a :: Nat) -> Proxy (a+b) -> ()
+proxyInEq3 = proxyInEq
+
+proxyInEq4 :: Proxy (2*a) -> Proxy (4*a) -> ()
+proxyInEq4 = proxyInEq
+
+proxyInEq5 :: Proxy 1 -> Proxy (2^a) -> ()
+proxyInEq5 = proxyInEq
+
 main :: IO ()
 main = defaultMain tests
 
@@ -271,6 +285,23 @@
       show (proxyFun7 (Proxy :: Proxy 8) :: Proxy 3) @?=
       "Proxy"
     ]
+  , testGroup "Inequality"
+    [ testCase "a <= a+1" $
+      show (proxyInEq1 (Proxy :: Proxy 2) (Proxy :: Proxy 3)) @?=
+      "()"
+    , testCase "(a+1 <=? a) ~ False" $
+      show (proxyInEq2 (Proxy :: Proxy 3) (Proxy :: Proxy 2)) @?=
+      "()"
+    , testCase "a <= a+b" $
+      show (proxyInEq3 (Proxy :: Proxy 2) (Proxy :: Proxy 2)) @?=
+      "()"
+    , testCase "2a <= 4a" $
+      show (proxyInEq4 (Proxy :: Proxy 2) (Proxy :: Proxy 4)) @?=
+      "()"
+    , testCase "1 <= 2^a" $
+      show (proxyInEq5 (Proxy :: Proxy 1) (Proxy :: Proxy 1)) @?=
+      "()"
+    ]
   , testGroup "errors"
     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors
     , testCase "GCD 6 8 + x ~ x + GCD 9 6" $ testProxy2 `throws` testProxy2Errors
@@ -279,6 +310,14 @@
     , testCase "Unify \"(2*x)+4\" with \"7\"" $ testProxy5 `throws` testProxy5Errors
     , testCase "Unify \"2^k\" with \"7\"" $ testProxy6 `throws` testProxy6Errors
     , testCase "x ~ y + x" $ testProxy8 `throws` testProxy8Errors
+    , testGroup "Inequality"
+      [ testCase "a+1 <= a" $ testProxy9 `throws` testProxy9Errors
+      , testCase "(a <=? a+1) ~ False" $ testProxy10 `throws` testProxy10Errors
+      , testCase "(a <=? a) ~ False" $ testProxy11 `throws` testProxy11Errors
+      , testCase "() => (a+b <= a+c)" $ testProxy12 `throws` testProxy12Errors
+      , testCase "4a <= 2a" $ testProxy13 `throws` testProxy13Errors
+      , testCase "2a <=? 4a ~ False" $ testProxy14 `throws` testProxy14Errors
+      ]
     ]
   ]
 
@@ -290,11 +329,7 @@
   result <- try (evaluate v)
   case result of
     Right _ -> assertFailure "No exception!"
-#if MIN_VERSION_base(4,9,0)
     Left (TypeError msg) ->
-#else
-    Left (ErrorCall msg) ->
-#endif
       if all (`isInfixOf` msg) xs
          then return ()
          else assertFailure msg