diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,8 @@
 # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package
 
+# 0.4.1 *November 10 2020*
+* Reduce `n <=? Max (n + p) p` to `True`
+
 # 0.4 *March 9 2020*
 * `Max` short-circuits on zero, but is stuckness preserving. i.e. `Max (0-1) 0` reduces to `(0-1)`
 * Reduce inside arithmetic equations. e.g. `1 + a ~ Max 0 a + CLog 2 2`
diff --git a/ghc-typelits-extra.cabal b/ghc-typelits-extra.cabal
--- a/ghc-typelits-extra.cabal
+++ b/ghc-typelits-extra.cabal
@@ -1,5 +1,5 @@
 name:                ghc-typelits-extra
-version:             0.4
+version:             0.4.1
 synopsis:            Additional type-level operations on GHC.TypeLits.Nat
 description:
   Additional type-level operations on @GHC.TypeLits.Nat@:
diff --git a/src/GHC/TypeLits/Extra/Solver.hs b/src/GHC/TypeLits/Extra/Solver.hs
--- a/src/GHC/TypeLits/Extra/Solver.hs
+++ b/src/GHC/TypeLits/Extra/Solver.hs
@@ -24,10 +24,9 @@
 
 -- external
 import Control.Monad.Trans.Maybe (MaybeT (..))
-import Data.Either               (lefts)
 import Data.Maybe                (catMaybes)
-import GHC.TcPluginM.Extra       (evByFiat, lookupModule, lookupName,
-                                  tracePlugin)
+import GHC.TcPluginM.Extra       (evByFiat, lookupModule, lookupName
+                                 ,tracePlugin, newWanted)
 
 -- GHC API
 import FastString (fsLit)
@@ -38,10 +37,11 @@
 #if MIN_VERSION_ghc(8,6,0)
 import Plugins    (purePlugin)
 #endif
+import PrelNames  (eqPrimTyConKey, hasKey)
 import TcEvidence (EvTerm)
 import TcPluginM  (TcPluginM, tcLookupTyCon, tcPluginTrace)
 import TcRnTypes  (TcPlugin(..), TcPluginResult (..))
-import Type       (Kind, eqType)
+import Type       (Kind, eqType, mkTyConApp, splitTyConApp_maybe)
 import TyCoRep    (Type (..))
 import TysWiredIn (typeNatKind, promotedTrueDataCon, promotedFalseDataCon)
 import TcTypeNats (typeNatLeqTyCon)
@@ -54,11 +54,11 @@
 #endif
 
 #if MIN_VERSION_ghc(8,10,0)
-import Constraint (Ct, ctEvidence, ctEvPred, isWantedCt)
+import Constraint (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt, cc_ev)
 import Predicate  (EqRel (NomEq), Pred (EqPred), classifyPredType)
 import Type       (typeKind)
 #else
-import TcRnTypes  (Ct, ctEvidence, ctEvPred, isWantedCt)
+import TcRnTypes  (Ct, CtEvidence, ctEvidence, ctEvPred, ctLoc, isWantedCt, cc_ev)
 import TcType     (typeKind)
 import Type       (EqRel (NomEq), PredTree (EqPred), classifyPredType)
 #endif
@@ -114,100 +114,129 @@
 decideEqualSOP defs givens  _deriveds wanteds = do
   -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out
   let wanteds' = filter isWantedCt wanteds
-  unit_wanteds <- catMaybes <$> mapM (runMaybeT . toNatEquality defs) wanteds'
+  unit_wanteds <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) wanteds'
   case unit_wanteds of
     [] -> return (TcPluginOk [] [])
     _  -> do
 #if MIN_VERSION_ghc(8,4,0)
-      unit_givens <- catMaybes <$> mapM (runMaybeT . toNatEquality defs) (givens ++ flattenGivens givens)
+      unit_givens <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) (givens ++ flattenGivens givens)
 #else
