diff --git a/src/Data/Type/Natural/Lemma/Arithmetic.hs b/src/Data/Type/Natural/Lemma/Arithmetic.hs
--- a/src/Data/Type/Natural/Lemma/Arithmetic.hs
+++ b/src/Data/Type/Natural/Lemma/Arithmetic.hs
@@ -16,6 +16,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE NoStarIsType #-}
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
 
 module Data.Type.Natural.Lemma.Arithmetic
diff --git a/src/Data/Type/Natural/Lemma/Order.hs b/src/Data/Type/Natural/Lemma/Order.hs
--- a/src/Data/Type/Natural/Lemma/Order.hs
+++ b/src/Data/Type/Natural/Lemma/Order.hs
@@ -36,8 +36,12 @@
     sMin,
     Max,
     sMax,
+    OrdCond,
+    sOrdCond,
 
     -- * Lemmas
+    ordCondDistrib,
+    leqOrdCond,
     sFlipOrdering,
     coerceLeqL,
     coerceLeqR,
@@ -58,6 +62,7 @@
     congFlipOrdering,
     ltToSuccLeq,
     cmpZero,
+    cmpSuccZeroGT,
     leqToGT,
     cmpZero',
     zeroNoLT,
@@ -118,6 +123,8 @@
     lneqSuccStepL,
     lneqSuccStepR,
     plusStrictMonotone,
+    minCase,
+    maxCase,
     maxZeroL,
     maxZeroR,
     minZeroL,
@@ -162,13 +169,44 @@
     (=~=),
   )
 import Proof.Propositional (IsTrue (..), eliminate, withWitness)
+#if MIN_VERSION_ghc(9,2,1)
+import qualified Data.Type.Ord as DTO
+import Data.Type.Ord (OrdCond)
+#endif
 
+
 --------------------------------------------------
 
 -- ** Type-level predicate & judgements.
 
 --------------------------------------------------
 
+#if !MIN_VERSION_ghc(9,2,1)
+type family OrdCond (o :: Ordering) (lt :: k) (eq :: k) (gt :: k) where
+  OrdCond 'LT lt eq gt = lt
+  OrdCond 'EQ lt eq gt = eq
+  OrdCond 'GT lt eq gt = gt
+#endif
+
+sOrdCond :: SOrdering o -> f lt -> f eq -> f gt -> f (OrdCond o lt eq gt)
+sOrdCond SLT lt _ _ = lt
+sOrdCond SEQ _ eq _ = eq
+sOrdCond SGT _ _ gt = gt
+
+minCase :: SNat n -> SNat m -> Either (Min n m :~: n) (Min n m :~: m)
+minCase n m =
+  case sCmpNat n m of
+    SLT -> Left Refl
+    SEQ -> Left Refl
+    SGT -> Right Refl
+
+maxCase :: SNat n -> SNat m -> Either (Max n m :~: m) (Max n m :~: n)
+maxCase n m =
+  case sCmpNat n m of
+    SLT -> Left Refl
+    SEQ -> Left Refl
+    SGT -> Right Refl
+
 -- | Comparison via GADTs.
 data Leq n m where
   ZeroLeq :: SNat m -> Leq 0 m
@@ -176,9 +214,10 @@
 
 type LeqWitness n m = IsTrue (n <=? m)
 
+-- | Since 1.2.0 (argument changed)
 data a :<: b where
-  ZeroLtSucc :: 0 :<: (m + 1)
-  SuccLtSucc :: n :<: m -> (n + 1) :<: (m + 1)
+  ZeroLtSucc :: SNat m -> 0 :<: (m + 1)
+  SuccLtSucc :: SNat n -> SNat m -> n :<: m -> (n + 1) :<: (m + 1)
 
 deriving instance Show (a :<: b)
 
@@ -206,16 +245,30 @@
 leqLhs (SuccLeqSucc leq) = sSucc $ leqLhs leq
 
 propToBoolLt :: n :<: m -> IsTrue (n <? m)
