diff --git a/src/Plugin/TypeCheck/Nat/Simple.hs b/src/Plugin/TypeCheck/Nat/Simple.hs
--- a/src/Plugin/TypeCheck/Nat/Simple.hs
+++ b/src/Plugin/TypeCheck/Nat/Simple.hs
@@ -27,8 +27,8 @@
 --   >		=<< (,) <$> (givens =<< decodeAll gs) <*> (wanted =<< decode w)
 
 plugin :: Plugin
-plugin = typeCheckWith @L "Plugin.TypeCheck.Nat.Simple" \gs _ w -> do
+plugin = typeCheckWith @L "Plugin.TypeCheck.Nat.Simple" \occ gs _ w -> do
 	tell @L $ "givens: " .+. fromSDoc (ppr gs)
 	tell @L $ "wanted: " .+. fromSDoc (ppr w)
 	uncurry canDerive
-		=<< (,) <$> (givens =<< decodeAll gs) <*> (wanted =<< decode w)
+		=<< (,) <$> (givens =<< decodeAll occ gs) <*> (wanted =<< decode occ w)
diff --git a/src/Plugin/TypeCheck/Nat/Simple/Decode.hs b/src/Plugin/TypeCheck/Nat/Simple/Decode.hs
--- a/src/Plugin/TypeCheck/Nat/Simple/Decode.hs
+++ b/src/Plugin/TypeCheck/Nat/Simple/Decode.hs
@@ -4,11 +4,11 @@
 
 module Plugin.TypeCheck.Nat.Simple.Decode (
 	-- * DECODE CT
-	decodeAll, decode ) where
+	decodeAll, decode, lookupOrdCondCompare ) where
 
 import GHC.Tc.Types.Constraint (Ct)
 import GHC.Builtin.Types.Literals (
-	typeNatAddTyCon, typeNatSubTyCon, typeNatLeqTyCon )
+	typeNatAddTyCon, typeNatSubTyCon) -- , typeNatLeqTyCon )
 import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon)
 import GHC.Core.TyCo.Rep (Type(..), TyLit(..))
 import GHC.Types.Var (Var)
@@ -20,6 +20,13 @@
 import Data.Derivation.Expression (Exp(..), ExpType(..))
 import Plugin.TypeCheck.Nat.Simple.UnNomEq (unNomEq)
 
+import GHC.Tc.Plugin
+import GHC.TcPluginM.Extra
+import GHC.Data.FastString
+import GHC.Unit.Module
+import GHC.Types.Name.Occurrence
+import GHC.Core.TyCon
+
 ---------------------------------------------------------------------------
 
 -- * DECODE
@@ -29,28 +36,34 @@
 -- DECODE
 ---------------------------------------------------------------------------
 
