diff --git a/Data/Type/Natural/Builtin.hs b/Data/Type/Natural/Builtin.hs
--- a/Data/Type/Natural/Builtin.hs
+++ b/Data/Type/Natural/Builtin.hs
@@ -263,7 +263,7 @@
   case sn %~ (sing :: Sing 0) of
     Proved eql -> withRefl eql Refl
     Disproved nPos -> case sm %~ (sing :: Sing 0) of
-      Proved _ -> absurd $ nPos $ natLeqZero sn
+      Proved mEq0 -> withRefl mEq0 $ absurd $ nPos $ natLeqZero sn
       Disproved mPos ->
         let pn = sPred sn
             pm = sPred sm
diff --git a/type-natural.cabal b/type-natural.cabal
--- a/type-natural.cabal
+++ b/type-natural.cabal
@@ -1,64 +1,57 @@
--- Initial type-natural.cabal generated by cabal init.  For further 
--- documentation, see http://haskell.org/cabal/users-guide/
-
-name:                type-natural
-version:             0.7.1.1
-synopsis:            Type-level natural and proofs of their properties.
-description:         Type-level natural numbers and proofs of their properties.
-                     .
-                     Version 0.6+ supports __GHC 8+ only__.
-                     .
-                     __Use 0.5.* with ~ GHC 7.10.3__.
-homepage:            https://github.com/konn/type-natural
-license:             BSD3
-license-file:        LICENSE
-author:              Hiromi ISHII
-maintainer:          konn.jinro_at_gmail.com
-copyright:           (C) Hiromi ISHII 2013-2014
-category:            Math
-build-type:          Simple
-cabal-version:       >= 1.10
-tested-with:         GHC == 7.10.3
+name: type-natural
+version: 0.7.1.2
+cabal-version: >=1.10
+build-type: Simple
+license: BSD3
+license-file: LICENSE
+copyright: (C) Hiromi ISHII 2013-2014
+maintainer: konn.jinro_at_gmail.com
+homepage: https://github.com/konn/type-natural
+synopsis: Type-level natural and proofs of their properties.
+description:
+    Type-level natural numbers and proofs of their properties.
+    .
+    Version 0.6+ supports __GHC 8+ only__.
+    .
+    __Use 0.5.* with ~ GHC 7.10.3__.
+category: Math
+author: Hiromi ISHII
+tested-with: GHC ==7.10.3
 
 source-repository head
-  Type: git
-  Location: git://github.com/konn/type-natural.git
-
+    type: git
+    location: git://github.com/konn/type-natural.git
 
 library
-  ghc-options:         -Wall -O2 -fno-warn-orphans
-  if impl(ghc >= 8.0.0)
-    ghc-options:       -Wno-redundant-constraints
-  exposed-modules:     Data.Type.Natural
-                     , Data.Type.Ordinal
-                     , Data.Type.Ordinal.Builtin
-                     , Data.Type.Ordinal.Peano
-                     , Data.Type.Natural.Builtin
-                     , Data.Type.Natural.Class
-                     , Data.Type.Natural.Class.Arithmetic
-                     , Data.Type.Natural.Class.Order
-  other-modules:       Data.Type.Natural.Definitions
-                     , Data.Type.Natural.Core
-                     , Data.Type.Natural.Compat
-  build-depends:       base                      >= 4       && < 5
-                     , equational-reasoning      >= 0.4.1.1 && < 1
-                     , monomorphic               >= 0.0.3
-                     , template-haskell          >= 2.8     && < 3
-                     , constraints               >= 0.3     && < 0.9
-                     , ghc-typelits-natnormalise == 0.4.*
-                     , ghc-typelits-presburger   >= 0.1.1   && < 1
-                     , singletons                == 2.2.*
+    
+    if impl(ghc >=8.0.0)
+        ghc-options: -Wno-redundant-constraints
+    exposed-modules:
+        Data.Type.Natural
+        Data.Type.Ordinal
+        Data.Type.Ordinal.Builtin
+        Data.Type.Ordinal.Peano
+        Data.Type.Natural.Builtin
+        Data.Type.Natural.Class
+        Data.Type.Natural.Class.Arithmetic
+        Data.Type.Natural.Class.Order
+    build-depends:
+        base ==4.*,
+        equational-reasoning >=0.4.1.1 && <1,
+        monomorphic >=0.0.3 && <0.1,
+        template-haskell >=2.8 && <3,
+        constraints >=0.3 && <0.9,
+        ghc-typelits-natnormalise >=0.4 && <0.6,
+        ghc-typelits-presburger >=0.1.1 && <1,
+        singletons ==2.2.*
+    default-language: Haskell2010
+    default-extensions: DataKinds PolyKinds ConstraintKinds GADTs
+                        ScopedTypeVariables TemplateHaskell TypeFamilies TypeOperators
+                        MultiParamTypeClasses UndecidableInstances FlexibleContexts
+                        FlexibleInstances
+    other-modules:
+        Data.Type.Natural.Definitions
+        Data.Type.Natural.Core
+        Data.Type.Natural.Compat
+    ghc-options: -Wall -O2 -fno-warn-orphans
 
-  default-language:    Haskell2010
-  default-extensions:  DataKinds
-                       PolyKinds
-                       ConstraintKinds
-                       GADTs
-                       ScopedTypeVariables
-                       TemplateHaskell
-                       TypeFamilies
-                       TypeOperators
-                       MultiParamTypeClasses
-                       UndecidableInstances
-                       FlexibleContexts
-                       FlexibleInstances