-propToBoolLt ZeroLtSucc = Witness
-propToBoolLt (SuccLtSucc lt) =
+propToBoolLt (ZeroLtSucc (sm :: SNat m)) = 
+  gcastWith (cmpZero sm) Witness
+propToBoolLt (SuccLtSucc sn sm lt) =
+  gcastWith (cmpSucc sn sm) $
   withWitness (propToBoolLt lt) Witness
 
 boolToPropLt :: n < m => SNat n -> SNat m -> n :<: m
-boolToPropLt Zero (Succ _) = ZeroLtSucc
-boolToPropLt (Succ _) Zero = eliminate (Refl :: 0 :~: 1)
-boolToPropLt (Succ n) (Succ m) = SuccLtSucc (boolToPropLt n m)
+boolToPropLt Zero (Succ sn) = ZeroLtSucc sn
+boolToPropLt (Succ n) Zero = eliminate $
+  start STrue
+  =~= (Succ n %<? Zero)
+  =~= sOrdCond (sCmpNat (Succ n) Zero) STrue SFalse SFalse
+  === sOrdCond SGT STrue SFalse SFalse
+    `because` sOrdCondCong1 (cmpSuccZeroGT n) STrue SFalse SFalse
+  =~= SFalse
+boolToPropLt (Succ n) (Succ m) = 
+  gcastWith (cmpSucc n m) $
+  SuccLtSucc n m (boolToPropLt n m)
 
-type Min n m = MinAux (n <=? m) n m
+#if MIN_VERSION_ghc(9,2,1)
+type Min m n = DTO.Min @Nat m n
+#else
+type Min m n = OrdCond (CmpNat m n) m m n
+#endif
 
 sMin :: SNat n -> SNat m -> SNat (Min n m)
 sMin = coerce $ min @Natural
@@ -223,41 +276,87 @@
 sMax :: SNat n -> SNat m -> SNat (Max n m)
 sMax = coerce $ max @Natural
 
-type family MinAux (p :: Bool) (n :: Nat) (m :: Nat) :: Nat where
-  MinAux 'True n _ = n
-  MinAux 'False _ m = m
-
-type Max n m = MaxAux (n >=? m) n m
-
-type family MaxAux (p :: Bool) (n :: Nat) (m :: Nat) :: Nat where
-  MaxAux 'True n _ = n
-  MaxAux 'False _ m = m
+#if MIN_VERSION_ghc(9,2,1)
+type Max m n = DTO.Max @Nat m n
+#else
+type Max m n = OrdCond (CmpNat m n) n n m
+#endif
 
 infix 4 <?, <, >=?, >=, >, >?
 
-type n <? m = n + 1 <=? m
+#if MIN_VERSION_ghc(9,2,1)
+type (n :: Nat) <? m = n DTO.<? m
+#else
+type n <? m = OrdCond (CmpNat n m) 'True 'False 'False
+#endif
 
 (%<?) :: SNat n -> SNat m -> SBool (n <? m)
-(%<?) = (%<=?) . sSucc
+n %<? m = sOrdCond (sCmpNat n m) STrue SFalse SFalse
 
+#if MIN_VERSION_ghc(9,2,2)
+type (n :: Nat) < m = n DTO.< m
+#else
 type n < m = (n <? m) ~ 'True
+#endif
 
-type n >=? m = m <=? n
+#if MIN_VERSION_ghc(9,2,1)
+type n >=? m = (DTO.>=?) @Nat n m
+#else
+type n >=? m = OrdCond (CmpNat n m) 'False 'True 'True
+#endif
 
 (%>=?) :: SNat n -> SNat m -> SBool (n >=? m)
-(%>=?) = flip (%<=?)
+n %>=? m = sOrdCond (sCmpNat n m) SFalse STrue STrue
 
+#if MIN_VERSION_ghc(9,2,1)
+type (n :: Nat) >= m = n DTO.>= m
+#else
 type n >= m = (n >=? m) ~ 'True
+#endif
 
-type n >? m = m <? n
+#if MIN_VERSION_ghc(9,2,1)
+type (n :: Nat) >? m = n DTO.>? m
+#else
+type n >? m = OrdCond (CmpNat n m) 'False 'False 'True
+#endif
 
 (%>?) :: SNat n -> SNat m -> SBool (n >? m)