-decodeAll :: (Monoid w, IsSDoc w, Set w w) => [Ct] -> Try w w [Exp Var 'Boolean]
-decodeAll = rights . (decode <$>)
+decodeAll :: (Monoid w, IsSDoc w, Set w w) => (TyCon, TyCon) -> [Ct] -> Try w w [Exp Var 'Boolean]
+decodeAll occ = rights . (decode occ <$>)
 
-decode :: (Monoid w, IsSDoc w) => Ct -> Try w w (Exp Var 'Boolean)
-decode = uncurry decodeTs <=< unNomEq
+decode :: (Monoid w, IsSDoc w) => (TyCon, TyCon) -> Ct -> Try w w (Exp Var 'Boolean)
+decode occ = uncurry (decodeTs occ) <=< unNomEq
 
-decodeTs :: (Monoid w, IsSDoc w) => Type -> Type -> Try w w (Exp Var 'Boolean)
-decodeTs (TyVarTy l) (TyVarTy r) = pure $ Var l :== Var r
-decodeTs l r = (:==) <$> exBool l <*> exBool r <|> (:==) <$> exNum l <*> exNum r
+decodeTs :: (Monoid w, IsSDoc w) => (TyCon, TyCon) -> Type -> Type -> Try w w (Exp Var 'Boolean)
+decodeTs _ (TyVarTy l) (TyVarTy r) = pure $ Var l :== Var r
+decodeTs occ l r = (:==) <$> exBool occ l <*> exBool occ r <|> (:==) <$> exNum l <*> exNum r
 
 ---------------------------------------------------------------------------
 -- BOOLEAN AND NUMBER
 ---------------------------------------------------------------------------
 
-exBool :: (Monoid s, IsSDoc e) => Type -> Try e s (Exp Var 'Boolean)
-exBool (TyVarTy v) = pure $ Var v
-exBool (TyConApp tc [])
+exBool :: (Monoid s, IsSDoc e) => (TyCon, TyCon) -> Type -> Try e s (Exp Var 'Boolean)
+exBool _ (TyVarTy v) = pure $ Var v
+exBool _ (TyConApp tc [])
 	| tc == promotedFalseDataCon = pure $ Bool False
 	| tc == promotedTrueDataCon = pure $ Bool True
-exBool (TyConApp tc [l, r])
-	| tc == typeNatLeqTyCon = (:<=) <$> exNum l <*> exNum r
-exBool t = throw . fromSDoc $ text "exBool: not boolean:" <+> ppr t
+-- exBool (TyConApp tc [l, r])
+--	| tc == typeNatLeqTyCon = (:<=) <$> exNum l <*> exNum r
+exBool (oc, cmp) (TyConApp tc [_,
+		TyConApp cmpNatTc [_, l, r],
+		TyConApp t1 [], TyConApp t2 [], TyConApp f1 []])
+	| tc == oc, cmpNatTc == cmp
+	, t1 == promotedTrueDataCon, t2 == promotedTrueDataCon
+	, f1 == promotedFalseDataCon = (:<=) <$> exNum l <*> exNum r
+exBool _ t = throw . fromSDoc $ text "exBool: not boolean:" <+> ppr t
 
 exNum :: (Monoid s, IsSDoc e) => Type -> Try e s (Exp Var 'Number)
 exNum (TyVarTy v) = pure $ Var v
@@ -59,3 +72,17 @@
 	| tc == typeNatAddTyCon = (:+) <$> exNum l <*> exNum r
 	| tc == typeNatSubTyCon = (:-) <$> exNum l <*> exNum r
 exNum t = throw . fromSDoc $ text "exNum: not number:" <+> ppr t
+
+lookupOrdCondCompare :: TcPluginM (TyCon, TyCon)
+lookupOrdCondCompare = do
+	md2 <- lookupModule ordModule basePackage
+	(,) <$> look md2 "OrdCond" <*> look md2 "Compare"
+
+ordModule :: ModuleName
+ordModule = mkModuleName "Data.Type.Ord"
+
+basePackage :: FastString
+basePackage = fsLit "base"
+
+look :: Module -> String -> TcPluginM TyCon
+look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s)
diff --git a/src/Plugin/TypeCheck/Nat/Simple/TypeCheckWith.hs b/src/Plugin/TypeCheck/Nat/Simple/TypeCheckWith.hs
--- a/src/Plugin/TypeCheck/Nat/Simple/TypeCheckWith.hs
+++ b/src/Plugin/TypeCheck/Nat/Simple/TypeCheckWith.hs
@@ -6,7 +6,7 @@
 	typeCheckWith ) where
 
 import GHC.Plugins (
-	Plugin(..), defaultPlugin, Expr(..), mkUnivCo, Role(..),
+	Plugin(..), defaultPlugin, Expr(..), mkUnivCo,
 	Outputable, ppr, text )
 import GHC.Tc.Plugin (TcPluginM, tcPluginTrace)
 import GHC.Tc.Types (TcPlugin(..), TcPluginResult(..))
@@ -18,19 +18,24 @@
 import Data.Log (IsSDoc, fromSDoc)
 import Plugin.TypeCheck.Nat.Simple.UnNomEq (unNomEq)
 
+import Plugin.TypeCheck.Nat.Simple.Decode (lookupOrdCondCompare)
+import GHC.Core.TyCon
+
 ---------------------------------------------------------------------------
 
 typeCheckWith :: (Monoid w, Outputable w, IsSDoc w, Set w w) =>
-	String -> ([Ct] -> [Ct] -> Ct -> Try w w Bool) -> Plugin
+	String -> ((TyCon, TyCon) -> [Ct] -> [Ct] -> Ct -> Try w w Bool) -> Plugin
 typeCheckWith hd ck = defaultPlugin { tcPlugin = const $ Just TcPlugin {
 	tcPluginInit = pure (), tcPluginSolve = const $ solve hd ck,
 	tcPluginStop = const $ pure () } }
 
 solve :: (Monoid w, Outputable w, IsSDoc w, Set w w) =>
-	String -> ([Ct] -> [Ct] -> Ct -> Try w w Bool) ->
+	String -> ((TyCon, TyCon) -> [Ct] -> [Ct] -> Ct -> Try w w Bool) ->
 	[Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
-solve hd ck gs ds ws = TcPluginOk rs [] <$ tcPluginTrace hd (ppr lgs)
-	where (rs, lgs) = gatherSuccess $ result hd ck gs ds <$> ws
+solve hd ck gs ds ws = do
+	occ <- lookupOrdCondCompare
+	let	(rs, lgs) = gatherSuccess $ result hd (ck occ) gs ds <$> ws
+	TcPluginOk rs [] <$ tcPluginTrace hd (ppr lgs)
 
 result :: (Monoid s, IsSDoc e) =>
 	String -> ([Ct] -> [Ct] -> Ct -> Try e s Bool) ->
diff --git a/typecheck-plugin-nat-simple.cabal b/typecheck-plugin-nat-simple.cabal
--- a/typecheck-plugin-nat-simple.cabal
+++ b/typecheck-plugin-nat-simple.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: a9ba3f2374494be0d74d84c38ca16841d48bfc5e88e9446906fc520669707902
+-- hash: e2e0789fc40e15f06d431a711fa5db62d9d427d20e869202ae7f8e3cac3e5fb9
 
 name:           typecheck-plugin-nat-simple
-version:        0.1.0.4
+version:        0.1.0.5
 synopsis:       Simple type check plugin which calculate addition, subtraction and less-or-equal-than
 description:    Please see the README on GitHub at <https://github.com/YoshikuniJujo/typecheck-plugin-nat-simple#readme>
 category:       Compiler Plugin
@@ -58,6 +58,7 @@
       base >=4.7 && <5
     , containers
     , ghc >=9.0.2
+    , ghc-tcplugins-extra
   default-language: Haskell2010
 
 test-suite typecheck-plugin-nat-simple-test-log
@@ -72,6 +73,7 @@
       base >=4.7 && <5
     , containers
     , ghc >=9.0.2
+    , ghc-tcplugins-extra
     , typecheck-plugin-nat-simple
   default-language: Haskell2010
 
@@ -87,6 +89,7 @@
       base >=4.7 && <5
     , containers
     , ghc >=9.0.2
+    , ghc-tcplugins-extra
     , typecheck-plugin-nat-simple
   default-language: Haskell2010
 
@@ -102,5 +105,6 @@
       base >=4.7 && <5
     , containers
     , ghc >=9.0.2
+    , ghc-tcplugins-extra
     , typecheck-plugin-nat-simple
   default-language: Haskell2010