diff --git a/sized.cabal b/sized.cabal
--- a/sized.cabal
+++ b/sized.cabal
@@ -1,6 +1,6 @@
 cabal-version: >=2.0
 name:          sized
-version:       0.8.0.0
+version:       0.9.0.0
 license:       BSD3
 license-file:  LICENSE
 maintainer:    konn.jinro_at_gmail.com
@@ -37,6 +37,7 @@
         type-natural >=0.8.1.0,
         ghc-typelits-presburger >=0.2.0.0,
         ghc-typelits-knownnat,
+        singletons-presburger,
         mono-traversable >=0.10,
         singletons >=2.0,
         subcategories,
diff --git a/src/Data/Sized.hs b/src/Data/Sized.hs
--- a/src/Data/Sized.hs
+++ b/src/Data/Sized.hs
@@ -71,7 +71,7 @@
     -- ** Definitions
     viewCons, ConsView (..), viewSnoc, SnocView(..),
 
-    pattern Nil, pattern (:<), pattern NilL , pattern (:>), pattern NilR,
+    pattern Nil, pattern (:<), pattern (:>),
   ) where
 
 import Data.Sized.Internal
@@ -97,13 +97,13 @@
 import           Data.Singletons.Prelude.Bool (Sing)
 import           Data.Singletons.Prelude.Enum (PEnum (..), sPred, sSucc)
 import           Data.These                   (These (..))
-import           Data.Type.Equality           ((:~:) (..), gcastWith)
+import           Data.Type.Equality           (gcastWith, (:~:) (..))
 import qualified Data.Type.Natural            as Peano
-import           Data.Type.Natural.Class      (type (-.), IsPeano (..), One,
-                                               PNum (..), POrd (..),
-                                               PeanoOrder (..), S, SNum (..),
-                                               Zero, pattern Zero,
-                                               ZeroOrSucc (..), sOne, sZero)
+import           Data.Type.Natural.Class      (IsPeano (..), One, PNum (..),
+                                               POrd (..), PeanoOrder (..), S,
+                                               SNum (..), Zero, ZeroOrSucc (..),
+                                               pattern Zero, sOne, sZero,
+                                               type (-.))
 import           Data.Type.Ordinal            (HasOrdinal, Ordinal (..),
                                                ordToNatural)
 import           Data.Typeable                (Typeable)
@@ -1220,7 +1220,9 @@
 -- Since 0.7.0.0
 data ConsView f n a where
   NilCV :: ConsView f (Zero nat) a
-  (:-) :: SingI n => a -> Sized f n a -> ConsView f (One nat + n) a
+  (:-)
+    :: (SingI n, SingI (One nat + n))
+    => a -> Sized f n a -> ConsView f (One nat + n) a
 
 infixr 5 :-
 
@@ -1323,13 +1325,6 @@
 pattern Nil <- (chkNil -> IsZero) where
   Nil = empty
 