-(%>?) = flip (%<?)
+n %>? m = sOrdCond (sCmpNat n m) SFalse SFalse STrue
 
+#if MIN_VERSION_ghc(9,2,1)
+type (n :: Nat) > m = n DTO.> m
+#else
 type n > m = (n >? m) ~ 'True
+#endif
 
 infix 4 %>?, %<?, %>=?
 
+ordCondDistrib :: proxy f -> SOrdering o -> p l -> p' e -> p'' g ->
+  OrdCond o (f l) (f e) (f g) :~: f (OrdCond o l e g)
+ordCondDistrib _ SLT _ _ _ = Refl
+ordCondDistrib _ SEQ _ _ _ = Refl
+ordCondDistrib _ SGT _ _ _ = Refl
+
+leqOrdCond
+  :: SNat n -> SNat m -> (n <=? m) :~: OrdCond (CmpNat n m) 'True 'True 'False
+#if MIN_VERSION_ghc(9,2,1)
+leqOrdCond _ _ = Refl
+#else
+leqOrdCond Zero n =
+  case cmpZero' n of
+    Left Refl -> Refl
+    Right Refl -> Refl
+leqOrdCond (Succ m) Zero = 
+  gcastWith (succLeqZeroAbsurd' m) $
+  gcastWith (cmpSuccZeroGT m) $
+  Refl
+leqOrdCond (Succ m) (Succ n) =
+  gcastWith (cmpSucc m n) $
+  start (Succ m %<=? Succ n)
+  === (m %<=? n) `because` sym (leqSucc' m n)
+  === sOrdCond (sCmpNat m n) STrue STrue SFalse `because` leqOrdCond m n
+#endif
+
 data LeqView n m where
   LeqZero :: SNat n -> LeqView 0 n
   LeqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView (Succ n) (Succ m)
@@ -373,6 +472,9 @@
 cmpZero :: SNat a -> CmpNat 0 (Succ a) :~: 'LT
 cmpZero _ = Refl
 
+cmpSuccZeroGT :: SNat a -> CmpNat (Succ a) 0 :~: 'GT
+cmpSuccZeroGT _ = Refl
+
 leqToGT ::
   SNat a ->
   SNat b ->
@@ -480,7 +582,7 @@
     step :: SNat x -> LeqWitPf x -> LeqWitPf (Succ x)
     step (n :: SNat x) (LeqWitPf ih) = LeqWitPf $ \m snLEQm ->
       case viewLeq (sSucc n) m snLEQm of
-#if !MIN_VERSION_ghc(9,2,0)
+#if !MIN_VERSION_ghc(9,2,0) || MIN_VERSION_ghc(9,4,0)
         LeqZero _ -> absurd $ succNonCyclic n Refl
 #endif
         LeqSucc (_ :: SNat n') pm nLEQpm ->
@@ -595,13 +697,17 @@
 leqSucc' _ _ = Refl
 
 leqToMin :: SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
-leqToMin _ _ Witness = Refl
+leqToMin n m Witness =
+  case leqToCmp n m Witness of
+    Left Refl -> Refl
+    Right Refl -> Refl
 
 geqToMin :: SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
 geqToMin n m Witness =
-  case n %<=? m of
-    SFalse -> Refl
-    STrue -> Refl
+  case leqToCmp m n Witness of
+    Left Refl -> Refl
+    Right Refl -> 
+      gcastWith (flipCmpNat m n) Refl
 
 minComm :: SNat n -> SNat m -> Min n m :~: Min m n
 minComm n m =
@@ -642,25 +748,23 @@
   IsTrue (l <=? n) ->
   IsTrue (l <=? m) ->
   IsTrue (l <=? Min n m)
-minLargest l n m lLEQn lLEQm =
-  withKnownNat l $
-    withKnownNat n $
-      withKnownNat m $
-        withKnownNat (sMin n m) $
-          case n %<=? m of
-            STrue -> lLEQn
-            SFalse -> lLEQm
+minLargest _ n m lLEQn lLEQm =
+  case minCase n m of
+    Left Refl -> lLEQn
+    Right Refl -> lLEQm
 
 leqToMax :: SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
-leqToMax n m Witness =
-  case n %>=? m of
-    STrue -> Refl
-    SFalse -> Refl
+leqToMax n m lLeqm =
+  case leqToCmp n m lLeqm of
+    Left Refl -> Refl
+    Right Refl -> Refl
 
 geqToMax :: SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
 geqToMax n m Witness =
-  case n %>=? m of
-    STrue -> Refl
+  case sCmpNat n m of
+    SLT -> Refl
+    SEQ -> Refl
+    SGT -> Refl
 
 maxComm :: SNat n -> SNat m -> Max n m :~: Max m n
 maxComm n m =
@@ -701,36 +805,57 @@
   IsTrue (n <=? l) ->
   IsTrue (m <=? l) ->
   IsTrue (Max n m <=? l)
-maxLeast l n m lLEQn lLEQm =
-  withKnownNat l $
-    withKnownNat n $
-      withKnownNat m $
-        withKnownNat (sMax n m) $
-          case n %>=? m of
-            STrue -> lLEQn
-            SFalse -> lLEQm
+maxLeast _ n m nLEQl mLEQl =
+  case maxCase n m of
+    Left Refl -> mLEQl
+    Right Refl -> nLEQl
 
-lneqSuccLeq :: SNat n -> SNat m -> (n < m) :~: (Succ n <= m)
+
+-- | Since 1.2.0.0 (type changed)
+lneqSuccLeq :: SNat n -> SNat m -> (n <? m) :~: (Succ n <=? m)
+#if MIN_VERSION_ghc(9,2,1)
 lneqSuccLeq _ _ = Refl
+#else
+lneqSuccLeq n m = isTrueRefl (n %<? m) (Succ n %<=? m)
+  (ltToSuccLeq n m . lneqToLT n m)
+  (ltToLneq n m . succLeqToLT n m)
 
-lneqReversed :: SNat n -> SNat m -> (n < m) :~: (m > n)
+isTrueRefl :: SBool a -> SBool b 
+  -> (IsTrue a -> IsTrue b)
+  -> (IsTrue b -> IsTrue a)
+  -> a :~: b
+isTrueRefl SFalse SFalse _ _ = Refl
+isTrueRefl STrue _ f _ = withWitness (f Witness) Refl
+isTrueRefl _ STrue _ g = withWitness (g Witness) Refl
+#endif
+
+-- | Since 1.2.0.0 (type changed)
+lneqReversed :: SNat n -> SNat m -> (n <? m) :~: (m >? n)
+#if MIN_VERSION_ghc(9,2,1)
 lneqReversed _ _ = Refl
+#else
+lneqReversed n m = 
+  case sCmpNat n m of
+    SLT -> gcastWith (flipCmpNat n m) Refl
+    SEQ -> gcastWith (flipCmpNat n m) Refl
+    SGT -> gcastWith (flipCmpNat n m) Refl
+#endif
 
 lneqToLT ::
   SNat n ->
   SNat m ->
   IsTrue (n <? m) ->
   CmpNat n m :~: 'LT
-lneqToLT n m nLNEm =
-  succLeqToLT n m $ gcastWith (lneqSuccLeq n m) nLNEm
+lneqToLT n m Witness =
+  case sCmpNat n m of
+    SLT -> Refl
 
 ltToLneq ::
   SNat n ->
   SNat m ->
   CmpNat n m :~: 'LT ->
   IsTrue (n <? m)
-ltToLneq n m nLTm =
-  gcastWith (sym $ lneqSuccLeq n m) $ ltToSuccLeq n m nLTm
+ltToLneq _ _ Refl = Witness
 
 lneqZero :: SNat a -> IsTrue (0 <? Succ a)
 lneqZero n = ltToLneq sZero (sSucc n) $ cmpZero n
@@ -742,7 +867,17 @@
   SNat n ->
   SNat m ->
   (n <? m) :~: (Succ n <? Succ m)
-succLneqSucc _ _ = Refl
+succLneqSucc n m = 
+  start (n %<? m)
+  =~=
+  sOrdCond (sCmpNat n m)  STrue SFalse SFalse
+  === sOrdCond (sCmpNat (Succ n) (Succ m)) STrue SFalse SFalse 
+    `because` sOrdCondCong1 (cmpSucc n m) STrue SFalse SFalse
+  =~= (Succ n %<? Succ m)
+
+sOrdCondCong1 :: o :~: o' -> proxy a -> proxy' b -> proxy' c 
+  -> OrdCond o a b c :~: OrdCond o' a b c
+sOrdCondCong1 Refl _ _ _ = Refl
 
 lneqRightPredSucc ::
   SNat n ->
diff --git a/src/Data/Type/Natural/Presburger/MinMaxSolver.hs b/src/Data/Type/Natural/Presburger/MinMaxSolver.hs
--- a/src/Data/Type/Natural/Presburger/MinMaxSolver.hs
+++ b/src/Data/Type/Natural/Presburger/MinMaxSolver.hs
@@ -48,14 +48,18 @@
 
   singMin <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "Min")
   singMax <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "Max")
-  caseMinAux <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "MinAux")
-  caseMaxAux <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "MaxAux")
+#if !MIN_VERSION_ghc(9,2,1)
+  ordCondTyCon <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "OrdCond")
+#endif
   return
     mempty
       { natGeqBool = [singNatGeq]
       , natLtBool = [singNatLt]
       , natGtBool = [singNatGt]
       , natMin = [singMin]
+#if !MIN_VERSION_ghc(9,2,1)
+      , ordCond = [ordCondTyCon]
+#endif
       , natMax = [singMax]
       , parsePred = \toE ty ->
           case splitTyConApp_maybe ty of
@@ -63,13 +67,5 @@
               | con == singNatLtProp -> (:<) <$> toE l <*> toE r
               | con == singNatGtProp -> (:>) <$> toE l <*> toE r
               | con == singNatGeqProp -> (:>=) <$> toE l <*> toE r
-            _ -> mzero
-      , parseExpr = \toE ty ->
-          case splitTyConApp_maybe ty of
-            Just (con, [_, n, m])
-              | con == caseMinAux ->
-                Min <$> toE n <*> toE m
-              | con == caseMaxAux ->
-                Max <$> toE n <*> toE m
             _ -> mzero
       }
