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,7 @@
-{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs    #-}
-{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude #-}
-{-# LANGUAGE PolyKinds, RankNTypes, TemplateHaskell, TypeFamilies     #-}
-{-# LANGUAGE TypeOperators, UndecidableInstances, StandaloneDeriving  #-}
+{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}
+{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude   #-}
+{-# LANGUAGE PolyKinds, RankNTypes, TemplateHaskell, TypeFamilies       #-}
+{-# LANGUAGE TypeOperators, UndecidableInstances, StandaloneDeriving    #-}
 -- | Type level peano natural number, some arithmetic functions and their singletons.
 module Data.Type.Natural (-- * Re-exported modules.
                           module Data.Singletons,
@@ -11,13 +11,15 @@
                           -- | Singleton type for 'Nat'.
                           SNat, Sing (SZ, SS),
                           -- ** Smart constructors
+                          -- | WARNING: Smart constructors are deprecated as of singletons 0.10,
+                          -- so these are provided only for backward compatibility.
                           sZ, sS,
                           -- ** Arithmetic functions and their singletons.
                           min, Min, sMin, max, Max, sMax,
                           (:+:), (:+), (%+), (%:+), (:*:), (:*), (%:*), (%*),
                           (:-:), (:-), (%:-), (%-),
                           -- ** Type-level predicate & judgements
-                          Leq(..), (:<=), (:<<=), (%:<<=), LeqInstance, leqRefl, leqSucc,
+                          Leq(..), (:<=), (:<<=), (%:<<=), LeqInstance,
                           boolToPropLeq, boolToClassLeq, propToClassLeq,
                           LeqTrueInstance, propToBoolLeq,
                           -- * Conversion functions
@@ -27,13 +29,17 @@
                           -- * Properties of natural numbers
                           succCongEq, plusCongR, plusCongL, succPlusL, succPlusR,
                           plusZR, plusZL, eqPreservesS, plusAssociative,
-                          multAssociative, multComm, multZL, multZR, multOneL, multOneR,
+                          multAssociative, multComm, multZL, multZR, multOneL,
+                          multOneR, snEqZAbsurd, succInjective, plusInjectiveL, plusInjectiveR,
                           plusMultDistr, multPlusDistr, multCongL, multCongR,
                           sAndPlusOne, plusCommutative, minusCongEq, minusNilpotent,
-                          eqSuccMinus, plusMinusEqL, plusMinusEqR, plusLeqL, plusLeqR,
-                          zAbsorbsMinR, zAbsorbsMinL, minLeqL, minLeqR, plusSR,
-                          leqRhs, leqLhs, leqTrans, minComm, leqAnitsymmetric,
-                          maxZL, maxComm, maxZR, maxLeqL, maxLeqR, plusMonotone,
+                          eqSuccMinus, plusMinusEqL, plusMinusEqR,
+                          zAbsorbsMinR, zAbsorbsMinL, plusSR, plusNeutralR, plusNeutralL,
+                          leqRhs, leqLhs, minComm, maxZL, maxComm, maxZR,
+                          -- * Properties of ordering 'Leq'
+                          leqRefl, leqSucc, leqTrans, plusMonotone, plusLeqL, plusLeqR,
+                          minLeqL, minLeqR, leqAnitsymmetric, maxLeqL, maxLeqR,
+                          leqSnZAbsurd, leqnZElim, leqSnLeq, leqPred, leqSnnAbsurd,
                           -- * Useful type synonyms and constructors
                           zero, one, two, three, four, five, six, seven, eight, nine, ten, eleven,
                           twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty,
@@ -47,6 +53,9 @@
                           sN15, sN16, sN17, sN18, sN19, sN20
                          ) where
 import           Data.Singletons
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+import Data.Singletons.TH
+#endif
 import           Data.Type.Monomorphic
 import           Prelude          (Int, Bool (..), Eq (..), Integral (..), Ord ((<)),
                                    Show (..), error, id, otherwise, ($), (.), undefined)
@@ -184,6 +193,17 @@
  n20 = twenty
  |]
 
+#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.
 --------------------------------------------------
@@ -272,14 +292,6 @@
 boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m
 boolToPropLeq _      _      = bugInGHC
 
-leqRefl :: SNat n -> Leq n n
-leqRefl SZ = ZeroLeq sZ
-leqRefl (SS n) = SuccLeqSucc $ leqRefl n
-
-leqSucc :: SNat n -> Leq n (S n)
-leqSucc SZ = ZeroLeq sOne
-leqSucc (SS n) = SuccLeqSucc $ leqSucc n
-
 leqRhs :: Leq n m -> SNat m
 leqRhs (ZeroLeq m) = m
 leqRhs (SuccLeqSucc leq) = sS $ leqRhs leq
@@ -288,15 +300,6 @@
 leqLhs (ZeroLeq _) = sZ
 leqLhs (SuccLeqSucc leq) = sS $ leqLhs leq
 
-leqTrans :: Leq n m -> Leq m l -> Leq n l
-leqTrans (ZeroLeq _) leq = ZeroLeq $ leqRhs leq
-leqTrans (SuccLeqSucc nLeqm) (SuccLeqSucc mLeql) = SuccLeqSucc $ leqTrans nLeqm mLeql
-leqTrans _ _ = error "impossible!"
-
-instance Preorder Leq where
-  reflexivity = leqRefl
-  transitivity = leqTrans
-
 --------------------------------------------------
 -- * Properties
 --------------------------------------------------
@@ -316,6 +319,23 @@
 succCongEq :: n :=: m -> S n :=: S m
 succCongEq Refl = Refl
 
+snEqZAbsurd :: S n :=: Z -> a
+snEqZAbsurd _ = bugInGHC "impossible!"
+
+succInjective :: S n :=: S m -> n :=: m
+succInjective Refl = Refl
+
+plusInjectiveL :: SNat n -> SNat m -> SNat l -> n :+ m :=: n :+ l -> m :=: l
+plusInjectiveL SZ     _ _ Refl = Refl
+plusInjectiveL (SS n) m l eq   = plusInjectiveL n m l $ succInjective eq
+
+plusInjectiveR :: SNat n -> SNat m -> SNat l -> n :+ l :=: m :+ l -> n :=: m
+plusInjectiveR n m l eq = plusInjectiveL l n m $
+  start (l %:+ n)
+    === n %:+ l   `because` plusCommutative l n
+    === m %:+ l   `because` eq
+    === l %:+ m   `because` plusCommutative m l 
+
 sAndPlusOne :: SNat n -> S n :=: n :+: One
 sAndPlusOne SZ = Refl
 sAndPlusOne (SS n) =
@@ -340,13 +360,6 @@
     === n %+ (m %+ sOne) `because` symmetry (plusAssociative n m sOne)
     === n %+ sS m        `because` plusCongL n (symmetry $ sAndPlusOne m)
 
-plusMonotone :: Leq n m -> Leq l k -> Leq (n :+: l) (m :+: k)
-plusMonotone (ZeroLeq m) (ZeroLeq k) = ZeroLeq (m %+ k)
-plusMonotone (ZeroLeq m) (SuccLeqSucc leq) =
-  case plusSR m (leqRhs leq) of
-    Refl -> SuccLeqSucc $ plusMonotone (ZeroLeq m) leq
-plusMonotone (SuccLeqSucc leq) leq' = SuccLeqSucc $ plusMonotone leq leq'
-
 plusCongL :: SNat n -> m :=: m' -> n :+ m :=: n :+ m'
 plusCongL _ Refl = Refl
 
@@ -399,15 +412,6 @@
     =~= sS (sS n %:- sS m)
 eqSuccMinus _ _ = bugInGHC
 
-plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m)
-plusLeqL SZ     m = case plusZR m of Refl -> ZeroLeq m
-plusLeqL (SS n) m = SuccLeqSucc $ plusLeqL n m
-
-plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m)
-plusLeqR n m =
-  case plusCommutative n m of
-    Refl -> plusLeqL m n
-
 plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n
 plusMinusEqL SZ     m = minusNilpotent m
 plusMinusEqL (SS n) m =
@@ -427,25 +431,12 @@
 zAbsorbsMinL SZ     = Refl
 zAbsorbsMinL (SS n) = case zAbsorbsMinL n of Refl -> Refl
 
-minLeqL :: SNat n -> SNat m -> Leq (Min n m) n
-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)
-
-minLeqR :: SNat n -> SNat m -> Leq (Min n m) m
-minLeqR n m = case minComm n m of Refl -> minLeqL m n
-
 minComm :: SNat n -> SNat m -> Min n m :=: Min m n
 minComm SZ     SZ = Refl
 minComm SZ     (SS _) = Refl
 minComm (SS _) SZ = Refl
 minComm (SS n) (SS m) = case minComm n m of Refl -> Refl
 
-leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m
-leqAnitsymmetric (ZeroLeq _) (ZeroLeq _) = Refl
-leqAnitsymmetric (SuccLeqSucc leq1) (SuccLeqSucc leq2) = eqPreservesS $ leqAnitsymmetric leq1 leq2
-leqAnitsymmetric _ _ = bugInGHC
-
 maxZL :: SNat n -> Max Z n :=: n
 maxZL SZ = Refl
 maxZL (SS _) = Refl
@@ -459,24 +450,6 @@
 maxZR :: SNat n -> Max n Z :=: n
 maxZR n = transitivity (maxComm n sZ) (maxZL n)
 
-maxLeqL :: SNat n -> SNat m -> Leq n (Max n 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
-
-maxLeqR :: SNat n -> SNat m -> Leq m (Max n m)
-maxLeqR n m = case maxComm n m of
-                Refl -> maxLeqL m n
-
-newtype MultPlusDistr l m n =
-    MultPlusDistr { unMultPlusDistr :: l :* (m :+ n) :=: l :* m :+ l :* n}
-
-instance Proposition (MultPlusDistr l m) where
-  type OriginalProp (MultPlusDistr l m) n = l :* (m :+ n) :=: l :* m :+ l :* n
-  wrap = MultPlusDistr
-  unWrap = unMultPlusDistr
-
 multPlusDistr :: SNat n -> SNat m -> SNat l -> n :* (m :+ l) :=: n :* m :+ n :* l
 multPlusDistr SZ     _ _ = Refl
 multPlusDistr (SS n) m l = 
@@ -559,6 +532,105 @@
     === m %* (n %+ sOne)     `because` symmetry (multPlusDistr m n sOne)
     === 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
+plusNeutralR (SS n) m eq = plusNeutralR n m $ succInjective eq
+
+plusNeutralL :: SNat n -> SNat m -> n :+ m :=: m -> n :=: Z
+plusNeutralL n m eq = plusNeutralR m n $
+  start (m %:+ n)
+    === n %:+ m   `because` plusCommutative m n
+    === m         `because` eq
+
+--------------------------------------------------
+-- * Properties of 'Leq'
+--------------------------------------------------
+
+leqRefl :: SNat n -> Leq n n
+leqRefl SZ = ZeroLeq sZ
+leqRefl (SS n) = SuccLeqSucc $ leqRefl n
+
+leqSucc :: SNat n -> Leq n (S n)
+leqSucc SZ = ZeroLeq sOne
+leqSucc (SS n) = SuccLeqSucc $ leqSucc n
+
+leqTrans :: Leq n m -> Leq m l -> Leq n l
+leqTrans (ZeroLeq _) leq = ZeroLeq $ leqRhs leq
+leqTrans (SuccLeqSucc nLeqm) (SuccLeqSucc mLeql) = SuccLeqSucc $ leqTrans nLeqm mLeql
+leqTrans _ _ = error "impossible!"
+
+instance Preorder Leq where
+  reflexivity = leqRefl
+  transitivity = leqTrans
+
+plusMonotone :: Leq n m -> Leq l k -> Leq (n :+: l) (m :+: k)
+plusMonotone (ZeroLeq m) (ZeroLeq k) = ZeroLeq (m %+ k)
+plusMonotone (ZeroLeq m) (SuccLeqSucc leq) =
+  case plusSR m (leqRhs leq) of
+    Refl -> SuccLeqSucc $ plusMonotone (ZeroLeq m) leq
+plusMonotone (SuccLeqSucc leq) leq' = SuccLeqSucc $ plusMonotone leq leq'
+
+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
+
+plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m)
+plusLeqR n m =
+  case plusCommutative n m of
+    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 n SZ = case zAbsorbsMinR n of Refl -> ZeroLeq n
+minLeqL (SS n) (SS m) = SuccLeqSucc (minLeqL n m)
+
+minLeqR :: SNat n -> SNat m -> Leq (Min n m) m
+minLeqR n m = case minComm n m of Refl -> minLeqL m n
+
+leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m
+leqAnitsymmetric (ZeroLeq _) (ZeroLeq _) = Refl
+leqAnitsymmetric (SuccLeqSucc leq1) (SuccLeqSucc leq2) = eqPreservesS $ leqAnitsymmetric leq1 leq2
+leqAnitsymmetric _ _ = bugInGHC
+
+maxLeqL :: SNat n -> SNat m -> Leq n (Max n 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
+
+maxLeqR :: SNat n -> SNat m -> Leq m (Max n m)
+maxLeqR n m = case maxComm n m of
+                Refl -> maxLeqL m n
+
+leqSnZAbsurd :: Leq (S n) Z -> a
+leqSnZAbsurd _ = error "cannot be occured"
+
+leqnZElim :: Leq n Z -> n :=: Z
+leqnZElim (ZeroLeq SZ) = Refl
+
+leqSnLeq :: Leq (S n) m -> Leq n m
+leqSnLeq (SuccLeqSucc leq) =
+  let n = leqLhs leq
+      m = sS $ leqRhs leq
+  in start n
+       =<= sS n   `because` leqSucc n
+       =<= m      `because` SuccLeqSucc leq
+
+leqPred :: Leq (S n) (S m) -> Leq n m
+leqPred (SuccLeqSucc leq) = leq
+
+leqSnnAbsurd :: Leq (S n) n -> a
+leqSnnAbsurd (SuccLeqSucc leq) =
+  case leqLhs leq of
+    SS _ -> leqSnnAbsurd leq
+    _    -> bugInGHC "cannot be occured"
+  
 --------------------------------------------------
 -- * Conversion functions.
 --------------------------------------------------
diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs
--- a/Data/Type/Ordinal.hs
+++ b/Data/Type/Ordinal.hs
@@ -1,7 +1,7 @@
-{-# LANGUAGE DataKinds, EmptyDataDecls, FlexibleContexts, FlexibleInstances #-}
-{-# LANGUAGE ScopedTypeVariables, TemplateHaskell #-}
-{-# LANGUAGE GADTs, KindSignatures, PolyKinds, StandaloneDeriving           #-}
-{-# LANGUAGE TypeFamilies, TypeOperators                                    #-}
+{-# LANGUAGE CPP, DataKinds, EmptyDataDecls, FlexibleContexts         #-}
+{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures, PolyKinds      #-}
+{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies, TypeOperators                              #-}
 -- | Set-theoretic ordinal arithmetic
 module Data.Type.Ordinal
        ( -- * Data-types
@@ -15,13 +15,16 @@
          -- * Quasi Quote
          od
        ) where
+import Data.Constraint
 import Data.Type.Monomorphic
-import Unsafe.Coerce
-import Language.Haskell.TH.Quote
+import Data.Type.Natural         hiding (promote)
 import Language.Haskell.TH
-import Data.Type.Natural hiding (promote)
-import Proof.Equational (coerce)
-import Data.Constraint
+import Language.Haskell.TH.Quote
+import Proof.Equational          (coerce)
+import Unsafe.Coerce
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
+import Data.Singletons.Prelude
+#endif
 
 -- | Set-theoretic (finite) ordinals:
 --
@@ -36,7 +39,7 @@
 instance Read (Ordinal Z) where
   readsPrec _ _ = []
 
-instance SingRep n => Num (Ordinal n) where
+instance SingI n => Num (Ordinal n) where
   _ + _ = error "Finite ordinal is not closed under addition."
   _ - _ = error "Ordinal subtraction is not defined"
   negate OZ = OZ
@@ -53,33 +56,33 @@
 deriving instance Eq (Ordinal n)
 deriving instance Ord (Ordinal n)
 
-instance SingRep n => Enum (Ordinal n) where
+instance SingI n => Enum (Ordinal n) where
   fromEnum = ordToInt
   toEnum   = unsafeFromInt
   enumFrom = enumFromOrd
   enumFromTo = enumFromToOrd
 
-enumFromToOrd :: forall n. SingRep n => Ordinal n -> Ordinal n -> [Ordinal n]
+enumFromToOrd :: forall n. SingI n => Ordinal n -> Ordinal n -> [Ordinal n]
 enumFromToOrd ok ol =
   let k = ordToInt ok
       l = ordToInt ol
   in take (l - k + 1) $ enumFromOrd ok
 
-enumFromOrd :: forall n. SingRep n => Ordinal n -> [Ordinal n]
+enumFromOrd :: forall n. SingI n => Ordinal n -> [Ordinal n]
 enumFromOrd ord = drop (ordToInt ord) $ enumOrdinal (sing :: SNat n)
 
 enumOrdinal :: SNat n -> [Ordinal n]
 enumOrdinal SZ = []
 enumOrdinal (SS n) = OZ : map OS (enumOrdinal n)
 
-instance SingRep n => Bounded (Ordinal (S n)) where
+instance SingI n => Bounded (Ordinal (S n)) where
   minBound = OZ
   maxBound =
     case propToBoolLeq $ leqRefl (sing :: SNat n) of
       Dict -> sNatToOrd (sing :: SNat n)
 
-unsafeFromInt :: forall n. SingRep n => Int -> Ordinal n
-unsafeFromInt n = 
+unsafeFromInt :: forall n. SingI n => Int -> Ordinal n
+unsafeFromInt n =
     case promote n of
       Monomorphic sn ->
         case sS sn %:<<= (sing :: SNat n) of
@@ -93,7 +96,7 @@
 sNatToOrd' _ _ = bugInGHC
 
 -- | 'sNatToOrd'' with @n@ inferred.
-sNatToOrd :: (SingRep n, (S m :<<= n) ~ True) => SNat m -> Ordinal n
+sNatToOrd :: (SingI n, (S m :<<= n) ~ True) => SNat m -> Ordinal n
 sNatToOrd = sNatToOrd' sing
 
 data CastedOrdinal n where
@@ -139,7 +142,7 @@
 {-# INLINE inclusion #-}
 
 -- | Ordinal addition.
-(@+) :: forall n m. (SingRep n, SingRep m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)
+(@+) :: forall n m. (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)
 OZ @+ n =
   let sn = sing :: SNat n
       sm = sing :: SNat 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.0.0
+version:             0.2.1.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
@@ -22,9 +22,12 @@
 library
   exposed-modules:     Data.Type.Natural, Data.Type.Ordinal
   -- other-modules:       
-  build-depends:       base                     == 4.6.*
-               ,       singletons               == 0.8.*
-               ,       equational-reasoning     == 0.0.*
+  build-depends:       base                     >= 4       && < 5
+               ,       equational-reasoning     == 0.2.*
                ,       monomorphic              >= 0.0.3
-               ,       template-haskell         == 2.8.*
+               ,       template-haskell         >= 2.8     && < 2.11
                ,       constraints              == 0.3.*
+  if impl(ghc < 7.8)
+    build-depends:     singletons               == 0.8.*
+  else
+    build-depends:     singletons               >= 0.10    && < 0.11