diff --git a/Changelog.md b/Changelog.md
new file mode 100644
--- /dev/null
+++ b/Changelog.md
@@ -0,0 +1,6 @@
+# Changelog
+
+## 1.3.0.0
+
+* Supports GHC 9.6
+* Adds compatibility layer for `SNat` singleton provided since base 4.18
diff --git a/src/Data/Type/Natural.hs b/src/Data/Type/Natural.hs
--- a/src/Data/Type/Natural.hs
+++ b/src/Data/Type/Natural.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE EmptyCase #-}
@@ -32,6 +33,7 @@
     toSomeSNat,
     withSNat,
     withKnownNat,
+    fromSNat,
     natVal,
     natVal',
     someNatVal,
@@ -103,20 +105,23 @@
     -- * Singletons for auxiliary types
     SBool (..),
     SOrdering (..),
+    OrderingI(..),
+    fromOrderingI,
+    toOrderingI,
     FlipOrdering,
     sFlipOrdering,
   )
 where
 
-import Data.Coerce (coerce)
 import Data.Proxy (Proxy)
 import Data.Type.Natural.Core
 import Data.Type.Natural.Lemma.Arithmetic
 import Data.Type.Natural.Lemma.Order
 import Language.Haskell.TH (litT, numTyLit)
 import Language.Haskell.TH.Quote
-import Numeric.Natural
 import Text.Read (readMaybe)
+import Data.Ord (comparing)
+import Data.Function (on)
 
 {- | Quotesi-quoter for SNatleton types for @'GHC.TypeLits.Nat'@. This can be used for an expression.
 
@@ -141,7 +146,8 @@
     }
 
 toNatural :: SNat n -> Natural