diff --git a/src/Data/Type/Ordinal.hs b/src/Data/Type/Ordinal.hs
--- a/src/Data/Type/Ordinal.hs
+++ b/src/Data/Type/Ordinal.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE EmptyDataDecls #-}
@@ -19,8 +20,8 @@
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE ViewPatterns #-}
-{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
+{-# OPTIONS_GHC -fplugin Data.Type.Natural.Presburger.MinMaxSolver #-}
+{-# OPTIONS_GHC -fobject-code #-}
 
 {- | Set-theoretic ordinals for built-in type-level naturals
 
@@ -64,11 +65,13 @@
 import Data.Proxy (Proxy (Proxy))
 import Data.Type.Equality
 import Data.Type.Natural
-import Data.Type.Natural.Core (SNat (..))
 import Data.Typeable (Typeable)
 import Language.Haskell.TH.Quote
-import Numeric.Natural
+import Numeric.Natural ( Natural )
 import Unsafe.Coerce
+import Proof.Propositional (IsTrue (Witness))
+import Data.Type.Natural.Lemma.Order (lneqZeroAbsurd)
+import Data.Void (absurd)
 
 {- | Set-theoretic (finite) ordinals:
 
@@ -178,16 +181,15 @@
 enumOrdinal :: SNat (n :: Nat) -> [Ordinal n]
 enumOrdinal sn = withKnownNat sn $ map (reallyUnsafeNaturalToOrd Proxy) [0 .. toNatural sn - 1]
 
--- | Since 1.0.0.0(type changed)
+-- | Since 1.0.0.0 (type changed)
 succOrd :: forall (n :: Nat). (KnownNat n) => Ordinal n -> Ordinal (Succ n)
-succOrd (OLt n) =
-  OLt (sSucc n)
+succOrd (OLt k) = OLt (sSucc k)
 {-# INLINE succOrd #-}
 
 instance (KnownNat n, 0 < n) => Bounded (Ordinal n) where
   minBound = OLt sZero
 
-  maxBound = OLt $ sNat @(n - 1)
+  maxBound = withKnownNat (sNat @n %- sNat @1) $ OLt $ sNat @(n - 1)
 
 {- | Converts @'Natural'@s into @'Ordinal n'@.
    If the given natural is greater or equal to @n@, raises exception.
@@ -303,7 +305,7 @@
  Since 1.0.0.0
 -}
 absurdOrd :: Ordinal 0 -> a
-absurdOrd (OLt _) = case (Refl :: 0 :~: 1) of
+absurdOrd (OLt sn) = absurd $ lneqZeroAbsurd sn Witness
 
 {- | @'absurdOrd'@ for value in 'Functor'.
 
diff --git a/tests/Data/Type/Natural/Lemma/OrderSpec.hs b/tests/Data/Type/Natural/Lemma/OrderSpec.hs
--- a/tests/Data/Type/Natural/Lemma/OrderSpec.hs
+++ b/tests/Data/Type/Natural/Lemma/OrderSpec.hs
@@ -29,7 +29,7 @@
 someNat' = toSomeSNat . fromInteger . getNonNegative
 
 data SomeLeqNat where
-  MkSomeLeqNat :: n <= m => SNat n -> SNat m -> SomeLeqNat
+  MkSomeLeqNat :: (n <=? m) ~ 'True => SNat n -> SNat m -> SomeLeqNat
 
 data SomeLtNat where
   MkSomeLtNat ::
@@ -40,7 +40,7 @@
 
 data SomeLneqNat where
   MkSomeLneqNat ::
-    n < m =>
+    (n <? m) ~ 'True =>
     SNat n ->
     SNat m ->
     SomeLneqNat
@@ -461,6 +461,12 @@
         "truncMinusLeq terminates"
         $ \(SomeSNat n) (SomeSNat m) ->
           totalWitness $ truncMinusLeq n m
+    , testProperty @(SomeSNat -> SomeSNat -> Property)
+      "leqOrdCond terminates"
+      $ \(SomeSNat n) (SomeSNat m) -> totalRefl $ leqOrdCond n m
+    , testProperty @(SomeSNat -> Property)
+      "cmpSuccZeroGT terminates"
+      $ \(SomeSNat n) -> totalRefl $ cmpSuccZeroGT n
     ]
 
 totalWitness :: IsTrue p -> Property
diff --git a/tests/Shared.hs b/tests/Shared.hs
--- a/tests/Shared.hs
+++ b/tests/Shared.hs
@@ -8,6 +8,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Shared where
diff --git a/type-natural.cabal b/type-natural.cabal
--- a/type-natural.cabal
+++ b/type-natural.cabal
@@ -1,12 +1,14 @@
 cabal-version: >=1.10
 name:          type-natural
-version:       1.1.0.1
+version:       1.2.0.1
 license:       BSD3
 license-file:  LICENSE
-copyright:     (C) Hiromi ISHII 2013-2014
+copyright:     (C) Hiromi ISHII 2013-2022
 maintainer:    konn.jinro_at_gmail.com
 author:        Hiromi ISHII
-tested-with:   GHC ==8.6.5 || ==8.8.4 || ==8.10.7 || ==9.0.1 || ==9.2.1
+tested-with:
+  GHC ==8.6.5 || ==8.8.4 || ==8.10.7 || ==9.0.1 || ==9.2.4 || ==9.4.3
+
 homepage:      https://github.com/konn/type-natural
 synopsis:      Type-level natural and proofs of their properties.
 description:
@@ -62,9 +64,14 @@
     , ghc
     , ghc-typelits-knownnat
     , ghc-typelits-natnormalise  >=0.4
-    , ghc-typelits-presburger    >=0.5.1
     , integer-logarithms
     , template-haskell           >=2.8
+
+  if impl(ghc >=9.4)
+    build-depends: ghc-typelits-presburger >=0.7.1
+
+  else
+    build-depends: ghc-typelits-presburger
 
   if impl(ghc >=8.0.0)
     ghc-options: -Wno-redundant-constraints