-      unit_givens <- catMaybes <$> mapM ((runMaybeT . toNatEquality defs) <=< zonkCt) givens
+      unit_givens <- catMaybes <$> mapM ((runMaybeT . toSolverConstraint defs) <=< zonkCt) givens
 #endif
-      sr <- simplifyExtra (unit_givens ++ unit_wanteds)
+      sr <- simplifyExtra defs (unit_givens ++ unit_wanteds)
       tcPluginTrace "normalised" (ppr sr)
       case sr of
-        Simplified evs -> return (TcPluginOk (filter (isWantedCt . snd) evs) [])
-        Impossible eq  -> return (TcPluginContradiction [fromNatEquality eq])
+        Simplified evs new -> return (TcPluginOk (filter (isWantedCt . snd) evs) new)
+        Impossible eq  -> return (TcPluginContradiction [fromSolverConstraint eq])
 
-type NatEquality   = (Ct,ExtraOp,ExtraOp)
-type NatInEquality = (Ct,ExtraOp,ExtraOp,Bool)
+data SolverConstraint
+   = NatEquality Ct ExtraOp ExtraOp Normalised
+   | NatInequality Ct ExtraOp ExtraOp Bool Normalised
 
+instance Outputable SolverConstraint where
+  ppr (NatEquality ct op1 op2 norm) = text "NatEquality" $$ ppr ct $$ ppr op1 $$ ppr op2 $$ ppr norm
+  ppr (NatInequality _ op1 op2 b norm) = text "NatInequality" $$ ppr op1 $$ ppr op2 $$ ppr b $$ ppr norm
+
 data SimplifyResult
-  = Simplified [(EvTerm,Ct)]
-  | Impossible (Either NatEquality NatInEquality)
+  = Simplified [(EvTerm,Ct)] [Ct]
+  | Impossible SolverConstraint
 
 instance Outputable SimplifyResult where
-  ppr (Simplified evs) = text "Simplified" $$ ppr evs
-  ppr (Impossible eq)  = text "Impossible" <+> ppr eq
+  ppr (Simplified evs new) = text "Simplified" $$ text "Solved:" $$ ppr evs $$ text "New:" $$ ppr new
+  ppr (Impossible sct)  = text "Impossible" <+> ppr sct
 
-simplifyExtra :: [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
-simplifyExtra eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] eqs
+simplifyExtra :: ExtraDefs -> [SolverConstraint] -> TcPluginM SimplifyResult
+simplifyExtra defs eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] [] eqs
   where