-toNatural = coerce
+{-# DEPRECATED toNatural "Use fromSNat instead" #-}
+toNatural = fromSNat
 
 data SomeSNat where
   SomeSNat :: KnownNat n => SNat n -> SomeSNat
@@ -149,8 +155,12 @@
 deriving instance Show SomeSNat
 
 instance Eq SomeSNat where
-  SomeSNat (SNat n) == SomeSNat (SNat m) = n == m
-  SomeSNat (SNat n) /= SomeSNat (SNat m) = n /= m
+  (==) = (==) `on` \(SomeSNat n) -> fromSNat n
+  {-# INLINE (==) #-}
+
+instance Ord SomeSNat where
+  compare = comparing (\(SomeSNat n) -> fromSNat n)
+  {-# INLINE compare #-}
 
 toSomeSNat :: Natural -> SomeSNat
 toSomeSNat n = case someNatVal n of
diff --git a/src/Data/Type/Natural/Core.hs b/src/Data/Type/Natural/Core.hs
--- a/src/Data/Type/Natural/Core.hs
+++ b/src/Data/Type/Natural/Core.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE EmptyCase #-}
@@ -23,11 +24,16 @@
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
 
 module Data.Type.Natural.Core
-  ( SNat (.., Zero, Succ),
+  ( SNat (Zero, Succ),
+#if !MIN_VERSION_base(4,18,0)
+    fromSNat,
+    withKnownNat,
+    withSomeSNat,
+#endif
+    unsafeLiftSBin,
     ZeroOrSucc (..),
     viewNat,
     sNat,
-    withKnownNat,
     (%+),
     (%-),
     (%*),
@@ -56,73 +62,119 @@
     FlipOrdering,
     SOrdering (..),
     SBool (..),
+    Natural,
+    OrderingI(..),
+    fromOrderingI,
+    toOrderingI,
     -- Re-exports
     module GHC.TypeNats,
   )
 where
 
-import Data.Coerce (coerce)
-import Data.Proxy (Proxy)
 import Data.Type.Equality
-  ( TestEquality (..),
-    gcastWith,
-    type (:~:) (..),
+  ( type (:~:) (..),
     type (==),
   )
-import Data.Type.Natural.Utils
-import GHC.Exts (Proxy#, proxy#)
 import GHC.TypeNats
 import Math.NumberTheory.Logarithms (naturalLog2)
-import Numeric.Natural (Natural)
 import Type.Reflection (Typeable)
 import Unsafe.Coerce (unsafeCoerce)
+import Numeric.Natural
 
+#if MIN_VERSION_base(4,16,0)
+import Data.Type.Ord (OrderingI(..))
+#endif
+
+#if !MIN_VERSION_base(4,18,0)
+import Data.Proxy
+import Data.Type.Equality
+import GHC.Exts
+#endif
+
+#if !MIN_VERSION_base(4,18,0)
 -- | A singleton for type-level naturals
-newtype SNat (n :: Nat) = SNat Natural
+newtype SNat (n :: Nat) = UnsafeSNat Natural
   deriving newtype (Show, Eq, Ord)
 
-withKnownNat :: forall n r. SNat n -> (KnownNat n => r) -> r
-withKnownNat (SNat n) act =
+fromSNat :: SNat n -> Natural
+fromSNat = coerce
+
+withKnownNat :: forall n rep (r :: TYPE rep). SNat n -> (KnownNat n => r) -> r
+withKnownNat (UnsafeSNat n) act =
   case someNatVal n of
     SomeNat (_ :: Proxy m) ->
-      gcastWith (unsafeCoerce (Refl @()) :: n :~: m) act
+      case unsafeCoerce (Refl @()) :: n :~: m of
+        Refl -> act
 
+data KnownNatInstance (n :: Nat) where
+  KnownNatInstance :: KnownNat n => KnownNatInstance n
+
+-- An internal function that is only used for defining the SNat pattern
+-- synonym.
+knownNatInstance :: SNat n -> KnownNatInstance n
+knownNatInstance sn = withKnownNat sn KnownNatInstance
+
+pattern SNat :: forall n. () => KnownNat n => SNat n
+pattern SNat <- (knownNatInstance -> KnownNatInstance) 
+  where SNat = sNat
+
+withSomeSNat :: forall rep (r :: TYPE rep). Natural -> (forall n. SNat n -> r) -> r
+withSomeSNat n f = f (UnsafeSNat n)
+#endif
+
+unsafeLiftSBin :: (Natural -> Natural -> Natural) -> SNat n -> SNat m -> SNat k
+{-# INLINE unsafeLiftSBin #-}
+unsafeLiftSBin f = \l r -> withSomeSNat (fromSNat l `f` fromSNat r) unsafeCoerce
+
+unsafeLiftSUnary :: (Natural -> Natural) -> SNat n -> SNat k
+{-# INLINE unsafeLiftSUnary #-}
+unsafeLiftSUnary f = \l -> withSomeSNat (f $ fromSNat l) unsafeCoerce
+
 (%+) :: SNat n -> SNat m -> SNat (n + m)
-(%+) = coerce $ (+) @Natural
+{-# INLINE (%+) #-}
+(%+) = unsafeLiftSBin (+)
 
 (%-) :: SNat n -> SNat m -> SNat (n - m)
-(%-) = coerce $ (-) @Natural
+(%-) = unsafeLiftSBin (-)
 
 (%*) :: SNat n -> SNat m -> SNat (n * m)
-(%*) = coerce $ (*) @Natural
+(%*) = unsafeLiftSBin (*)
 
 sDiv :: SNat n -> SNat m -> SNat (Div n m)
-sDiv = coerce $ div @Natural
+sDiv = unsafeLiftSBin quot
 
 sMod :: SNat n -> SNat m -> SNat (Mod n m)
-sMod = coerce $ mod @Natural
+sMod = unsafeLiftSBin rem
 
 (%^) :: SNat n -> SNat m -> SNat (n ^ m)
-(%^) = coerce $ (^) @Natural @Natural
+(%^) = unsafeLiftSBin (^)
 
 sLog2 :: SNat n -> SNat (Log2 n)
-sLog2 = coerce $ fromIntegral @Int @Natural . naturalLog2
+sLog2 = unsafeLiftSUnary $ fromIntegral . naturalLog2
 
 sNat :: forall n. KnownNat n => SNat n
-sNat = SNat $ natVal' (proxy# :: Proxy# n)
+#if MIN_VERSION_base(4,18,0)
+sNat = SNat
+#else
+sNat = UnsafeSNat $ natVal' (proxy# :: Proxy# n)
+#endif
 
+
 infixl 6 %+, %-
 
 infixl 7 %*, `sDiv`, `sMod`
 
 infixr 8 %^
 
+#if !MIN_VERSION_ghc(4,18,0)
 instance TestEquality SNat where
-  testEquality (SNat l) (SNat r) =
+  testEquality (UnsafeSNat l) (UnsafeSNat r) =
     if l == r
       then Just trustMe
       else Nothing
+#endif
 
+
 -- | Since 1.1.0.0 (Type changed)
 data Equality n m where
   Equal :: ((n == n) ~ 'True) => Equality n n
@@ -141,8 +193,8 @@
 infix 4 ===, %~
 
 (%~) :: SNat l -> SNat r -> Equality l r
-SNat l %~ SNat r =
-  if l == r
+l %~ r =
+  if fromSNat l == fromSNat r
     then unsafeCoerce (Equal @())
     else unsafeCoerce (NonEqual @0 @1)
 
@@ -195,27 +247,45 @@
     Equal -> IsZero
     NonEqual -> IsSucc (sPred n)
 
+
+#if !MIN_VERSION_base(4,16,0)
+data OrderingI (a :: Nat) (b :: Nat) where
+  LTI :: CmpNat a b ~ 'LT => OrderingI a b
+  EQI :: CmpNat a b ~ 'EQ => OrderingI a b
+  GTI :: CmpNat a b ~ 'GT => OrderingI a b
+#endif
+
 type family FlipOrdering ord where
   FlipOrdering 'LT = 'GT
   FlipOrdering 'GT = 'LT
   FlipOrdering 'EQ = 'EQ
 
-sFlipOrdering :: SOrdering ord -> SOrdering (FlipOrdering ord)
-sFlipOrdering SLT = SGT
-sFlipOrdering SEQ = SEQ
-sFlipOrdering SGT = SLT
-
 data SOrdering (ord :: Ordering) where
   SLT :: SOrdering 'LT
   SEQ :: SOrdering 'EQ
   SGT :: SOrdering 'GT
 
+fromOrderingI :: OrderingI n m -> SOrdering (CmpNat n m)
+fromOrderingI LTI = SLT
+fromOrderingI EQI = SEQ
+fromOrderingI GTI = SGT
+
+toOrderingI :: SOrdering (CmpNat n m) -> OrderingI n m
+toOrderingI SLT = LTI
+toOrderingI SEQ = EQI
+toOrderingI SGT = GTI
+
 deriving instance Show (SOrdering ord)
 
 deriving instance Eq (SOrdering ord)
 
 deriving instance Typeable SOrdering
 
+sFlipOrdering :: SOrdering ord -> SOrdering (FlipOrdering ord)
+sFlipOrdering SLT = SGT
+sFlipOrdering SEQ = SEQ
+sFlipOrdering SGT = SLT
+
 data SBool (b :: Bool) where
   SFalse :: SBool 'False
   STrue :: SBool 'True
@@ -229,15 +299,16 @@
 infix 4 %<=?
 
 (%<=?) :: SNat n -> SNat m -> SBool (n <=? m)
-SNat n %<=? SNat m =
-  if n <= m
+n %<=? m =
+  if fromSNat n <= fromSNat m
     then unsafeCoerce STrue
     else unsafeCoerce SFalse
 
 sCmpNat, sCompare :: SNat n -> SNat m -> SOrdering (CmpNat n m)
 sCompare = sCmpNat
-sCmpNat (SNat n) (SNat m) =
-  case compare n m of
+sCmpNat n m =
+  case compare (fromSNat n) (fromSNat m) of
     LT -> unsafeCoerce SLT
     EQ -> unsafeCoerce SEQ
     GT -> unsafeCoerce SGT
+
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
@@ -154,12 +154,10 @@
   )
 where
 
-import Data.Coerce (coerce)
 import Data.Type.Equality (gcastWith, (:~:) (..))
 import Data.Type.Natural.Core
 import Data.Type.Natural.Lemma.Arithmetic
 import Data.Void (Void, absurd)
-import Numeric.Natural (Natural)
 import Proof.Equational
   ( because,
     start,
@@ -271,10 +269,12 @@
 #endif
 
 sMin :: SNat n -> SNat m -> SNat (Min n m)
-sMin = coerce $ min @Natural
+{-# INLINE sMin #-}
+sMin = unsafeLiftSBin min
 
 sMax :: SNat n -> SNat m -> SNat (Max n m)
-sMax = coerce $ max @Natural
+{-# INLINE sMax #-}
+sMax = unsafeLiftSBin max
 
 #if MIN_VERSION_ghc(9,2,1)
 type Max m n = DTO.Max @Nat m n
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
@@ -137,7 +137,7 @@
   (KnownNat n) =>
   Show (Ordinal (n :: Nat))
   where
-  showsPrec d o = showChar '#' . showParen True (showsPrec d (ordToNatural o) . showString " / " . showsPrec d (toNatural (sNat :: SNat n)))
+  showsPrec d o = showChar '#' . showParen True (showsPrec d (ordToNatural o) . showString " / " . showsPrec d (fromSNat (sNat :: SNat n)))
 
 instance Eq (Ordinal (n :: Nat)) where
   o == o' = ordToNatural o == ordToNatural o'
@@ -179,7 +179,7 @@
 
 -- | Enumerate all @'Ordinal'@s less than @n@.
 enumOrdinal :: SNat (n :: Nat) -> [Ordinal n]
-enumOrdinal sn = withKnownNat sn $ map (reallyUnsafeNaturalToOrd Proxy) [0 .. toNatural sn - 1]
+enumOrdinal sn = withKnownNat sn $ map (reallyUnsafeNaturalToOrd Proxy) [0 .. fromSNat sn - 1]
 
 -- | Since 1.0.0.0 (type changed)
 succOrd :: forall (n :: Nat). (KnownNat n) => Ordinal n -> Ordinal (Succ n)
@@ -270,7 +270,7 @@
 ordToNatural ::
   Ordinal (n :: Nat) ->
   Natural
-ordToNatural (OLt n) = toNatural n
+ordToNatural (OLt n) = fromSNat n
 
 {- | Inclusion function for ordinals.
 
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
@@ -127,11 +127,14 @@
   eith <- try @SomeException $ evaluate contradiction
   case eith of
     Left someE -> do
-      pure $
+      pure $ counterexample (show someE) $
         property $
           "Impossible" `isPrefixOf` show someE
             || "Non-exhaustive" `isInfixOf` show someE
-    Right {} -> pure $ property False
+            || "missingAlt" `isInfixOf` show someE
+    Right v -> 
+      pure $ counterexample "Value of void returned..." 
+        $ property False
 
 test_Lemmas :: TestTree
 test_Lemmas =
@@ -146,8 +149,8 @@
         \(SomeSNat sn) (SomeSNat sm) ->
           case succDiffNat sn (sn %+ sm) (DiffNat sn sm) of
             DiffNat sns sms ->
-              toNatural (sns %+ sms)
-                === toNatural sn + toNatural sm + 1
+              fromSNat (sns %+ sms)
+                === fromSNat sn + fromSNat sm + 1
     , testProperty @(SomeSNat -> SomeSNat -> Property)
         "compareCongR terminates"
         $ \(SomeSNat a) (SomeSNat (_ :: SNat b)) ->
@@ -157,9 +160,9 @@
         $ \case
           MkSomeLeqNat a b ->
             case leqToCmp a b Witness of
-              Left Refl -> toNatural a === toNatural b
+              Left Refl -> fromSNat a === fromSNat b
               Right Refl ->
-                property $ toNatural a < toNatural b
+                property $ fromSNat a < fromSNat b
     , testProperty @(SomeSNat -> Property)
         "eqlCmpEQ terminates"
         $ \(SomeSNat n) ->
@@ -248,24 +251,24 @@
     , testProperty @(SomeSNat -> Property) "leqViewRefl works properly" $ \(SomeSNat sn) ->
         case leqViewRefl sn of
           LeqZero sn' ->
-            toNatural sn' === toNatural sn .&&. toNatural sn' === 0
+            fromSNat sn' === fromSNat sn .&&. fromSNat sn' === 0
           LeqSucc sn' sm' Witness ->
-            toNatural sn' === toNatural sm'
-              .&&. toNatural sn' + 1 === toNatural sn
+            fromSNat sn' === fromSNat sm'
+              .&&. fromSNat sn' + 1 === fromSNat sn
     , testProperty @(SomeLeqNat -> Property) "viewLeq works properly" $ \(MkSomeLeqNat sn sm) ->
         case viewLeq sn sm Witness of
           LeqZero sm' ->
-            toNatural sn === 0 .&&. toNatural sm === toNatural sm'
+            fromSNat sn === 0 .&&. fromSNat sm === fromSNat sm'
           LeqSucc sn' sm' Witness ->
-            toNatural sn' + 1 === toNatural sn
-              .&&. toNatural sm' + 1 === toNatural sm
-              .&&. toNatural sn' <= toNatural sm'
+            fromSNat sn' + 1 === fromSNat sn
+              .&&. fromSNat sm' + 1 === fromSNat sm
+              .&&. fromSNat sn' <= fromSNat sm'
     , testProperty @(SomeLeqNat -> Property) "leqWitness gives the difference as a witness" $
         \(MkSomeLeqNat sn sm) ->
           case leqWitness sn sm Witness of
             DiffNat sn' delta ->
-              toNatural sn === toNatural sn'
-                .&&. toNatural sn' + toNatural delta === toNatural sm
+              fromSNat sn === fromSNat sn'
+                .&&. fromSNat sn' + fromSNat delta === fromSNat sm
     , testProperty @(SomeSNat -> SomeSNat -> Property)
         "leqStep terminates"
         $ \(SomeSNat n) (SomeSNat l) ->
@@ -392,7 +395,7 @@
           totalWitness $ maxLeqR n m
     , testProperty @(SomeLeqNat -> Property) "maxLeast termaxates" $
         \(MkSomeLeqNat n l) ->
-          forAll (elements [0 .. toNatural l]) $ \m0 ->
+          forAll (elements [0 .. fromSNat l]) $ \m0 ->
             case toSomeSNat m0 of
               SomeSNat m ->
                 totalWitness $
@@ -479,4 +482,4 @@
       )
 
 totalRefl :: a :~: b -> Property
-totalRefl = total
+totalRefl = within 10000 . total
diff --git a/tests/Data/Type/NaturalSpec.hs b/tests/Data/Type/NaturalSpec.hs
--- a/tests/Data/Type/NaturalSpec.hs
+++ b/tests/Data/Type/NaturalSpec.hs
@@ -23,50 +23,50 @@
     "Arithmetic operations on singletons behaves correctly"
     [ testProperty "(+), compared to demoted" $ \(SomeSNat n) (SomeSNat m) ->
         tabulateDigits [natVal n, natVal m] $
-          toNatural (n %+ m) === (natVal n + natVal m)
+          fromSNat (n %+ m) === (natVal n + natVal m)
     , $(testBinary "(+)" ''(+) '(%+))
     , testProperty "(-), compared to demoted" $ \(SomeSNat n) (SomeSNat m) ->
         tabulateDigits [natVal n, natVal m] $
           disjoin
-            [ natVal n < natVal m .&&. toNatural (m %- n) === (natVal m - natVal n)
-            , toNatural (n %- m) === (natVal n - natVal m)
+            [ natVal n < natVal m .&&. fromSNat (m %- n) === (natVal m - natVal n)
+            , fromSNat (n %- m) === (natVal n - natVal m)
             ]
     , $(testBinaryP (>=) "(-)" ''(-) '(%-))
     , testProperty "(*), compared to demoted" $ \(SomeSNat n) (SomeSNat m) ->
         tabulateDigits [natVal n, natVal m] $
-          toNatural (n %* m) === (natVal n * natVal m)
+          fromSNat (n %* m) === (natVal n * natVal m)
     , $(testBinary "(*)" ''(*) '(%*))
     , testProperty "Div, compared to demoted" $ \(SomeSNat n) (SomeSNat m) ->
         tabulateDigits [natVal n, natVal m] $
           label "divide by zero" (natVal m === 0)
-            .||. toNatural (n `sDiv` m) === (natVal n `div` natVal m)
+            .||. fromSNat (n `sDiv` m) === (natVal n `div` natVal m)
     , $(testBinaryP (const $ (/= 0)) "Div" ''Div 'sDiv)
     , testProperty "Mod, compared to demoted" $ \(SomeSNat n) (SomeSNat m) ->
         tabulateDigits [natVal n, natVal m] $
           label "divide by zero" (natVal m === 0)
-            .||. toNatural (n `sMod` m) === (natVal n `mod` natVal m)
+            .||. fromSNat (n `sMod` m) === (natVal n `mod` natVal m)
     , $(testBinaryP (const $ (/= 0)) "Mod" ''Mod 'sMod)
     , testProperty "(^), compared to demoted" $ \(SomeSNat n) (SomeSNat m) ->
         tabulateDigits [natVal n, natVal m] $
-          toNatural (n %^ m) === (natVal n ^ natVal m)
+          fromSNat (n %^ m) === (natVal n ^ natVal m)
     , $(testBinaryP (\a b -> a /= 0 && b /= 0) "(^)" ''(^) '(%^))
     , testProperty "(-.), compared to demoted" $ \(SomeSNat n) (SomeSNat m) ->
         tabulateDigits [natVal n, natVal m] $
-          toNatural (n %-. m) === (if natVal n < natVal m then 0 else natVal n - natVal m)
+          fromSNat (n %-. m) === (if natVal n < natVal m then 0 else natVal n - natVal m)
     , $(testBinary "(-.)" ''(-.) '(%-.))
     , testProperty "Log2" $ \(SomeSNat n) ->
         tabulateDigits [natVal n] $
           label "undefined" (natVal n === 0)
-            .||. toNatural (sLog2 n) === fromIntegral (naturalLog2 (natVal n))
+            .||. fromSNat (sLog2 n) === fromIntegral (naturalLog2 (natVal n))
     , $(testUnary False "Log2" ''Log2 'sLog2)
     , testProperty "succ" $ \(SomeSNat n) ->
         tabulateDigits [natVal n] $
-          toNatural (sSucc n) === succ (natVal n)
+          fromSNat (sSucc n) === succ (natVal n)
     , $(testUnary True "Succ" ''Succ 'sSucc)
     , testProperty "pred" $ \(SomeSNat n) ->
         tabulateDigits [natVal n] $
           label "undefiend" (natVal n === 0)
-            .||. toNatural (sPred n) === pred (natVal n)
+            .||. fromSNat (sPred n) === pred (natVal n)
     , $(testUnary False "Pred" ''Pred 'sPred)
     ]
 
@@ -105,11 +105,11 @@
     , $(testBinary "CmpNat" ''CmpNat 'sCmpNat)
     , testProperty "min" $ \(SomeSNat n) (SomeSNat m) ->
         tabulateDigits [natVal n, natVal m] $
-          toNatural (n `sMin` m) === (natVal n `min` natVal m)
+          fromSNat (n `sMin` m) === (natVal n `min` natVal m)
     , $(testBinary "min" ''Min 'sMin)
     , testProperty "max" $ \(SomeSNat n) (SomeSNat m) ->
         tabulateDigits [natVal n, natVal m] $
-          toNatural (n `sMax` m) === (natVal n `max` natVal m)
+          fromSNat (n `sMax` m) === (natVal n `max` natVal m)
     , $(testBinary "max" ''Max 'sMax)
     ]
 
diff --git a/tests/Shared.hs b/tests/Shared.hs
--- a/tests/Shared.hs
+++ b/tests/Shared.hs
@@ -68,7 +68,7 @@
 
 instance Demote Nat where
   type Demoted Nat = Natural
-  demote = toNatural
+  demote = fromSNat
 
 type instance Sing = SOrdering
 
diff --git a/type-natural.cabal b/type-natural.cabal
--- a/type-natural.cabal
+++ b/type-natural.cabal
@@ -1,13 +1,13 @@
 cabal-version: >=1.10
 name:          type-natural
-version:       1.2.0.1
+version:       1.3.0.0
 license:       BSD3
 license-file:  LICENSE
-copyright:     (C) Hiromi ISHII 2013-2022
+copyright:     (C) Hiromi ISHII 2013-2023
 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.4 || ==9.4.3
+  GHC ==8.6.5 || ==8.8.4 || ==8.10.7 || ==9.0.2 || ==9.2.7 || ==9.4.4 || ==9.6.1
 
 homepage:      https://github.com/konn/type-natural
 synopsis:      Type-level natural and proofs of their properties.
@@ -20,6 +20,8 @@
 
 category:      Math
 build-type:    Simple
+extra-source-files:
+  Changelog.md
 
 source-repository head
   type:     git
@@ -56,7 +58,7 @@
     TypeOperators
     UndecidableInstances
 
-  ghc-options:        -Wall -O2 -fno-warn-orphans
+  ghc-options:        -Wall -fno-warn-orphans
   build-depends:
       base                       >=4       && <5
     , constraints                >=0.3
@@ -67,11 +69,13 @@
     , integer-logarithms
     , template-haskell           >=2.8
 
-  if impl(ghc >=9.4)
-    build-depends: ghc-typelits-presburger >=0.7.1
-
+  if impl(ghc >= 9.6)
+    build-depends: ghc-typelits-presburger >=0.7.2
   else
-    build-depends: ghc-typelits-presburger
+    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
@@ -82,7 +86,7 @@
 test-suite type-natural-test
   type:             exitcode-stdio-1.0
   main-is:          test.hs
-  build-tools:      tasty-discover -any
+  build-tool-depends: tasty-discover:tasty-discover
   hs-source-dirs:   tests
   default-language: Haskell2010
   ghc-options:      -Wall