diff --git a/Data/Type/Natural.hs b/Data/Type/Natural.hs
--- a/Data/Type/Natural.hs
+++ b/Data/Type/Natural.hs
@@ -1,7 +1,8 @@
-{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}
-{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude   #-}
-{-# LANGUAGE PolyKinds, RankNTypes, TemplateHaskell, TypeFamilies, ScopedTypeVariables       #-}
-{-# LANGUAGE TypeOperators, UndecidableInstances, StandaloneDeriving    #-}
+{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs     #-}
+{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude       #-}
+{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables, StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators                   #-}
+{-# LANGUAGE UndecidableInstances                                           #-}
 -- | Type level peano natural number, some arithmetic functions and their singletons.
 module Data.Type.Natural (-- * Re-exported modules.
                           module Data.Singletons,
@@ -40,7 +41,7 @@
                           -- ** Type-level predicate & judgements
                           Leq(..), (:<=), (:<<=),
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
-                          (:<<=$),(:<<=$$),(:<<=$$$), 
+                          (:<<=$),(:<<=$$),(:<<=$$$),
 #endif
                           (%:<<=), LeqInstance,
                           boolToPropLeq, boolToClassLeq, propToClassLeq,
@@ -85,136 +86,66 @@
                           sN0, sN1, sN2, sN3, sN4, sN5, sN6, sN7, sN8, sN9, sN10, sN11, sN12, sN13, sN14,
                           sN15, sN16, sN17, sN18, sN19, sN20
                          ) where
-import           Data.Singletons
+import Data.Singletons
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+import Data.Singletons.Prelude hiding ((:<=), Max, MaxSym0, MaxSym1, MaxSym2,
+                                Min, MinSym0, MinSym1, MinSym2, SOrd (..))
 import Data.Singletons.TH      (singletons)
-import Data.Singletons.Prelude hiding ((:<=), SOrd(..), MaxSym1, MaxSym0, MaxSym2
-                                      , MinSym1, MinSym0, MinSym2, Max, Min)
 #endif
+import           Data.Constraint           hiding ((:-))
 import           Data.Type.Monomorphic
-import           Prelude          (Int, Bool (..), Eq (..), Integral (..), Ord ((<)),
-                                   Show (..), error, id, otherwise, ($), (.), undefined)
-import qualified Prelude          as P
+import           Language.Haskell.TH
+import           Language.Haskell.TH.Quote
+import           Prelude                   (Bool (..), Eq (..), Int,
+                                            Integral (..), Ord ((<)), Show (..),
+                                            error, id, otherwise, undefined,
+                                            ($), (.))
+import qualified Prelude                   as P
 import           Proof.Equational
-import Data.Constraint hiding ((:-))
-import Language.Haskell.TH.Quote
-import Unsafe.Coerce
-import Language.Haskell.TH
+import           Unsafe.Coerce
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 710
+import Data.Type.Natural.Definitions hiding ((:<=))
+-- import Data.Type.Natural.Proofs.GHC710
+import Prelude (Num (..), Ord (..))
+#else
 import Data.Type.Natural.Definitions
-
-instance P.Num Nat where
-  n - m = n - m
-  n + m = n + m
-  n * m = n * m
-  abs = id
-  signum Z = Z
-  signum _ = S Z
-  fromInteger 0             = Z
-  fromInteger n | n P.< 0   = error "negative integer"
-                | otherwise = S $ P.fromInteger (n P.- 1)
-
---------------------------------------------------
--- ** Convenient synonyms
---------------------------------------------------
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
-sZ :: SNat Z
-sZ = SZ
-
-sS :: SNat n -> SNat (S n)
-sS = SS
-
-{-# DEPRECATED sZ, sS "Smart constructors are no longer needed in singletons; Use `SS` or `SZ` instead." #-}
+-- import Data.Type.Natural.Proofs.GHC708
 #endif
-
+import Data.Type.Natural.Core
 
 --------------------------------------------------
--- ** Type-level predicate & judgements.
+-- * Conversion functions.
 --------------------------------------------------
--- | Comparison via type-class.
-class (n :: Nat) :<= (m :: Nat)
-instance Z :<= n
-instance (n :<= m) => S n :<= S m
 
--- | Comparison via GADTs.
-data Leq (n :: Nat) (m :: Nat) where
-  ZeroLeq     :: SNat m -> Leq Zero m
-  SuccLeqSucc :: Leq n m -> Leq (S n) (S m)
-
-type LeqTrueInstance a b = Dict ((a :<<= b) ~ True)
-
-(%-) :: (m :<<= n) ~ True => SNat n -> SNat m -> SNat (n :-: m)
-n   %- SZ    = n
-SS n %- SS m = n %- m
-_    %- _    = error "impossible!"
-
-infixl 6 %-
-deriving instance Show (SNat n)
-deriving instance Eq (SNat n)
-
-data (a :: Nat) :<: (b :: Nat) where
-  ZeroLtSucc :: Zero :<: S m
-  SuccLtSucc :: n :<: m -> S n :<: S m
-
-deriving instance Show (a :<: b)
-
---------------------------------------------------
--- * Total orderings on natural numbers.
---------------------------------------------------
-propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m
-propToBoolLeq _ = unsafeCoerce (Dict :: Dict ())
-{-# INLINE propToBoolLeq #-}
-
-boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m
-boolToClassLeq _ = unsafeCoerce (Dict :: Dict ())
-{-# INLINE boolToClassLeq #-}
-
-propToClassLeq :: Leq n m -> LeqInstance n m
-propToClassLeq _ = unsafeCoerce (Dict :: Dict ())
-{-# INLINE propToClassLeq #-}
-
-{-
--- | Below is the "proof" of the correctness of above:
-propToBoolLeq :: Leq n m -> LeqTrueInstance n m
-propToBoolLeq (ZeroLeq _) = Dict
-propToBoolLeq (SuccLeqSucc leq) = case propToBoolLeq leq of Dict -> Dict
-{-# RULES
- "propToBoolLeq/unsafeCoerce" forall (x :: Leq n m) .
-  propToBoolLeq x = unsafeCoerce (Dict :: Dict ()) :: Dict ((n :<<= m) ~ True)
- #-}
-
-boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m
-boolToClassLeq SZ     _      = Dict
-boolToClassLeq (SS n) (SS m) = case boolToClassLeq n m of Dict -> Dict
-boolToClassLeq _ _ = bugInGHC
-{-# RULES
- "boolToClassLeq/unsafeCoerce" forall (n :: SNat n) (m :: SNat m).
-  boolToClassLeq n m = unsafeCoerce (Dict :: Dict ()) :: Dict (n :<= m)
- #-}
-
-propToClassLeq :: Leq n m -> LeqInstance n m
-propToClassLeq (ZeroLeq _) = Dict
-propToClassLeq (SuccLeqSucc leq) = case propToClassLeq leq of Dict -> Dict
-{-# RULES
- "propToClassLeq/unsafeCoerce" forall (x :: Leq n m) .
-  propToClassLeq x = unsafeCoerce (Dict :: Dict ()) :: Dict (n :<= m)
- #-}
--}
-
-type LeqInstance n m = Dict (n :<= m)
+-- | Convert integral numbers into 'Nat'
+intToNat :: (Integral a, Ord a) => a -> Nat
+intToNat 0 = Z
+intToNat n
+    | n < 0     = error "negative integer"
+    | otherwise = S $ intToNat (n P.- 1)
 
-boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m
-boolToPropLeq SZ     m      = ZeroLeq m
-boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m
-boolToPropLeq _      _      = bugInGHC
+-- | Convert 'Nat' into normal integers.
+natToInt :: Integral n => Nat -> n
+natToInt Z     = 0
+natToInt (S n) = natToInt n P.+ 1
 
-leqRhs :: Leq n m -> SNat m
-leqRhs (ZeroLeq m) = m
-leqRhs (SuccLeqSucc leq) = sS $ leqRhs leq
+-- | Convert 'SNat n' into normal integers.
+sNatToInt :: P.Num n => SNat x -> n
+sNatToInt SZ     = 0
+sNatToInt (SS n) = sNatToInt n P.+ 1
 
-leqLhs :: Leq n m -> SNat n
-leqLhs (ZeroLeq _) = sZ
-leqLhs (SuccLeqSucc leq) = sS $ leqLhs leq
+instance Monomorphicable (Sing :: Nat -> *) where
+  type MonomorphicRep (Sing :: Nat -> *) = Int
+  demote  (Monomorphic sn) = sNatToInt sn
+  promote n
+      | n < 0     = error "negative integer!"
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 708
+      | n == 0    = Monomorphic sZ
+      | otherwise = withPolymorhic (n P.- 1) $ \sn -> Monomorphic $ sS sn
+#else
+      | n == 0    = Monomorphic SZ
+      | otherwise = withPolymorhic (n P.- 1) $ \sn -> Monomorphic $ SS sn
+#endif
 
 --------------------------------------------------
 -- * Properties
@@ -222,9 +153,9 @@
 plusZR :: SNat n -> n :+: Z :=: n
 plusZR SZ     = Refl
 plusZR (SS n) =
- start (sS n %+ sZ)
-   =~= sS (n %+ sZ)
-   === sS n          `because` cong' sS (plusZR n)
+ start (SS n %+ SZ)
+   =~= SS (n %+ SZ)
+   === SS n          `because` cong' SS (plusZR n)
 
 eqPreservesS :: n :=: m -> S n :=: S m
 eqPreservesS Refl = Refl
@@ -250,31 +181,31 @@
   start (l %:+ n)
     === n %:+ l   `because` plusCommutative l n
     === m %:+ l   `because` eq
-    === l %:+ m   `because` plusCommutative m l 
+    === l %:+ m   `because` plusCommutative m l
 
 sAndPlusOne :: SNat n -> S n :=: n :+: One
 sAndPlusOne SZ = Refl
 sAndPlusOne (SS n) =
-  start (sS (sS n))
-    === sS (n %+ sOne) `because` cong' sS (sAndPlusOne n)
-    =~= sS n %+ sOne
+  start (SS (SS n))
+    === SS (n %+ sOne) `because` cong' SS (sAndPlusOne n)
+    =~= SS n %+ sOne
 
 plusAssociative :: SNat n -> SNat m -> SNat l
                 -> n :+: (m :+: l) :=: (n :+: m) :+: l
 plusAssociative SZ     _ _ = Refl
 plusAssociative (SS n) m l =
-  start (sS n %+ (m %+ l))
-    =~= sS (n %+ (m %+ l))
-    === sS ((n %+ m) %+ l)  `because` cong' sS (plusAssociative n m l)
-    =~= sS (n %+ m) %+ l
-    =~= (sS n %+ m) %+ l
+  start (SS n %+ (m %+ l))
+    =~= SS (n %+ (m %+ l))
+    === SS ((n %+ m) %+ l)  `because` cong' SS (plusAssociative n m l)
+    =~= SS (n %+ m) %+ l
+    =~= (SS n %+ m) %+ l
 
 plusSR :: SNat n -> SNat m -> S (n :+: m) :=: n :+: S m
 plusSR n m =
-  start (sS (n %+ m))
+  start (SS (n %+ m))
     === (n %+ m) %+ sOne `because` sAndPlusOne (n %+ m)
     === n %+ (m %+ sOne) `because` symmetry (plusAssociative n m sOne)
-    === n %+ sS m        `because` plusCongL n (symmetry $ sAndPlusOne m)
+    === n %+ SS m        `because` plusCongL n (symmetry $ sAndPlusOne m)
 
 plusCongL :: SNat n -> m :=: m' -> n :+ m :=: n :+ m'
 plusCongL _ Refl = Refl
@@ -288,10 +219,10 @@
 succPlusR :: SNat n -> SNat m -> n :+ S m :=: S (n :+ m)
 succPlusR SZ     _ = Refl
 succPlusR (SS n) m =
-  start (sS n %+ sS m)
-    =~= sS (n %+ sS m)
-    === sS (sS (n %+ m)) `because` succCongEq (succPlusR n m)
-    =~= sS (sS n %+ m)
+  start (SS n %+ SS m)
+    =~= SS (n %+ SS m)
+    === SS (SS (n %+ m)) `because` succCongEq (succPlusR n m)
+    =~= SS (SS n %+ m)
 
 minusCongEq :: n :=: m -> SNat l -> n :-: l :=: m :-: l
 minusCongEq Refl _ = Refl
@@ -299,33 +230,33 @@
 minusNilpotent :: SNat n -> n :-: n :=: Zero
 minusNilpotent SZ = Refl
 minusNilpotent (SS n) =
-  start (sS n %:- sS n)
+  start (SS n %:- SS n)
     =~= n %:- n
-    === sZ     `because` minusNilpotent n
+    === SZ     `because` minusNilpotent n
 
 plusCommutative :: SNat n -> SNat m -> n :+: m :=: m :+: n
 plusCommutative SZ SZ     = Refl
 plusCommutative SZ (SS m) =
-  start (sZ %+ sS m)
-    =~= sS m
-    === sS (m %+ sZ) `because` cong' sS (plusCommutative SZ m)
-    =~= sS m %+ sZ
+  start (SZ %+ SS m)
+    =~= SS m
+    === SS (m %+ SZ) `because` cong' SS (plusCommutative SZ m)
+    =~= SS m %+ SZ
 plusCommutative (SS n) m =
-  start (sS n %+ m)
-    =~= sS (n %+ m)
-    === sS (m %+ n)      `because` cong' sS (plusCommutative n m)
+  start (SS n %+ m)
+    =~= SS (n %+ m)
+    === SS (m %+ n)      `because` cong' SS (plusCommutative n m)
     === (m %+ n) %+ sOne `because` sAndPlusOne (m %+ n)
     === m %+ (n %+ sOne) `because` symmetry (plusAssociative m n sOne)
-    === m %+ sS n        `because` plusCongL m (symmetry $ sAndPlusOne n)
+    === m %+ SS n        `because` plusCongL m (symmetry $ sAndPlusOne n)
 
 eqSuccMinus :: ((m :<<= n) ~ True)
             => SNat n -> SNat m -> (S n :-: m) :=: (S (n :-: m))
 eqSuccMinus _      SZ     = Refl
 eqSuccMinus (SS n) (SS m) =
-  start (sS (sS n) %:- sS m)
-    =~= sS n %:- m
-    === sS (n %:- m)       `because` eqSuccMinus n m
-    =~= sS (sS n %:- sS m)
+  start (SS (SS n) %:- SS m)
+    =~= SS n %:- m
+    === SS (n %:- m)       `because` eqSuccMinus n m
+    =~= SS (SS n %:- SS m)
 eqSuccMinus _ _ = bugInGHC
 
 plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n
@@ -364,44 +295,45 @@
 maxComm (SS n) (SS m) = case maxComm n m of Refl -> Refl
 
 maxZR :: SNat n -> Max n Z :=: n
-maxZR n = transitivity (maxComm n sZ) (maxZL n)
+maxZR n = transitivity (maxComm n SZ) (maxZL n)
 
-multPlusDistr :: SNat n -> SNat m -> SNat l -> n :* (m :+ l) :=: n :* m :+ n :* l
+multPlusDistr :: forall n m l. SNat n -> SNat m -> SNat l -> n :* (m :+ l) :=: (n :* m) :+ (n :* l)
 multPlusDistr SZ     _ _ = Refl
-multPlusDistr (SS n) m l = 
-  start (sS n %* (m %+ l))
-    =~= n %* (m %+ l) %+ (m %+ l)
-    === (n %* m) %+ (n %* l) %+ (m %+ l) `because` plusCongR (m %+ l) (multPlusDistr n m l)
+multPlusDistr (SS (n :: SNat n')) m l =
+  start (SS n %* (m %+ l))
+    =~= (n %* (m %+ l)) %+ (m %+ l)
+    === ((n %* m) %+ (n %* l)) %+ (m %+ l)
+        `because` plusCongR (m %+ l) (multPlusDistr n m l :: n' :* (m :+ l) :=: (n' :* m) :+ (n' :* l))
     === (n %* m) %+ (n %* l) %+ (l %+ m) `because` plusCongL ((n %* m) %+ (n %* l)) (plusCommutative m l)
     === n %* m %+ (n %*l %+ (l %+ m))    `because` symmetry (plusAssociative (n %* m) (n %* l) (l %+ m))
     === n %* l %+ (l %+ m) %+ n %* m     `because` plusCommutative (n %* m) (n %*l %+ (l %+ m))
     === (n %* l %+ l) %+ m %+ n %* m     `because` plusCongR (n %* m) (plusAssociative (n %* l) l m)
-    =~= (sS n %* l)   %+ m %+ n %* m
-    === (sS n %* l)   %+ (m %+ (n %* m)) `because` symmetry (plusAssociative (sS n %* l) m (n %* m))
-    === (sS n %* l)   %+ ((n %* m) %+ m) `because` plusCongL (sS n %* l) (plusCommutative m (n %* m))
-    =~= (sS n %* l)   %+ (sS n %* m)
-    === (sS n %* m)   %+ (sS n %* l)     `because` plusCommutative (sS n %* l) (sS n %* m)
+    =~= (SS n %* l)   %+ m %+ n %* m
+    === (SS n %* l)   %+ (m %+ (n %* m)) `because` symmetry (plusAssociative (SS n %* l) m (n %* m))
+    === (SS n %* l)   %+ ((n %* m) %+ m) `because` plusCongL (SS n %* l) (plusCommutative m (n %* m))
+    =~= (SS n %* l)   %+ (SS n %* m)
+    === (SS n %* m)   %+ (SS n %* l)     `because` plusCommutative (SS n %* l) (SS n %* m)
 
-plusMultDistr :: SNat n -> SNat m -> SNat l -> (n :+ m) :* l :=: n :* l :+ m :* l
+plusMultDistr :: SNat n -> SNat m -> SNat l -> (n :+ m) :* l :=: (n :* l) :+ (m :* l)
 plusMultDistr SZ _ _ = Refl
 plusMultDistr (SS n) m l =
   start ((SS n %+ m) %* l)
-    =~= sS (n %+ m) %* l
+    =~= SS (n %+ m) %* l
     =~= (n %+ m) %* l %+ l
     === n %* l  %+  m %* l  %+  l   `because` plusCongR l (plusMultDistr n m l)
     === m %* l  %+  n %* l  %+  l   `because` plusCongR l (plusCommutative (n %* l) (m %* l))
     === m %* l  %+ (n %* l  %+  l)  `because` symmetry (plusAssociative (m %* l) (n %*l) l)
-    =~= m %* l  %+ (sS n %* l)
-    === (sS n %* l)  %+  (m %* l)   `because` plusCommutative (m %* l) (sS n %* l)
+    =~= m %* l  %+ (SS n %* l)
+    === (SS n %* l)  %+  (m %* l)   `because` plusCommutative (m %* l) (SS n %* l)
 
 multAssociative :: SNat n -> SNat m -> SNat l -> n :* (m :* l) :=: (n :* m) :* l
 multAssociative SZ     _ _ = Refl
 multAssociative (SS n) m l =
-  start (sS n %* (m %* l))
+  start (SS n %* (m %* l))
     =~= n %* (m %* l) %+ (m %* l)
     === (n %* m) %* l %+ (m %* l) `because` plusCongR (m %* l) (multAssociative n m l)
     === (n %* m %+ m) %* l        `because` symmetry (plusMultDistr (n %* m) m l)
-    =~= (sS n %* m) %* l
+    =~= (SS n %* m) %* l
 
 multZL :: SNat m -> Zero :* m :=: Zero
 multZL _ = Refl
@@ -409,10 +341,10 @@
 multZR :: SNat m -> m :* Zero :=: Zero
 multZR SZ = Refl
 multZR (SS n) =
-  start (sS n %* sZ)
-    =~= n %* sZ %+ sZ
-    === sZ %+ sZ      `because` plusCongR sZ (multZR n)
-    =~= sZ
+  start (SS n %* SZ)
+    =~= n %* SZ %+ SZ
+    === SZ %+ SZ      `because` plusCongR SZ (multZR n)
+    =~= SZ
 
 multOneL :: SNat n -> One :* n :=: n
 multOneL n =
@@ -424,10 +356,10 @@
 multOneR :: SNat n -> n :* One :=: n
 multOneR SZ = Refl
 multOneR (SS n) =
-  start (sS n %* sOne)
+  start (SS n %* sOne)
     =~= n %* sOne %+ sOne
     === n %+ sOne         `because` plusCongR sOne (multOneR n)
-    === sS n              `because` symmetry (sAndPlusOne n)
+    === SS n              `because` symmetry (sAndPlusOne n)
 
 multCongL :: SNat n -> m :=: l -> n :* m :=: n :* l
 multCongL _ Refl = Refl
@@ -437,22 +369,22 @@
 
 multComm :: SNat n -> SNat m -> n :* m :=: m :* n
 multComm SZ m =
-  start (sZ %* m)
-    =~= sZ
-    === m %* sZ `because` symmetry (multZR m)
+  start (SZ %* m)
+    =~= SZ
+    === m %* SZ `because` symmetry (multZR m)
 multComm (SS n) m =
-  start (sS n %* m)
+  start (SS n %* m)
     =~= n %* m %+ m
     === m %* n %+ m          `because` plusCongR m (multComm n m)
     === m %* n %+ m %* sOne  `because` plusCongL (m %* n) (symmetry $ multOneR m)
     === m %* (n %+ sOne)     `because` symmetry (multPlusDistr m n sOne)
-    === m %* sS n            `because` multCongL m (symmetry $ sAndPlusOne n)
+    === m %* SS n            `because` multCongL m (symmetry $ sAndPlusOne n)
 
 plusNeutralR :: SNat n -> SNat m -> n :+ m :=: n -> m :=: Z
 plusNeutralR SZ m eq =
   start m
-    =~= sZ %:+ m
-    === sZ       `because` eq
+    =~= SZ %:+ m
+    === SZ       `because` eq
 plusNeutralR (SS n) m eq = plusNeutralR n m $ succInjective eq
 
 plusNeutralL :: SNat n -> SNat m -> n :+ m :=: m -> n :=: Z
@@ -466,7 +398,7 @@
 --------------------------------------------------
 
 leqRefl :: SNat n -> Leq n n
-leqRefl SZ = ZeroLeq sZ
+leqRefl SZ = ZeroLeq SZ
 leqRefl (SS n) = SuccLeqSucc $ leqRefl n
 
 leqSucc :: SNat n -> Leq n (S n)
@@ -492,9 +424,9 @@
 plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m)
 plusLeqL SZ     m = ZeroLeq $ coerce (symmetry $ plusZL m) m
 plusLeqL (SS n) m =
-  start (sS n)
-    =<= sS (n %+ m) `because` SuccLeqSucc (plusLeqL n m)
-    =~= sS n %+ m
+  start (SS n)
+    =<= SS (n %+ m) `because` SuccLeqSucc (plusLeqL n m)
+    =~= SS n %+ m
 
 plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m)
 plusLeqR n m =
@@ -502,7 +434,7 @@
     Refl -> plusLeqL m n
 
 minLeqL :: SNat n -> SNat m -> Leq (Min n m) n
-minLeqL SZ m = case zAbsorbsMinL m of Refl -> ZeroLeq sZ
+minLeqL SZ m = case zAbsorbsMinL m of Refl -> ZeroLeq SZ
 minLeqL n SZ = case zAbsorbsMinR n of Refl -> ZeroLeq n
 minLeqL (SS n) (SS m) = SuccLeqSucc (minLeqL n m)
 
@@ -515,7 +447,7 @@
 leqAnitsymmetric _ _ = bugInGHC
 
 maxLeqL :: SNat n -> SNat m -> Leq n (Max n m)
-maxLeqL SZ m = ZeroLeq (sMax sZ m)
+maxLeqL SZ m = ZeroLeq (sMax SZ m)
 maxLeqL n SZ = case maxZR n of
                  Refl -> leqRefl n
 maxLeqL (SS n) (SS m) = SuccLeqSucc $ maxLeqL n m
@@ -533,9 +465,9 @@
 leqSnLeq :: Leq (S n) m -> Leq n m
 leqSnLeq (SuccLeqSucc leq) =
   let n = leqLhs leq
-      m = sS $ leqRhs leq
+      m = SS $ leqRhs leq
   in start n
-       =<= sS n   `because` leqSucc n
+       =<= SS n   `because` leqSucc n
        =<= m      `because` SuccLeqSucc leq
 
 leqPred :: Leq (S n) (S m) -> Leq n m
@@ -546,36 +478,7 @@
   case leqLhs leq of
     SS _ -> leqSnnAbsurd leq
     _    -> bugInGHC "cannot be occured"
-  
---------------------------------------------------
--- * Conversion functions.
---------------------------------------------------
 
--- | Convert integral numbers into 'Nat'
-intToNat :: (Integral a, Ord a) => a -> Nat
-intToNat 0 = Z
-intToNat n
-    | n < 0     = error "negative integer"
-    | otherwise = S $ intToNat (n P.- 1)
-
--- | Convert 'Nat' into normal integers.
-natToInt :: Integral n => Nat -> n
-natToInt Z     = 0
-natToInt (S n) = natToInt n P.+ 1
-
--- | Convert 'SNat n' into normal integers.
-sNatToInt :: P.Num n => SNat x -> n
-sNatToInt SZ     = 0
-sNatToInt (SS n) = sNatToInt n P.+ 1
-
-instance Monomorphicable (Sing :: Nat -> *) where
-  type MonomorphicRep (Sing :: Nat -> *) = Int
-  demote  (Monomorphic sn) = sNatToInt sn
-  promote n
-      | n < 0     = error "negative integer!"
-      | n == 0    = Monomorphic sZ
-      | otherwise = withPolymorhic (n P.- 1) $ \sn -> Monomorphic $ sS sn
-
 --------------------------------------------------
 -- * Quasi Quoter
 --------------------------------------------------
@@ -591,7 +494,7 @@
                   }
 
 -- | Quotesi-quoter for 'SNat'. This can be used for an expression, pattern and type.
--- 
+--
 --  For example: @[snat|12|] '%+' [snat| 5 |]@, @'sing' :: [snat| 12 |]@, @f [snat| 12 |] = \"hey\"@
 snat :: QuasiQuoter
 snat = QuasiQuoter { quoteExp = P.foldr appE (conE 'SZ) . P.flip P.replicate (conE 'SS) . P.read
diff --git a/Data/Type/Natural/Core.hs b/Data/Type/Natural/Core.hs
new file mode 100644
--- /dev/null
+++ b/Data/Type/Natural/Core.hs
@@ -0,0 +1,132 @@
+{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs     #-}
+{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude       #-}
+{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables, StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators                   #-}
+{-# LANGUAGE UndecidableInstances                                           #-}
+module Data.Type.Natural.Core where
+import Data.Singletons
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+import Data.Singletons.Prelude hiding ((:<=), Max, MaxSym0, MaxSym1, MaxSym2,
+                                Min, MinSym0, MinSym1, MinSym2, SOrd (..))
+import Data.Singletons.TH      (singletons)
+#endif
+import           Data.Constraint           hiding ((:-))
+import           Data.Type.Monomorphic
+import           Language.Haskell.TH
+import           Language.Haskell.TH.Quote
+import           Prelude                   (Bool (..), Eq (..), Int,
+                                            Integral (..), Ord ((<)), Show (..),
+                                            error, id, otherwise, undefined,
+                                            ($), (.))
+import qualified Prelude                   as P
+import           Proof.Equational
+import           Unsafe.Coerce
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 710
+import Data.Type.Natural.Definitions hiding ((:<=))
+import Prelude                       (Num (..))
+#else
+import Data.Type.Natural.Definitions
+#endif
+
+
+--------------------------------------------------
+-- ** Convenient synonyms
+--------------------------------------------------
+
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+sZ :: SNat Z
+sZ = SZ
+
+sS :: SNat n -> SNat (S n)
+sS = SS
+
+{-# DEPRECATED sZ, sS "Smart constructors are no longer needed in singletons; Use `SS` or `SZ` instead." #-}
+#endif
+
+--------------------------------------------------
+-- ** Type-level predicate & judgements.
+--------------------------------------------------
+-- | Comparison via type-class.
+class (n :: Nat) :<= (m :: Nat)
+instance Z :<= n
+instance (n :<= m) => S n :<= S m
+
+-- | Comparison via GADTs.
+data Leq (n :: Nat) (m :: Nat) where
+  ZeroLeq     :: SNat m -> Leq Zero m
+  SuccLeqSucc :: Leq n m -> Leq (S n) (S m)
+
+type LeqTrueInstance a b = Dict ((a :<<= b) ~ True)
+
+(%-) :: (m :<<= n) ~ True => SNat n -> SNat m -> SNat (n :-: m)
+n   %- SZ    = n
+SS n %- SS m = n %- m
+_    %- _    = error "impossible!"
+
+infixl 6 %-
+deriving instance Show (SNat n)
+deriving instance Eq (SNat n)
+
+data (a :: Nat) :<: (b :: Nat) where
+  ZeroLtSucc :: Zero :<: S m
+  SuccLtSucc :: n :<: m -> S n :<: S m
+
+deriving instance Show (a :<: b)
+
+--------------------------------------------------
+-- * Total orderings on natural numbers.
+--------------------------------------------------
+propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m
+propToBoolLeq _ = unsafeCoerce (Dict :: Dict ())
+{-# INLINE propToBoolLeq #-}
+
+boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m
+boolToClassLeq _ = unsafeCoerce (Dict :: Dict ())
+{-# INLINE boolToClassLeq #-}
+
+propToClassLeq :: Leq n m -> LeqInstance n m
+propToClassLeq _ = unsafeCoerce (Dict :: Dict ())
+{-# INLINE propToClassLeq #-}
+
+{-
+-- | Below is the "proof" of the correctness of above:
+propToBoolLeq :: Leq n m -> LeqTrueInstance n m
+propToBoolLeq (ZeroLeq _) = Dict
+propToBoolLeq (SuccLeqSucc leq) = case propToBoolLeq leq of Dict -> Dict
+{-# RULES
+ "propToBoolLeq/unsafeCoerce" forall (x :: Leq n m) .
+  propToBoolLeq x = unsafeCoerce (Dict :: Dict ()) :: Dict ((n :<<= m) ~ True)
+ #-}
+
+boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m
+boolToClassLeq SZ     _      = Dict
+boolToClassLeq (SS n) (SS m) = case boolToClassLeq n m of Dict -> Dict
+boolToClassLeq _ _ = bugInGHC
+{-# RULES
+ "boolToClassLeq/unsafeCoerce" forall (n :: SNat n) (m :: SNat m).
+  boolToClassLeq n m = unsafeCoerce (Dict :: Dict ()) :: Dict (n :<= m)
+ #-}
+
+propToClassLeq :: Leq n m -> LeqInstance n m
+propToClassLeq (ZeroLeq _) = Dict
+propToClassLeq (SuccLeqSucc leq) = case propToClassLeq leq of Dict -> Dict
+{-# RULES
+ "propToClassLeq/unsafeCoerce" forall (x :: Leq n m) .
+  propToClassLeq x = unsafeCoerce (Dict :: Dict ()) :: Dict (n :<= m)
+ #-}
+-}
+
+type LeqInstance n m = Dict (n :<= m)
+
+boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m
+boolToPropLeq SZ     m      = ZeroLeq m
+boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m
+boolToPropLeq _      _      = bugInGHC
+
+leqRhs :: Leq n m -> SNat m
+leqRhs (ZeroLeq m) = m
+leqRhs (SuccLeqSucc leq) = sS $ leqRhs leq
+
+leqLhs :: Leq n m -> SNat n
+leqLhs (ZeroLeq _) = sZ
+leqLhs (SuccLeqSucc leq) = sS $ leqLhs leq
diff --git a/Data/Type/Natural/Definitions.hs b/Data/Type/Natural/Definitions.hs
--- a/Data/Type/Natural/Definitions.hs
+++ b/Data/Type/Natural/Definitions.hs
@@ -4,12 +4,26 @@
 {-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving  #-}
 {-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators         #-}
 {-# LANGUAGE UndecidableInstances                                 #-}
-module Data.Type.Natural.Definitions where
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ > 708
+{-# LANGUAGE InstanceSigs #-}
+#endif
+module Data.Type.Natural.Definitions
+       (module Data.Type.Natural.Definitions,
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 710
+        module Data.Singletons.Prelude
+#endif
+       ) where
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+import Data.Singletons.TH (singletons)
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 710
+import Data.Singletons.Prelude
+import Prelude                 (Num (..), Ord (..))
+#else
 import Data.Singletons.Prelude hiding ((:<=), Max, MaxSym0, MaxSym1, MaxSym2,
                                 Min, MinSym0, MinSym1, MinSym2, SOrd (..))
-import Data.Singletons.TH      (singletons)
 #endif
+import Data.Singletons.TH (singletons)
+#endif
 import           Data.Constraint           hiding ((:-))
 import           Data.Type.Monomorphic
 import           Data.Typeable             (Typeable)
@@ -28,7 +42,7 @@
 --------------------------------------------------
 singletons [d|
  data Nat = Z | S Nat
-            deriving (Show, Eq, Ord)
+            deriving (Show, Eq)
  |]
 
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
@@ -40,6 +54,7 @@
 -- ** Arithmetic functions.
 --------------------------------------------------
 
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 710
 singletons [d|
  -- | Minimum function.
  min :: Nat -> Nat -> Nat
@@ -56,7 +71,54 @@
  max (S n) (S m) = S (max n m)
  |]
 
+instance P.Ord Nat where
+  Z   <= _   = True
+  S _ <= Z   = False
+  S n <= S m = n P.<= m
+
+  min = min
+  max = max
+#else
 singletons [d|
+  instance P.Ord Nat where
+     Z   <= _   = True
+     S _ <= Z   = False
+     S n <= S m = n <= m
+
+     min Z     Z     = Z
+     min Z     (S _) = Z
+     min (S _) Z     = Z
+     min (S m) (S n) = S (min m n)
+
+     max Z     Z     = Z
+     max Z     (S n) = S n
+     max (S n) Z     = S n
+     max (S n) (S m) = S (max n m)
+ |]
+#endif
+
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 710
+singletons [d|
+  instance P.Num Nat where
+    Z   + n = n
+    S m + n = S (m + n)
+
+    n   - Z   = n
+    S n - S m = n - m
+    Z   - S _ = Z
+
+    Z   * _ = Z
+    S n * m = n * m + m
+
+    abs n = n
+
+    signum Z = Z
+    signum (S n) = S Z
+
+    fromInteger n = if n == 0 then Z else S (fromInteger (n-1))
+ |]
+#else
+singletons [d|
  (+) :: Nat -> Nat -> Nat
  Z   + n = n
  S m + n = S (m + n)
@@ -69,31 +131,52 @@
  (*) :: Nat -> Nat -> Nat
  Z   * _ = Z
  S n * m = n * m + m
+ |]
 
+infixl 6 %:-, -
+
+infixl 6 %:+, :+
+
+infixl 7 %:*, :*
+
+instance P.Num Nat where
+  n - m = n - m
+  n + m = n + m
+  n * m = n * m
+  abs = id
+  signum Z = Z
+  signum _ = S Z
+  fromInteger 0             = Z
+  fromInteger n | n P.< 0   = error "negative integer"
+                | otherwise = S $ P.fromInteger (n P.- 1)
+
+#endif
+
+type n :-: m = n :- m
+type n :+: m = n :+ m
+
+infixl 6 :-:, :+:
+
+singletons [d|
  (**) :: Nat -> Nat -> Nat
  n ** Z = S Z
  n ** S m = (n ** m) * n
  |]
 
-infixl 6 :-:, %:-, -
 
-type n :-: m = n :- m
-infixl 6 :+:, %+, %:+, :+
-
-type n :+: m = n :+ m
-
 -- | Addition for singleton numbers.
 (%+) :: SNat n -> SNat m -> SNat (n :+: m)
 (%+) = (%:+)
-
-infixl 7 :*:, %*, %:*, :*
+infixl 6 %+
 
 -- | Type-level multiplication.
 type n :*: m = n :* m
+infixl 7 :*:
 
 -- | Multiplication for singleton numbers.
 (%*) :: SNat n -> SNat m -> SNat (n :*: m)
 (%*) = (%:*)
+infixl 7 %*
 
 -- | Type-level exponentiation.
 type n :**: m = n :** m
diff --git a/type-natural.cabal b/type-natural.cabal
--- a/type-natural.cabal
+++ b/type-natural.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                type-natural
-version:             0.2.3.2
+version:             0.3.0.0
 synopsis:            Type-level natural and proofs of their properties.
 description:         Type-level natural numbers and proofs of their properties.
 homepage:            https://github.com/konn/type-natural
@@ -14,6 +14,9 @@
 category:            Math
 build-type:          Simple
 cabal-version:       >=1.8
+tested-with:         GHC == 7.8.3, GHC == 7.8.4,
+                     GHC == 7.10.2
+
 source-repository head
   Type: git
   Location: git://github.com/konn/type-natural.git
@@ -21,7 +24,8 @@
 
 library
   exposed-modules:     Data.Type.Natural, Data.Type.Ordinal
-  other-modules:       Data.Type.Natural.Definitions
+  other-modules:       Data.Type.Natural.Definitions,
+                       Data.Type.Natural.Core
   build-depends:       base                     >= 4       && < 5
                ,       equational-reasoning     == 0.2.*
                ,       monomorphic              >= 0.0.3
@@ -30,4 +34,7 @@
   if impl(ghc < 7.8)
     build-depends:     singletons               == 0.8.*
   else
-    build-depends:     singletons               >= 1.0    && < 1.2
+    if impl(ghc < 7.10)
+      build-depends:     singletons               == 1.*
+    else 
+      build-depends:     singletons               == 2.0.*