-    simples :: [Maybe (EvTerm, Ct)] -> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
-    simples evs [] = return (Simplified (catMaybes evs))
-    simples evs (eq@(Left (ct,u,v)):eqs') = do
+    simples :: [Maybe (EvTerm, Ct)] -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult
+    simples evs news [] = return (Simplified (catMaybes evs) news)
+    simples evs news (eq@(NatEquality ct u v norm):eqs') = do
       ur <- unifyExtra ct u v
       tcPluginTrace "unifyExtra result" (ppr ur)
       case ur of
-        Win  -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'
-        Lose -> if null evs && null eqs'
-                   then return  (Impossible eq)
-                   else simples evs eqs'
-        Draw -> simples evs eqs'
-    simples evs (eq@(Right (ct,u,v,b)):eqs') = do
+        Win                          -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs'
+        Lose | null evs && null eqs' -> return (Impossible eq)
+        _ | norm == Normalised && isWantedCt ct -> do
+          newCt <- createWantedFromNormalised defs eq
+          simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs'
+        Lose -> simples evs news eqs'
+        Draw -> simples evs news eqs'
+    simples evs news (eq@(NatInequality ct u v b norm):eqs') = do
       tcPluginTrace "unifyExtra leq result" (ppr (u,v,b))
       case (u,v) of
         (I i,I j)
-          | (i <= j) == b -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'
+          | (i <= j) == b -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs'
           | otherwise     -> return  (Impossible eq)
         (p, Max x y)
-          | b && (p == x || p == y) -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'
+          | b && (p == x || p == y) -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs'
 
         -- transform:  q ~ Max x y => (p <=? q ~ True)
         -- to:         (p <=? Max x y) ~ True
         -- and try to solve that along with the rest of the eqs'
         (p, q@(V _))
           | b -> case findMax q eqs of
-                   Just m  -> simples evs ((Right (ct,p,m,b)):eqs')
-                   Nothing -> simples evs eqs'
-        _ -> simples evs eqs'
+                   Just m  -> simples evs news (NatInequality ct p m b norm:eqs')
+                   Nothing -> simples evs news eqs'
+        _ | norm == Normalised && isWantedCt ct -> do
+          newCt <- createWantedFromNormalised defs eq
+          simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs'
+        _ -> simples evs news eqs'
 
     -- look for given constraint with the form: c ~ Max x y
-    findMax :: ExtraOp -> [Either NatEquality NatInEquality] -> Maybe ExtraOp
-    findMax c = go . lefts
+    findMax :: ExtraOp -> [SolverConstraint] -> Maybe ExtraOp
+    findMax c = go
       where
         go [] = Nothing
-        go ((ct, a,b@(Max _ _)) :_)
+        go ((NatEquality ct a b@(Max _ _) _) :_)
           | c == a && not (isWantedCt ct)
             = Just b
-        go ((ct, a@(Max _ _),b) :_)
+        go ((NatEquality ct a@(Max _ _) b _) :_)
           | c == b && not (isWantedCt ct)
             = Just a
         go (_:rest) = go rest
 
 
 -- Extract the Nat equality constraints
-toNatEquality :: ExtraDefs -> Ct -> MaybeT TcPluginM (Either NatEquality NatInEquality)
-toNatEquality defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of
+toSolverConstraint :: ExtraDefs -> Ct -> MaybeT TcPluginM SolverConstraint
+toSolverConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of
     EqPred NomEq t1 t2
       | isNatKind (typeKind t1) || isNatKind (typeKind t2)
-      -> Left <$> ((ct,,) <$> normaliseNat defs t1 <*> normaliseNat defs t2)
+      -> do
+         (t1', n1) <- normaliseNat defs t1
+         (t2', n2) <- normaliseNat defs t2
+         pure (NatEquality ct t1' t2' (mergeNormalised n1 n2))
       | TyConApp tc [x,y] <- t1
       , tc == typeNatLeqTyCon
       , TyConApp tc' [] <- t2
-      -> if tc' == promotedTrueDataCon
-            then Right <$> ((ct,,,True) <$> normaliseNat defs x <*> normaliseNat defs y)
-            else if tc' == promotedFalseDataCon
-                 then Right <$> ((ct,,,False) <$> normaliseNat defs x <*> normaliseNat defs y)
-                 else fail "Nothing"
+      -> do
+          (x', n1) <- normaliseNat defs x
+          (y', n2) <- normaliseNat defs y
+          let res | tc' == promotedTrueDataCon  = pure (NatInequality ct x' y' True  (mergeNormalised n1 n2))
+                  | tc' == promotedFalseDataCon = pure (NatInequality ct x' y' False (mergeNormalised n1 n2))
+                  | otherwise                   = fail "Nothing"
+          res
     _ -> fail "Nothing"
   where
     isNatKind :: Kind -> Bool
     isNatKind = (`eqType` typeNatKind)
 
-fromNatEquality :: Either NatEquality NatInEquality -> Ct
-fromNatEquality (Left (ct, _, _))  = ct
-fromNatEquality (Right (ct,_,_,_)) = ct
+createWantedFromNormalised :: ExtraDefs -> SolverConstraint -> TcPluginM Ct
+createWantedFromNormalised defs sct = do
+  let extractCtSides (NatEquality ct t1 t2 _)   = (ct, reifyEOP defs t1, reifyEOP defs t2)
+      extractCtSides (NatInequality ct x y b _) = let tc = if b then promotedTrueDataCon else promotedFalseDataCon
+                                                      t1 = TyConApp typeNatLeqTyCon [reifyEOP defs x, reifyEOP defs y]
+                                                      t2 = TyConApp tc []
+                                                    in (ct, t1, t2)
+  let (ct, t1, t2) = extractCtSides sct
+  newPredTy <- case splitTyConApp_maybe $ ctEvPred $ ctEvidence ct of
+    Just (tc, [a, b, _, _]) | tc `hasKey` eqPrimTyConKey -> pure (mkTyConApp tc [a, b, t1, t2])
+    _ -> fail "Nothing"
+  ev <- newWanted (ctLoc ct) newPredTy
+  return (ct { cc_ev = ev })
+
+fromSolverConstraint :: SolverConstraint -> Ct
+fromSolverConstraint (NatEquality ct _ _ _)  = ct
+fromSolverConstraint (NatInequality ct _ _ _ _) = ct
 
 lookupExtraDefs :: TcPluginM ExtraDefs
 lookupExtraDefs = do
diff --git a/src/GHC/TypeLits/Extra/Solver/Operations.hs b/src/GHC/TypeLits/Extra/Solver/Operations.hs
--- a/src/GHC/TypeLits/Extra/Solver/Operations.hs
+++ b/src/GHC/TypeLits/Extra/Solver/Operations.hs
@@ -11,6 +11,9 @@
 module GHC.TypeLits.Extra.Solver.Operations
   ( ExtraOp (..)
   , ExtraDefs (..)
+  , Normalised (..)
+  , NormaliseResult
+  , mergeNormalised
   , reifyEOP
   , mergeMax
   , mergeMin
@@ -42,6 +45,23 @@
 import TyCon      (TyCon)
 import Type       (Type, TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy)
 
+-- | Indicates whether normalisation has occured
+data Normalised = Normalised | Untouched
+  deriving Eq
+
+instance Outputable Normalised where
+  ppr Normalised = text "Normalised"
+  ppr Untouched  = text "Untouched"
+
+mergeNormalised :: Normalised -> Normalised -> Normalised
+mergeNormalised Normalised _ = Normalised
+mergeNormalised _ Normalised = Normalised
+mergeNormalised _ _          = Untouched
+
+-- | A normalise result contains the ExtraOp and a flag that indicates whether any expression
+-- | was normalised within the ExtraOp.
+type NormaliseResult = (ExtraOp, Normalised)
+
 data ExtraOp
   = I    Integer
   | V    TyVar
@@ -110,80 +130,80 @@
 reifyEOP defs (Exp x y)  = mkTyConApp typeNatExpTyCon  [reifyEOP defs x
                                                        ,reifyEOP defs y]
 
-mergeMax :: ExtraDefs -> ExtraOp -> ExtraOp -> ExtraOp
-mergeMax _ (I 0) y = y
-mergeMax _ x (I 0) = x
+mergeMax :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult
+mergeMax _ (I 0) y = (y, Normalised)
+mergeMax _ x (I 0) = (x, Normalised)
 mergeMax defs x y =
   let x' = reifyEOP defs x
       y' = reifyEOP defs y
       z  = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])))
 #if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)
   in  case runWriterT (isNatural z) of
-        Just (True , cs) | Set.null cs -> y
-        Just (False, cs) | Set.null cs -> x
+        Just (True , cs) | Set.null cs -> (y, Normalised)
+        Just (False, cs) | Set.null cs -> (x, Normalised)
 #else
   in  case isNatural z of
-        Just True  -> y
-        Just False -> x
+        Just True  -> (y, Normalised)
+        Just False -> (x, Normalised)
 #endif
-        _ -> Max x y
+        _ -> (Max x y, Untouched)
 
-mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> ExtraOp
+mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult
 mergeMin defs x y =
   let x' = reifyEOP defs x
       y' = reifyEOP defs y
       z  = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])))
 #if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)
   in  case runWriterT (isNatural z) of
-        Just (True, cs) | Set.null cs -> x
-        Just (False,cs) | Set.null cs -> y
+        Just (True, cs) | Set.null cs -> (x, Normalised)
+        Just (False,cs) | Set.null cs -> (y, Normalised)
 #else
   in  case isNatural z of
-        Just True  -> x
-        Just False -> y
+        Just True  -> (x, Normalised)
+        Just False -> (y, Normalised)
 #endif
-        _ -> Min x y
+        _ -> (Min x y, Untouched)
 
-mergeDiv :: ExtraOp -> ExtraOp -> Maybe ExtraOp
+mergeDiv :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
 mergeDiv _     (I 0)      = Nothing
-mergeDiv (I i) (I j)      = Just (I (div i j))
-mergeDiv x y              = Just (Div x y)
+mergeDiv (I i) (I j)      = Just (I (div i j), Normalised)
+mergeDiv x y              = Just (Div x y, Untouched)
 
-mergeMod :: ExtraOp -> ExtraOp -> Maybe ExtraOp
+mergeMod :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
 mergeMod _     (I 0)      = Nothing
-mergeMod (I i) (I j)      = Just (I (mod i j))
-mergeMod x y              = Just (Mod x y)
+mergeMod (I i) (I j)      = Just (I (mod i j), Normalised)
+mergeMod x y              = Just (Mod x y, Untouched)
 
-mergeFLog :: ExtraOp -> ExtraOp -> Maybe ExtraOp
+mergeFLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
 mergeFLog (I i) _         | i < 2  = Nothing
-mergeFLog i     (Exp j k) | i == j = Just k
-mergeFLog (I i) (I j)              = I <$> flogBase i j
-mergeFLog x     y                  = Just (FLog x y)
+mergeFLog i     (Exp j k) | i == j = Just (k, Normalised)
+mergeFLog (I i) (I j)              = fmap (\r -> (I r, Normalised)) (flogBase i j)
+mergeFLog x     y                  = Just (FLog x y, Untouched)
 
-mergeCLog :: ExtraOp -> ExtraOp -> Maybe ExtraOp
+mergeCLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
 mergeCLog (I i) _         | i < 2  = Nothing
-mergeCLog i     (Exp j k) | i == j = Just k
-mergeCLog (I i) (I j)              = I <$> clogBase i j
-mergeCLog x     y                  = Just (CLog x y)
+mergeCLog i     (Exp j k) | i == j = Just (k, Normalised)
+mergeCLog (I i) (I j)              = fmap (\r -> (I r, Normalised)) (clogBase i j)
+mergeCLog x     y                  = Just (CLog x y, Untouched)
 
-mergeLog :: ExtraOp -> ExtraOp -> Maybe ExtraOp
+mergeLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
 mergeLog (I i) _          | i < 2   = Nothing
-mergeLog b     (Exp b' y) | b == b' = Just y
-mergeLog (I i) (I j)                = I <$> exactLogBase i j
-mergeLog x     y                    = Just (Log x y)
+mergeLog b     (Exp b' y) | b == b' = Just (y, Normalised)
+mergeLog (I i) (I j)                = fmap (\r -> (I r, Normalised)) (exactLogBase i j)
+mergeLog x     y                    = Just (Log x y, Untouched)
 
-mergeGCD :: ExtraOp -> ExtraOp -> ExtraOp
-mergeGCD (I i) (I j) = I (gcd i j)
-mergeGCD x     y     = GCD x y
+mergeGCD :: ExtraOp -> ExtraOp -> NormaliseResult
+mergeGCD (I i) (I j) = (I (gcd i j), Normalised)
+mergeGCD x     y     = (GCD x y, Untouched)
 
-mergeLCM :: ExtraOp -> ExtraOp -> ExtraOp
-mergeLCM (I i) (I j) = I (lcm i j)
-mergeLCM x     y     = LCM x y
+mergeLCM :: ExtraOp -> ExtraOp -> NormaliseResult
+mergeLCM (I i) (I j) = (I (lcm i j), Normalised)
+mergeLCM x     y     = (LCM x y, Untouched)
 
-mergeExp :: ExtraOp -> ExtraOp -> ExtraOp
-mergeExp (I i) (I j)                = I (i^j)
-mergeExp b     (Log b' y) | b == b' = y
-mergeExp x     y                    = Exp x y
+mergeExp :: ExtraOp -> ExtraOp -> NormaliseResult
+mergeExp (I i) (I j)                = (I (i^j), Normalised)
+mergeExp b     (Log b' y) | b == b' = (y, Normalised)
+mergeExp x     y                    = (Exp x y, Untouched)
 
 -- | \x y -> logBase x y, x > 1 && y > 0
 flogBase :: Integer -> Integer -> Maybe Integer
diff --git a/src/GHC/TypeLits/Extra/Solver/Unify.hs b/src/GHC/TypeLits/Extra/Solver/Unify.hs
--- a/src/GHC/TypeLits/Extra/Solver/Unify.hs
+++ b/src/GHC/TypeLits/Extra/Solver/Unify.hs
@@ -10,6 +10,7 @@
 module GHC.TypeLits.Extra.Solver.Unify
   ( ExtraDefs (..)
   , UnifyResult (..)
+  , NormaliseResult
   , normaliseNat
   , unifyExtra
   )
@@ -18,14 +19,13 @@
 -- external
 import Control.Monad.Trans.Class    (lift)
 import Control.Monad.Trans.Maybe    (MaybeT (..))
-import Control.Monad.Trans.Writer.Strict (runWriter)
+import Data.Maybe                   (catMaybes)
 import Data.Function                (on)
 import GHC.TypeLits.Normalise.Unify (CType (..))
-import qualified GHC.TypeLits.Normalise.Unify as Normalise
 
 -- GHC API
 import Outputable (Outputable (..), ($$), text)
-import TcPluginM  (TcPluginM, matchFam, tcPluginTrace)
+import TcPluginM  (TcPluginM, tcPluginTrace)
 import TcTypeNats (typeNatExpTyCon)
 import Type       (TyVar, coreView)
 import TyCoRep    (Type (..), TyLit (..))
@@ -40,46 +40,65 @@
 -- internal
 import GHC.TypeLits.Extra.Solver.Operations
 
-normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
+mergeNormResWith
+  :: (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
+  -> MaybeT TcPluginM NormaliseResult
+  -> MaybeT TcPluginM NormaliseResult
+  -> MaybeT TcPluginM NormaliseResult
+mergeNormResWith f x y = do
+  (x', n1) <- x
+  (y', n2) <- y
+  (res, n3) <- f x' y'
+  pure (res, n1 `mergeNormalised` n2 `mergeNormalised` n3)
+
+
+normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
 normaliseNat defs ty | Just ty1 <- coreView ty = normaliseNat defs ty1
-normaliseNat _ (TyVarTy v)          = pure (V v)
-normaliseNat _ (LitTy (NumTyLit i)) = pure (I i)
+normaliseNat _ (TyVarTy v)          = pure (V v, Untouched)
+normaliseNat _ (LitTy (NumTyLit i)) = pure (I i, Untouched)
 normaliseNat defs (TyConApp tc [x,y])
-  | tc == maxTyCon defs = mergeMax defs <$> normaliseNat defs x
-                                        <*> normaliseNat defs y
-  | tc == minTyCon defs = mergeMin defs <$> normaliseNat defs x
-                                        <*> normaliseNat defs y
-  | tc == divTyCon defs = do x' <- normaliseNat defs x
-                             y' <- normaliseNat defs y
-                             MaybeT (return (mergeDiv x' y'))
-  | tc == modTyCon defs = do x' <- normaliseNat defs x
-                             y' <- normaliseNat defs y
-                             MaybeT (return (mergeMod x' y'))
-  | tc == flogTyCon defs = do x' <- normaliseNat defs x
-                              y' <- normaliseNat defs y
-                              MaybeT (return (mergeFLog x' y'))
-  | tc == clogTyCon defs = do x' <- normaliseNat defs x
-                              y' <- normaliseNat defs y
-                              MaybeT (return (mergeCLog x' y'))
-  | tc == logTyCon defs = do x' <- normaliseNat defs x
-                             y' <- normaliseNat defs y
-                             MaybeT (return (mergeLog x' y'))
-  | tc == gcdTyCon defs = mergeGCD <$> normaliseNat defs x
-                                   <*> normaliseNat defs y
-  | tc == lcmTyCon defs = mergeLCM <$> normaliseNat defs x
-                                   <*> normaliseNat defs y
-  | tc == typeNatExpTyCon = mergeExp <$> normaliseNat defs x
-                                     <*> normaliseNat defs y
+  | tc == maxTyCon defs = mergeNormResWith (\x' y' -> return (mergeMax defs x' y'))
+                                           (normaliseNat defs x)
+                                           (normaliseNat defs y)
+  | tc == minTyCon defs = mergeNormResWith (\x' y' -> return (mergeMin defs x' y'))
+                                           (normaliseNat defs x)
+                                           (normaliseNat defs y)
+  | tc == divTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeDiv x' y')))
+                                           (normaliseNat defs x)
+                                           (normaliseNat defs y)
+  | tc == modTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeMod x' y')))
+                                           (normaliseNat defs x)
+                                           (normaliseNat defs y)
+  | tc == flogTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeFLog x' y')))
+                                           (normaliseNat defs x)
+                                           (normaliseNat defs y)
+  | tc == clogTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeCLog x' y')))
+                                           (normaliseNat defs x)
+                                           (normaliseNat defs y)
+  | tc == logTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeLog x' y')))
+                                           (normaliseNat defs x)
+                                           (normaliseNat defs y)
+  | tc == gcdTyCon defs = mergeNormResWith (\x' y' -> return (mergeGCD x' y'))
+                                           (normaliseNat defs x)
+                                           (normaliseNat defs y)
+  | tc == lcmTyCon defs = mergeNormResWith (\x' y' -> return (mergeLCM x' y'))
+                                           (normaliseNat defs x)
+                                           (normaliseNat defs y)
+  | tc == typeNatExpTyCon = mergeNormResWith (\x' y' -> return (mergeExp x' y'))
+                                             (normaliseNat defs x)
+                                             (normaliseNat defs y)
 
 normaliseNat defs (TyConApp tc tys) = do