--- | Pattern synonym for cons-side nil.
-{-# DEPRECATED NilL "Use Nil instead" #-}
-pattern NilL :: forall nat f (n :: nat) a.
-                (SingI n, CFreeMonoid f, Dom f a,  HasOrdinal nat)
-             => (n ~ Zero nat) => Sized f n a
-pattern NilL = Nil
-
 infixl 5 :>
 
 -- | Pattern synonym for snoc-side unsnoc.
@@ -1341,18 +1336,8 @@
 pattern a :> b <- (viewSnoc -> a :-:: b) where
   a :> b = a |> b
 
-{-# DEPRECATED NilR "Use Nil instead" #-}
-pattern NilR :: forall nat f (n :: nat) a.
-                (SingI n, CFreeMonoid f, Dom f a,  HasOrdinal nat)
-             => n ~ Zero nat => Sized f n a
-pattern NilR = Nil
-
 {-# COMPLETE (:<), Nil #-}
-{-# COMPLETE (:<), NilL #-}
-{-# COMPLETE (:<), NilR #-}
 {-# COMPLETE (:>), Nil #-}
-{-# COMPLETE (:>), NilL #-}
-{-# COMPLETE (:>), NilR #-}
 
 class Dom f a => DomC f a
 instance Dom f a => DomC f a
diff --git a/src/Data/Sized/Builtin.hs b/src/Data/Sized/Builtin.hs
--- a/src/Data/Sized/Builtin.hs
+++ b/src/Data/Sized/Builtin.hs
@@ -1,11 +1,11 @@
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE TypeOperators, NoImplicitPrelude #-}
-{-# LANGUAGE CPP, DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-}
-{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType           #-}
-{-# LANGUAGE ViewPatterns                                                 #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE NoStarIsType #-}
+{-# LANGUAGE CPP, ConstraintKinds, DataKinds, FlexibleContexts             #-}
+{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures                      #-}
+{-# LANGUAGE MultiParamTypeClasses, NoImplicitPrelude                      #-}
+{-# LANGUAGE NoMonomorphismRestriction, NoStarIsType, PatternSynonyms      #-}
+{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables, TypeApplications  #-}
+{-# LANGUAGE TypeInType, TypeOperators, UndecidableInstances, ViewPatterns #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
+{-# OPTIONS_GHC -fplugin Data.Singletons.TypeNats.Presburger #-}
 -- | This module exports provides the functionality to make length-parametrized types
 --   from existing 'CFreeMonoid' sequential types,
 --   parametrised with GHC's built in 'Nat' kind.
@@ -51,7 +51,7 @@
     Partitioned(), pattern Partitioned,
     takeWhile, dropWhile, span, break, partition,
     -- ** Searching
-    elem, notElem, find, findIndex, sFindIndex, 
+    elem, notElem, find, findIndex, sFindIndex,
     findIndices, sFindIndices,
     elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices,
     -- * Views and Patterns
@@ -69,31 +69,41 @@
     viewSnoc, SnocView,
     pattern (:-::), pattern NilSV,
 
-    pattern Nil, pattern (:<), pattern NilL , pattern (:>), pattern NilR,
+    pattern Nil, pattern (:<), pattern (:>),
   ) where
+import           Data.Sized (DomC)
 import qualified Data.Sized as S
-import Data.Sized (DomC)
 
 import           Control.Subcategory
+import           Data.Coerce                  (coerce)
 import           Data.Kind                    (Type)
-import           Data.Singletons.Prelude      (SingI)
+import           Data.Maybe                   (fromJust)
+import           Data.Singletons.Prelude      (SNum ((%+)), SingI (sing))
 import           Data.Singletons.Prelude.Enum (PEnum (..))
+import           Data.Singletons.TypeLits     (SNat, withKnownNat)
+import qualified Data.Sized.Internal          as Internal
+import           Data.Type.Natural            (IsPeano (toNatural, zeroOrSucc),
+                                               Min, PeanoOrder (plusMonotoneR))
+import           Data.Type.Natural.Class      (ZeroOrSucc (IsSucc, IsZero),
+                                               type (-.))
 import qualified Data.Type.Ordinal            as O
-import GHC.TypeNats (KnownNat, Nat) 
-import Prelude (Maybe, Ordering, Ord, Eq, Monoid, Bool(..), Int)
-import Data.Singletons.TypeLits (SNat)
-import Data.Singletons.Prelude (POrd((<=)))
-import Data.Type.Natural.Class (type (-.), type (<))
-import Data.Type.Natural (Min, type (-), type (+), type (*))
+import           GHC.TypeNats                 (KnownNat, Nat, type (*),
+                                               type (+), type (-), type (<=))
+import           Prelude                      (Bool (..), Eq, Int, Maybe,
+                                               Monoid, Ord, Ordering, const,
+                                               uncurry, ($), (.))
+import qualified Prelude                      as P
+import           Proof.Propositional          (IsTrue (Witness), withWitness)
 
 type Ordinal = (O.Ordinal :: Nat -> Type)
+type a < b = a + 1 <= b
 
 -- | @Sized@ wraps a sequential type 'f' and makes length-parametrized version.
 --
 -- Here, 'f' must satisfy @'CFreeMonoid' f@ and @Dom f a@.
 --
 -- Since 0.2.0.0
-type Sized = (S.Sized :: (Type -> Type) -> Nat -> Type -> Type)
+type Sized = (Internal.Sized :: (Type -> Type) -> Nat -> Type -> Type)
 
 -- | 'Sized' sequence with the length is existentially quantified.
 --   This type is used mostly when the return type's length cannot
@@ -143,9 +153,9 @@
 --   If you want to check boundary statically, use '%!!' or 'sIndex'.
 --
 -- Since 0.7.0.0
-(!!) :: (Dom f a, CFoldable f, (1 <= m) ~ 'True) => Sized f m a -> Int -> a
+(!!) :: forall f m a. (Dom f a, CFoldable f, (1 <= m)) => Sized f m a -> Int -> a
 {-# INLINE (!!) #-}
-(!!) = (S.!!) @Nat
+(!!) = coerce $ cindex @f @a
 
 -- | Safe indexing with 'Ordinal's.
 --
@@ -158,10 +168,10 @@
 --
 -- Since 0.7.0.0
 index
-  :: (Dom f a, CFoldable f, (1 <= m) ~ 'True)
+  :: (Dom f a, CFoldable f, (1 <= m))
   => Int -> Sized f m a -> a
 {-# INLINE index #-}
-index = S.index @Nat
+index = P.flip (!!)
 
 -- | Flipped version of '%!!'.
 --
@@ -175,18 +185,18 @@
 --   see  <#ViewsAndPatterns Views and Patterns> section.
 --
 -- Since 0.7.0.0
-head :: (Dom f a, CFoldable f, (0 < n) ~ 'True) => Sized f n a -> a
+head :: forall f n a. (Dom f a, CFoldable f, (1 <= n)) => Sized f n a -> a
 {-# INLINE head #-}
-head = S.head @Nat
+head = coerce $ chead @f @a
 
 -- | Take the last element of non-empty sequence.
 --   If you want to make case-analysis for general sequence,
 --   see  <#ViewsAndPatterns Views and Patterns> section.
 --
 -- Since 0.7.0.0
-last :: (Dom f a, CFoldable f, (0 < n) ~ 'True) => Sized f n a -> a
+last :: forall f n a. (Dom f a, CFoldable f, (0 < n)) => Sized f n a -> a
 {-# INLINE last #-}
-last = S.last @Nat
+last = coerce $ clast @f @a
 
 -- | Take the 'head' and 'tail' of non-empty sequence.
 --   If you want to make case-analysis for general sequence,
@@ -194,20 +204,22 @@
 --
 -- Since 0.7.0.0
 uncons
-  :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n) ~ 'True)
+  :: forall f n a.
+    (Dom f a, KnownNat n, CFreeMonoid f, (0 < n))
   => Sized f n a -> Uncons f n a
 {-# INLINE uncons #-}
-uncons = S.uncons @Nat
+uncons =
+  uncurry (Uncons @f @(Pred n) @a) . coerce (fromJust . cuncons @f @a)
 
 -- | 'uncons' with explicit specified length @n@
 --
 --   Since 0.7.0.0
 uncons'
-  :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n) ~ 'True)
+  :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n))
   => Sized f n a
   -> Uncons f n a
 {-# INLINE uncons' #-}
-uncons' = S.uncons @Nat
+uncons' = uncons
 
 -- | Take the 'init' and 'last' of non-empty sequence.
 --   If you want to make case-analysis for general sequence,
@@ -215,10 +227,10 @@
 --
 -- Since 0.7.0.0
 unsnoc
-  :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n) ~ 'True)
+  :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n))
   => Sized f n a -> Unsnoc f n a
 {-# INLINE unsnoc #-}
-unsnoc = S.unsnoc @Nat
+unsnoc = P.undefined
 
 -- | 'unsnoc'' with explicit specified length @n@
 --
@@ -227,13 +239,11 @@
 {-# INLINE unsnoc' #-}
 unsnoc' = S.unsnoc' @Nat
 
-type Uncons f (n :: Nat) a = S.Uncons f n a
-pattern Uncons
-  :: forall (f :: Type -> Type) (n :: Nat) a. ()
-  => forall (n1 :: Nat). (n ~ (1 + n1), SingI n1)
-  => a -> Sized f n1 a -> Uncons f n a
-pattern Uncons a as = S.Uncons a as
+data Uncons f n a where
+  Uncons :: forall f n a. KnownNat n
+    => a -> Sized f n a -> Uncons f (1 + n) a
 
+
 type Unsnoc f (n :: Nat) a = S.Unsnoc f n a
 
 pattern Unsnoc
@@ -265,10 +275,10 @@
 --
 -- Since 0.7.0.0
 take
-  :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True)
+  :: forall n f m a. (Dom f a, CFreeMonoid f, (n <= m))
   => SNat n -> Sized f m a -> Sized f n a
 {-# INLINE take #-}
-take = S.take @Nat
+take = coerce $ ctake @f @a . P.fromIntegral . toNatural @Nat @n
 
 -- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@.
 --
@@ -284,20 +294,20 @@
 --
 -- Since 0.7.0.0
 drop
-  :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True)
+  :: forall n f m a. (Dom f a, CFreeMonoid f, (n <= m))
   => SNat n -> Sized f m a -> Sized f (m - n) a
 {-# INLINE drop #-}
-drop = S.drop @Nat
+drop = coerce $ cdrop @f @a . P.fromIntegral . toNatural @Nat @n
 
 -- | @splitAt k xs@ split @xs@ at @k@, where
 -- the length of @xs@ should be less than or equal to @k@.
 --
 -- Since 0.7.0.0
 splitAt
-  :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True)
+  :: forall n f m a. (Dom f a, CFreeMonoid f, (n <= m))
   => SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a)
 {-# INLINE splitAt #-}
-splitAt = S.splitAt @Nat
+splitAt = coerce $ csplitAt @f @a . P.fromIntegral . toNatural @Nat
 
 -- | @splitAtMost k xs@ split @xs@ at @k@.
 --   If @k@ exceeds the length of @xs@, then the second result value become empty.
@@ -508,7 +518,7 @@
 -- Since 0.7.0.0
 intersperse
   :: (Dom f a, CFreeMonoid f)
-  => a -> Sized f n a -> Sized f ((2 * n) -. 1) a 
+  => a -> Sized f n a -> Sized f ((2 * n) -. 1) a
 {-# INLINE intersperse #-}
 intersperse = S.intersperse @Nat
 
@@ -716,7 +726,7 @@
 -- | Split the sequence into the longest prefix
 --   of elements that satisfy the predicate
 --   and the rest.
--- 
+--
 -- Since 0.7.0.0
 span :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a
 {-# INLINE span #-}
@@ -731,7 +741,7 @@
 break :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a
 break = S.break @Nat
 
--- | Split the sequence in two parts, the first one containing those elements that satisfy the predicate and the second one those that don't. 
+-- | Split the sequence in two parts, the first one containing those elements that satisfy the predicate and the second one those that don't.
 --
 -- Since 0.7.0.0
 {-# INLINE partition #-}
@@ -801,13 +811,13 @@
 {-# DEPRECATED sUnsafeElemIndex "Use sElemIndex instead" #-}
 
 -- | Ordinal version of 'elemIndex'.
---   Since 0.7.0.0, we no longer do boundary check inside the definition. 
+--   Since 0.7.0.0, we no longer do boundary check inside the definition.
 --
 --   Since 0.7.0.0
 sUnsafeElemIndex = S.sElemIndex @Nat
 
 -- | Ordinal version of 'elemIndex'.
---   Since 0.7.0.0, we no longer do boundary check inside the definition. 
+--   Since 0.7.0.0, we no longer do boundary check inside the definition.
 --
 --   Since 0.7.0.0
 sElemIndex = S.sElemIndex @Nat
@@ -870,37 +880,33 @@
 
 -- | View of the left end of sequence (cons-side).
 --
--- Since 0.7.0.0
-type ConsView = 
-  (S.ConsView :: (Type -> Type) -> Nat -> Type -> Type)
+-- Since 0.9.0.0
+data ConsView f n a where
+  NilCV :: ConsView f 0 a
+  (:-)
+    :: (KnownNat n, KnownNat (1 + n))
+    => a -> Sized f n a -> ConsView f (1 + n) a
 
--- | Since 0.8.0.0
-pattern NilCV
-  :: forall (f :: Type -> Type) n a. ()
-  => (n ~ 0)
-  => ConsView f n a
-pattern NilCV = S.NilCV
 
--- | Since 0.8.0.0
-pattern (:-)
-  :: forall (f :: Type -> Type) n a. ()
-  => forall n1. (n ~ (1 + n1), SingI n1)
-  => a -> Sized f n1 a -> ConsView f n a
-pattern l :- ls = l S.:- ls
-
 infixr 9 :-
-{-# COMPLETE NilCV, (:-) #-}
 
 -- | Case analysis for the cons-side of sequence.
 --
 -- Since 0.5.0.0 (type changed)
-viewCons :: (Dom f a, KnownNat n, CFreeMonoid f) => Sized f n a -> ConsView f n a
-viewCons = S.viewCons @Nat
+viewCons :: forall f n a. (Dom f a, KnownNat n, CFreeMonoid f) => Sized f n a -> ConsView f n a
+viewCons sz = case zeroOrSucc $ sing @n of
+  IsZero -> NilCV
+  IsSucc n' ->
+    withWitness (plusMonotoneR (sing @1) (sing @0) n' Witness) $
+    withKnownNat n'
+    $ withKnownNat (sing @1 %+ n')
+    $ case uncons' sz of
+        Uncons a xs -> a :- xs
 
 -- | View of the left end of sequence (snoc-side).
 --
 -- Since 0.7.0.0
-type SnocView = 
+type SnocView =
   (S.SnocView :: (Type -> Type) -> Nat -> Type -> Type)
 
 -- | Since 0.8.0.0
@@ -966,43 +972,34 @@
 pattern (:<)
   :: forall (f :: Type -> Type) a (n :: Nat).
       (Dom f a, KnownNat n, CFreeMonoid f)
-  => forall (n1 :: Nat). (n ~ (1 + n1), SingI n1)
+  => forall (n1 :: Nat). (n ~ (1 + n1), KnownNat n1, KnownNat n)
   => a -> Sized f n1 a -> Sized f n a
-pattern a :< b = a S.:< b
+pattern a :< as <- (viewCons -> a :- as) where
+   a :< as = a <| as
 infixr 5 :<
 
+chkNil
+  :: forall f n a.
+      (KnownNat n)
+  => Sized f n a -> ZeroOrSucc n
+chkNil = const $ zeroOrSucc $ sing @n
+
 -- | Pattern synonym for a nil sequence.
 pattern Nil
-  :: forall (f :: Type -> Type) a n. 
+  :: forall (f :: Type -> Type) n a.
       (Dom f a, KnownNat n, CFreeMonoid f)
   => (n ~ 0) => Sized f n a
-pattern Nil = S.Nil
-
-{-# DEPRECATED NilL "Use Nil instead" #-}
--- | Pattern synonym for cons-side nil.
-pattern NilL :: forall f (n :: Nat) a.
-                (KnownNat n, CFreeMonoid f, Dom f a)
-             => n ~ 0 => Sized f n a
-pattern NilL = Nil
+pattern Nil <- (chkNil -> IsZero) where
+  Nil = empty
 
 -- | Pattern synonym for snoc-side unsnoc.
 pattern (:>)
-  :: forall (f :: Type -> Type) a (n :: Nat). 
+  :: forall (f :: Type -> Type) a (n :: Nat).
       (Dom f a, KnownNat n, CFreeMonoid f)
   => forall (n1 :: Nat). (n ~ (n1 + 1), SingI n1)
   => Sized f n1 a -> a -> Sized f n a
 pattern a :> b = a S.:> b
 infixl 5 :>
 
-{-# DEPRECATED NilR "Use Nil instead" #-}
--- | Pattern synonym for snoc-side nil.
-pattern NilR :: forall f (n :: Nat) a.
-                (CFreeMonoid f, Dom f a,  KnownNat n)
-             => n ~ 0 => Sized f n a
-pattern NilR = Nil
-{-# COMPLETE (:<), NilL #-}
-{-# COMPLETE (:<), NilR #-}
 {-# COMPLETE (:<), Nil #-}
-{-# COMPLETE (:>), NilL #-}
-{-# COMPLETE (:>), NilR #-}
 {-# COMPLETE (:>), Nil #-}
diff --git a/src/Data/Sized/Peano.hs b/src/Data/Sized/Peano.hs
--- a/src/Data/Sized/Peano.hs
+++ b/src/Data/Sized/Peano.hs
@@ -1,10 +1,7 @@
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE TypeOperators, NoImplicitPrelude #-}
 {-# LANGUAGE CPP, DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-}
-{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType           #-}
-{-# LANGUAGE ViewPatterns                                                 #-}
-{-# LANGUAGE NoStarIsType #-}
+{-# LANGUAGE NoImplicitPrelude, NoMonomorphismRestriction, NoStarIsType   #-}
+{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeApplications     #-}
+{-# LANGUAGE TypeInType, TypeOperators, ViewPatterns                      #-}
 -- | This module exports provides the functionality to make length-parametrized types
 --   from existing 'CFreeMonoid' sequential types,
 --   parametrised with peano numeral 'PN.Nat' kind.
@@ -15,7 +12,7 @@
 --
 --  This module also provides powerful view types and pattern synonyms to
 --  inspect the sized sequence. See <#ViewsAndPatterns Views and Patterns> for more detail.
-module Data.Sized.Peano
+module Data.Sized.Peano {-# DEPRECATED "Removed in future release" #-}
   ( -- * Main Data-types
     Sized(), SomeSized, pattern SomeSized, Ordinal,
     DomC(),
@@ -50,7 +47,7 @@
     Partitioned(), pattern Partitioned,
     takeWhile, dropWhile, span, break, partition,
     -- ** Searching
-    elem, notElem, find, findIndex, sFindIndex, 
+    elem, notElem, find, findIndex, sFindIndex,
     findIndices, sFindIndices,
     elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices,
     -- * Views and Patterns
@@ -70,20 +67,19 @@
 
     pattern Nil, pattern (:<), pattern NilL , pattern (:>), pattern NilR,
   ) where
+import           Data.Sized (DomC)
 import qualified Data.Sized as S
-import Data.Sized (DomC)
 
 import           Control.Subcategory
 import           Data.Kind                    (Type)
-import           Data.Singletons.Prelude      (SingI)
+import           Data.Singletons.Prelude      (POrd ((<=)), SingI)
 import           Data.Singletons.Prelude.Enum (PEnum (..))
+import           Data.Type.Natural            (Min, Nat (..), One, SNat, Two,
+                                               type (*), type (+), type (-))
+import           Data.Type.Natural.Class      (type (-.), type (<))
 import qualified Data.Type.Ordinal            as O
-import Prelude (Maybe, Ordering, Ord, Eq, Monoid, Bool(..), Int)
-import Data.Type.Natural (Two, Nat(..), SNat)
-import Data.Singletons.Prelude (POrd((<=)))
-import Data.Type.Natural.Class (type (-.), type (<))
-import Data.Type.Natural (Min, type (-), type (+), type (*))
-import Data.Type.Natural (One)
+import           Prelude                      (Bool (..), Eq, Int, Maybe,
+                                               Monoid, Ord, Ordering)
 
 type Ordinal = (O.Ordinal :: Nat -> Type)
 
@@ -509,7 +505,7 @@
 {-# INLINE intersperse #-}
 intersperse
   :: (Dom f a, CFreeMonoid f)
-  => a -> Sized f n a -> Sized f ((Two * n) -. One) a 
+  => a -> Sized f n a -> Sized f ((Two * n) -. One) a
 intersperse = S.intersperse @Nat
 
 -- | Remove all duplicates.
@@ -716,7 +712,7 @@
 -- | Split the sequence into the longest prefix
 --   of elements that satisfy the predicate
 --   and the rest.
--- 
+--
 -- Since 0.7.0.0
 {-# INLINE span #-}
 span :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a
@@ -732,7 +728,7 @@
 break :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a
 break = S.break @Nat
 
--- | Split the sequence in two parts, the first one containing those elements that satisfy the predicate and the second one those that don't. 
+-- | Split the sequence in two parts, the first one containing those elements that satisfy the predicate and the second one those that don't.
 --
 -- Since 0.7.0.0
 {-# INLINE partition #-}
@@ -802,13 +798,13 @@
 {-# DEPRECATED sUnsafeElemIndex "Use sElemIndex instead" #-}
 
 -- | Ordinal version of 'elemIndex'.
---   Since 0.7.0.0, we no longer do boundary check inside the definition. 
+--   Since 0.7.0.0, we no longer do boundary check inside the definition.
 --
 --   Since 0.7.0.0
 sUnsafeElemIndex = S.sElemIndex @Nat
 
 -- | Ordinal version of 'elemIndex'.
---   Since 0.7.0.0, we no longer do boundary check inside the definition. 
+--   Since 0.7.0.0, we no longer do boundary check inside the definition.
 --
 --   Since 0.7.0.0
 sElemIndex = S.sElemIndex @Nat
@@ -973,7 +969,7 @@
 
 -- | Pattern synonym for a nil sequence.
 pattern Nil
-  :: forall (f :: Type -> Type) a n. 
+  :: forall (f :: Type -> Type) a n.
       (Dom f a, SingI n, CFreeMonoid f)
   => (n ~ 'Z) => Sized f n a
 pattern Nil = S.Nil
@@ -986,7 +982,7 @@
 
 -- | Pattern synonym for snoc-side unsnoc.
 pattern (:>)
-  :: forall (f :: Type -> Type) a (n :: Nat). 
+  :: forall (f :: Type -> Type) a (n :: Nat).
       (Dom f a, SingI n, CFreeMonoid f)
   => forall (n1 :: Nat). (n ~ (n1 + One), SingI n1)
   => Sized f n1 a -> a -> Sized f n a