diff --git a/examples/simple-arith.hs b/examples/simple-arith.hs
--- a/examples/simple-arith.hs
+++ b/examples/simple-arith.hs
@@ -2,34 +2,58 @@
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
 module Main where
 import Data.Type.Equality
-import GHC.TypeLits       (type (<=), type (*), type (+), type (<=?))
+import GHC.TypeLits       (Nat, type (<=), type (*), type (+), type (<=?), CmpNat)
 import Proof.Propositional (Empty(..))
 import Proof.Propositional (IsTrue(Witness))
+import Data.Singletons.Prelude
 
 type n <=! m = IsTrue (n <=? m)
 infix 4 <=!
 
-natLeqZero :: (n <= 0) => proxy n -> n :~: 0
-natLeqZero _ = Refl
+-- natLeqZero :: (n <= 0) => proxy n -> n :~: 0
+-- natLeqZero _ = Refl
 
+-- (%:<=?) :: Sing n -> Sing m -> Sing (n <=? m)
+-- n %:<=? m = case sCompare n m of
+--   SLT -> STrue
+--   SEQ -> STrue
+--   SGT -> SFalse
 
-hoge :: ((n + 1 <=? n) ~ 'False) => ()
-hoge = ()
+-- natLeqZero :: IsTrue (n <=? 0) -> Sing n -> n :~: 0
+-- natLeqZero Witness Zero = Refl
 
-fuga :: ((n + 1 <=? 0) ~ 'False) => ()
-fuga = ()
 
-bar :: ((2 * (n + 1)) ~ ((2 * n) + 2)) => ()
-bar = ()
+-- hoge :: ((n + 1 <=? n) ~ 'False) => ()
+-- hoge = ()
 
-trans :: proxy n -> proxy m -> n <=! m -> (n + 1) <=! (m + 1)
-trans _ _  Witness = Witness
+-- fuga :: ((n + 1 <=? 0) ~ 'False) => ()
+-- fuga = ()
 
-eqv :: proxy n -> proxy m -> (n <=? m) :~: ((n + 1) <=? (m + 1))
-eqv _ _ = Refl
+-- bar :: ((2 * (n + 1)) ~ ((2 * n) + 2)) => proxy n -> ()
+-- bar _ = ()
 
-predSucc :: forall proxy n. Empty (n <=! 0) => proxy n -> IsTrue (n + 1 <=? 2 * n)
-predSucc _ = Witness
+-- trans :: proxy n -> proxy m -> n <=! m -> (n + 1) <=! (m + 1)
+-- trans _ _  Witness = Witness
 
+-- eqv :: proxy n -> proxy m -> (n <=? m) :~: ((n + 1) <=? (m + 1))
+-- eqv _ _ = Refl
+
+-- leqSucc :: proxy n -> proxy m -> IsTrue ((n + 1) :<= m) -> CmpNat n m :~: 'LT
+-- leqSucc _ _ Witness = Refl
+
+
+-- predSucc :: forall proxy n. Empty (n <=! 0) => proxy n -> IsTrue (n + 1 <=? 2 * n)
+-- predSucc _ = Witness
+
 main :: IO ()
 main = putStrLn "finished"
+
+-- succLEqLTSucc :: Sing m -> Compare 0 (m + 1) :~: 'LT
+-- succLEqLTSucc _ = Refl
+
+
+-- succCompare :: Sing (n :: Nat) -> Sing m -> CmpNat n m :~: CmpNat (n + 1) (m + 1)
+-- succCompare _ _ = Refl
+
+eqToRefl :: Sing (n :: Nat) -> Sing (m :: Nat) -> CmpNat n m :~: 'EQ -> n :~: m
+eqToRefl _n _m Refl = Refl
diff --git a/ghc-typelits-presburger.cabal b/ghc-typelits-presburger.cabal
--- a/ghc-typelits-presburger.cabal
+++ b/ghc-typelits-presburger.cabal
@@ -1,7 +1,12 @@
 name:                ghc-typelits-presburger
-version:             0.1.0.0
-synopsis:            Initial project template from stack
-description:         Please see README.md
+version:             0.1.1.0
+synopsis:            Presburger Arithmetic Solver for GHC Type-level natural numbers.
+description: 
+  @ghc-typelits-presburger@ augments GHC type-system with Presburger Arithmetic Solver for Type-level natural numbers.
+  You can use by adding this package to @build-depends@ and add the following pragma to the head of .hs files:
+  .
+  > OPTIONS_GHC -fplugin GHC.TypeLits.Presburger
+                  
 homepage:            https://github.com/konn/ghc-typelits-presburger#readme
 license:             BSD3
 license-file:        LICENSE
diff --git a/src/GHC/Compat.hs b/src/GHC/Compat.hs
--- a/src/GHC/Compat.hs
+++ b/src/GHC/Compat.hs
@@ -17,9 +17,7 @@
                                           tcPluginTrace)
 import TcRnMonad           as GHC.Compat (Ct, TcPluginResult (..), isWanted)
 import TcRnTypes           as GHC.Compat (TcPlugin (..), ctEvPred, ctEvidence)
-import TcTypeNats          as GHC.Compat (typeNatAddTyCon, typeNatExpTyCon)
-import TcTypeNats          as GHC.Compat (typeNatLeqTyCon, typeNatMulTyCon)
-import TcTypeNats          as GHC.Compat (typeNatSubTyCon)
+import TcTypeNats          as GHC.Compat
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
 import           GhcPlugins (InScopeSet, Outputable, emptyUFM)
 import qualified PrelNames  as Old
diff --git a/src/GHC/TypeLits/Presburger.hs b/src/GHC/TypeLits/Presburger.hs
--- a/src/GHC/TypeLits/Presburger.hs
+++ b/src/GHC/TypeLits/Presburger.hs
@@ -15,6 +15,8 @@
 import           Data.Reflection  (give)
 import           TcPluginM        (tcLookupClass)
 import           TcPluginM        (lookupOrig)
+import           TysWiredIn       (promotedEQDataCon, promotedGTDataCon,
+                                   promotedLTDataCon)
 
 assert' :: Prop -> PropSet -> PropSet
 assert' p ps = foldr assert ps (p : varPos)
@@ -103,7 +105,7 @@
   let subst = foldr unionTvSubst emptyTvSubst $ map genSubst (gs ++ ds)
   tcPluginTrace "Current subst" (ppr subst)
   tcPluginTrace "wanteds" $ ppr $ map (deconsPred) ws
-  tcPluginTrace "givens" $ ppr $ map (deconsPred) gs
+  tcPluginTrace "givens" $ ppr $ map (substTy subst . deconsPred) gs
   tcPluginTrace "deriveds" $ ppr $ map deconsPred ds
   let wants = mapMaybe (\ct -> (,) ct <$> toPresburgerPred subst (substTy subst $ deconsPred ct)) $
               filter (isWanted . ctEvidence) ws
@@ -159,15 +161,15 @@
   | con == typeNatLeqTyCon = (:<=) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2
 toPresburgerPred subst ty
   | isEqPred ty = toPresburgerPredTree subst $ classifyPredType ty
-  | Just (con, [l, r]) <- splitTyConApp_maybe ty
+  | Just (con, [l, r]) <- splitTyConApp_maybe ty -- l ~ r
   , con == eqTyCon = toPresburgerPredTree subst $ EqPred NomEq l r
-  | Just (con, [_k, l, r]) <- splitTyConApp_maybe ty
+  | Just (con, [_k, l, r]) <- splitTyConApp_maybe ty -- l (:~: {k}) r
   , con == eqWitnessTyCon = toPresburgerPredTree subst $ EqPred NomEq l r
-  | Just (con, [l]) <- splitTyConApp_maybe ty
+  | Just (con, [l]) <- splitTyConApp_maybe ty -- Empty l => ...
   , con == emptyTyCon = Not <$> toPresburgerPred subst l
-  | Just (con, [l]) <- splitTyConApp_maybe ty
+  | Just (con, [l]) <- splitTyConApp_maybe ty -- IsTrue l =>
   , con == isTrueTyCon = toPresburgerPred subst l
-  | ts <- decompFunTy ty
+  | ts <- decompFunTy ty        -- v -> v' -> ... -> Void
   , (args , [vd]) <- splitAt (length ts - 1) ts
   , isVoidTy vd       = do
       preds <- mapM (toPresburgerPred subst) args
@@ -180,15 +182,43 @@
     Not <$> toPresburgerPredTree subst (EqPred NomEq p (mkTyConTy promotedTrueDataCon))
 toPresburgerPredTree subst (EqPred NomEq p b)  -- (n :<=? m) ~ 'True
   | Just promotedTrueDataCon  == tyConAppTyCon_maybe (substTy subst b)
-  , TyConApp con [t1, t2] <- substTy subst p
+  , Just (con, [t1, t2]) <- splitTyConApp_maybe (substTy subst p)
   , con == typeNatLeqTyCon = (:<=) <$> toPresburgerExp subst t1  <*> toPresburgerExp subst t2
 toPresburgerPredTree subst (EqPred NomEq p q)  -- (p :: Bool) ~ (q :: Bool)
   | typeKind p `eqType` mkTyConTy promotedBoolTyCon =
     (<=>) <$> toPresburgerPred subst p
           <*> toPresburgerPred subst q
-toPresburgerPredTree subst (EqPred NomEq t1 t2) -- (n :: Nat) ~ (m :: Nat)
-  | typeKind t1 `eqType` typeNatKind = (:==) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2
-toPresburgerPredTree subst (ClassPred con [t1, t2]) -- (n :: Nat) ~ (m :: Nat)
+toPresburgerPredTree subst (EqPred NomEq n m)  -- (n :: Nat) ~ (m :: Nat)
+  | typeKind n `eqType` typeNatKind =
+    (:==) <$> toPresburgerExp subst n
+          <*> toPresburgerExp subst m
+toPresburgerPredTree subst (EqPred _ t1 t2) -- CmpNat a b ~ CmpNat c d
+  | Just (con,  [a, b]) <- splitTyConApp_maybe (substTy subst t1)
+  , Just (con', [c, d]) <- splitTyConApp_maybe (substTy subst t2)
+  , con == typeNatCmpTyCon, con' == typeNatCmpTyCon
+  = (<=>) <$> ((:<) <$> toPresburgerExp subst a <*> toPresburgerExp subst b)
+          <*> ((:<) <$> toPresburgerExp subst c <*> toPresburgerExp subst d)
+toPresburgerPredTree subst (EqPred NomEq t1 t2) -- CmpNat a b ~ x
+  | Just (con, [a, b]) <- splitTyConApp_maybe (substTy subst t1)
+  , con == typeNatCmpTyCon
+  , Just cmp <- tyConAppTyCon_maybe (substTy subst t2) =
+    let dic = [(promotedLTDataCon, (:<))
+              ,(promotedEQDataCon, (:==))
+              ,(promotedGTDataCon, (:>))
+              ]
+    in lookup cmp dic <*> toPresburgerExp subst a
+                      <*> toPresburgerExp subst b
+toPresburgerPredTree subst (EqPred NomEq t1 t2) -- x ~ CmpNat a b
+  | Just (con, [a, b]) <- splitTyConApp_maybe (substTy subst t2)
+  , con == typeNatCmpTyCon
+  , Just cmp <- tyConAppTyCon_maybe (substTy subst t1) =
+    let dic = [(promotedLTDataCon, (:<))
+              ,(promotedEQDataCon, (:==))
+              ,(promotedGTDataCon, (:>))
+              ]
+    in lookup cmp dic <*> toPresburgerExp subst a
+                      <*> toPresburgerExp subst b
+toPresburgerPredTree subst (ClassPred con [t1, t2]) -- (n :: Nat) <= (m :: Nat)
   | typeNatLeqTyCon == classTyCon con
   , typeKind t1 `eqType` typeNatKind = (:<=) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2
 toPresburgerPredTree _ _ = Nothing
@@ -212,6 +242,8 @@
                  | (con, op) <- [(typeNatAddTyCon, (:+)), (typeNatSubTyCon, (:-))]]
   LitTy (NumTyLit n) -> Just (K n)
   _ -> Nothing
+
+-- simplTypeCmp :: Type -> Type
 
 simpleExp :: Type -> Type
 simpleExp (AppTy t1 t2) = AppTy (simpleExp t1) (simpleExp t2)