-  tys'   <- mapM (fmap (reifyEOP defs) . normaliseNat defs) tys
-  tyM    <- lift (matchFam tc tys')
-  case tyM of
-    Just (_,ty) -> normaliseNat defs ty
-    _ -> let q = fst (runWriter (Normalise.normaliseNat (TyConApp tc tys')))
-         in  return (C (CType (Normalise.reifySOP q)))
+  let mergeExtraOp [] = []
+      mergeExtraOp ((Just (op, Normalised), _):xs) = reifyEOP defs op:mergeExtraOp xs
+      mergeExtraOp ((_, ty):xs) = ty:mergeExtraOp xs
 
-normaliseNat _ t = return (C (CType t))
+  normResults <- lift (sequence (runMaybeT . normaliseNat defs <$> tys))
+  let anyNormalised = foldr mergeNormalised Untouched (snd <$> catMaybes normResults)
+  let tys' = mergeExtraOp (zip normResults tys)
+  pure (C (CType (TyConApp tc tys')), anyNormalised)
+
+normaliseNat _ t = return (C (CType t), Untouched)
 
 -- | Result of comparing two 'SOP' terms, returning a potential substitution
 -- list under which the two terms are equal.
diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs
--- a/tests/ErrorTests.hs
+++ b/tests/ErrorTests.hs
@@ -97,6 +97,9 @@
 
 testFail26 = testFail26' (Proxy @4) (Proxy @6) (Proxy @6)
 
+testFail27 :: Proxy n -> Proxy (n + 2 <=? Max (n + 1) 1) -> Proxy True
+testFail27 _ = id
+
 testFail1Errors =
   ["Expected type: Proxy (GCD 6 8) -> Proxy 4"
   ,"Actual type: Proxy 4 -> Proxy 4"
@@ -214,4 +217,9 @@
 testFail26Errors =
   ["Could not deduce: Max x y ~ n"
   ,"from the context: (x <=? n) ~ 'True"
+  ]
+
+testFail27Errors =
+  ["Expected type: Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True"
+  ,"Actual type: Proxy 'True -> Proxy 'True"
   ]
diff --git a/tests/Main.hs b/tests/Main.hs
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -191,6 +191,38 @@
   -> Proxy (Max 0 (BitPack a) + CLog 2 2)
 test52 _ = id
 
+test53
+  :: Proxy n
+  -> Proxy (1 <=? Max (n + 1) 1)
+  -> Proxy True
+test53 _ = id
+
+test54
+  :: Proxy n
+  -> Proxy (n <=? Max (n + 1) 1)
+  -> Proxy True
+test54 _ = id
+
+test55
+  :: Proxy n
+  -> Proxy (n + 1 <=? Max (n + 1) 1)
+  -> Proxy True
+test55 _ = id
+
+test56
+  :: Proxy n
+  -> Proxy p
+  -> Proxy (n <=? Max (n + p) p)
+  -> Proxy True
+test56 _ _ = id
+
+test57
+  :: Proxy n
+  -> Proxy p
+  -> Proxy (n + 1 <=? Max (n + p + 1) p)
+  -> Proxy True
+test57 _ _ = id
+
 main :: IO ()
 main = defaultMain tests
 
@@ -353,6 +385,21 @@
     , testCase "forall a . (1 + BitPack a) ~ (Max 0 (BitPack a) + CLog 2 2" $
       show (test52 Proxy Proxy) @?=
       "Proxy"
+    , testCase "forall n . 1 <= Max (n + 1) 1" $
+      show (test53 Proxy Proxy) @?=
+      "Proxy"
+    , testCase "forall n . n <= Max (n + 1) 1" $
+      show (test54 Proxy Proxy) @?=
+      "Proxy"
+    , testCase "forall n . n + 1 <= Max (n + 1) 1" $
+      show (test55 Proxy Proxy) @?=
+      "Proxy"
+    , testCase "forall n p . n <= Max (n + p) p" $
+      show (test56 Proxy Proxy Proxy) @?=
+      "Proxy"
+    , testCase "forall n p . n + 1 <= Max (n + p + 1) p" $
+      show (test57 Proxy Proxy Proxy) @?=
+      "Proxy"
     ]
   , testGroup "errors"
     [ testCase "GCD 6 8 /~ 4" $ testFail1 `throws` testFail1Errors
@@ -381,6 +428,7 @@
     , testCase "(z <=? Max x y) /~ True" $ testFail24 `throws` testFail24Errors
     , testCase "(x+1 <=? Max x y) /~ True" $ testFail25 `throws` testFail25Errors
     , testCase "(x <= n) /=> (Max x y) ~ n" $ testFail26 `throws` testFail26Errors
+    , testCase "n + 2 <=? Max (n + 1) 1 /~ True" $ testFail27 `throws` testFail27Errors
     ]
   ]