diff --git a/Data/Nat.hs b/Data/Nat.hs
--- a/Data/Nat.hs
+++ b/Data/Nat.hs
@@ -1,60 +1,78 @@
 {-# LANGUAGE
   UndecidableInstances, ScopedTypeVariables, DataKinds,
   FlexibleInstances, GADTs, TypeFamilies, TemplateHaskell,
-  TypeOperators #-}
+  InstanceSigs, TypeOperators, PolyKinds #-}
 
 module Data.Nat (
     Nat(..)
+  , NatPlus
+  , NatMul
+  , NatMinus
+  , NatAbs
   , natPlus
   , natMul
+  , natMinus
+  , natAbs
   , SNat
-  , Data.Singletons.Prelude.Sing(SS, SZ)    
-  , (:*)
-  , (:*$)
-  , (:*$$)
-  , (:+)    
-  , (:+$)
-  , (:+$$)
+  , Data.Singletons.Prelude.Sing(SS, SZ)
+  , Data.Singletons.Prelude.PNum
+  , Data.Singletons.Prelude.SNum    
   , SSym0(..)
   , SSym1(..)
   , ZSym0(..)
-  , (%:+)
-  , (%:*)
   , Lit
   , SLit ) where
 
 import Data.Singletons.TH
 import Data.Singletons.Prelude
-import qualified GHC.TypeLits as Lit
+import Unsafe.Coerce
+import qualified GHC.TypeLits as Lit  
 
 $(singletons [d|
   data Nat = Z | S Nat deriving (Eq, Show, Ord)
 
-  (+) :: Nat -> Nat -> Nat
-  Z + b = b
-  S a + b = S (a + b)
+  natPlus :: Nat -> Nat -> Nat
+  natPlus Z     b = b
+  natPlus (S a) b = S (natPlus a b)
 
-  (*) :: Nat -> Nat -> Nat
-  Z * b = Z
-  S a * b = b + (a * b) |])
+  natMul :: Nat -> Nat -> Nat
+  natMul Z     b = Z
+  natMul (S a) b = natPlus b (natMul a b)
 
-{-| This is the plain value-level version of addition on Nats. There's rarely a reason to use this;
-it's included for completeness. -}
-natPlus :: Nat -> Nat -> Nat
-natPlus = (Data.Nat.+)
+  natMinus :: Nat -> Nat -> Nat
+  natMinus Z     b     = Z
+  natMinus (S a) (S b) = natMinus a b
+  natMinus a     Z     = a
 
-{-| Similarly to 'natPlus', this one is included for completeness. -}
-natMul :: Nat -> Nat -> Nat
-natMul = (Data.Nat.*)
+  natAbs :: Nat -> Nat
+  natAbs n = n
+  |])                                
 
+instance PNum ('KProxy :: KProxy Nat) where
+  type a :+ b = NatPlus a b
+  type a :- b = NatMinus a b
+  type a :* b = NatMul a b
+  type Abs a = NatAbs a
+  type Signum (a :: Nat) = Error "Data.Nat: signum not implemented"
+  type FromInteger (a :: Lit.Nat) = Lit a
+
+instance SNum ('KProxy :: KProxy Nat) where  
+  (%:+) = sNatPlus
+  (%:*) = sNatMul
+  (%:-) = sNatMinus
+  sAbs  = sNatAbs  
+  sSignum = case toSing "Data.Nat: signum not implemented" of
+    SomeSing s -> sError s    
+  sFromInteger n = case n %:== (sing :: Sing 0) of
+    STrue  -> unsafeCoerce SZ
+    SFalse -> unsafeCoerce (SS (sFromInteger (n %:- (sing :: Sing 1))))
+
 {-| Converts a runtime 'Integer' to an existentially wrapped 'Nat'. Returns 'Nothing' if
 the argument is negative -}
-someNat :: Integer -> Maybe (SomeSing (KindOf Z))
-someNat n | n < 0 = Nothing
-someNat n = Just (go n) where  
-  go 0 = SomeSing SZ
-  go n = case go (n - 1) of
-    SomeSing sn -> SomeSing (SS sn)
+someNatVal :: Integer -> Maybe (SomeSing (KindOf Z))
+someNatVal n = case Lit.someNatVal n of
+  Just (Lit.SomeNat (pn :: Proxy n)) -> Just (SomeSing (sFromInteger (sing :: Sing n)))
+  Nothing -> Nothing
 
 {-| Provides a shorthand for 'Nat'-s using "GHC.TypeLits", for example:
 
diff --git a/singleton-nats.cabal b/singleton-nats.cabal
--- a/singleton-nats.cabal
+++ b/singleton-nats.cabal
@@ -1,23 +1,23 @@
-
-name:                singleton-nats
-version:             0.3.1.0
-synopsis:            Unary natural numbers relying on the singletons infrastructure.         
-license:             BSD3
-license-file:        LICENSE
-author:              András Kovács
-maintainer:          puttamalac@gmail.com
-copyright:           2015 András Kovács
-category:            Data
-build-type:          Simple
-
-cabal-version:       >=1.10
-
-library
-  exposed-modules:
-    Data.Nat
-
-  build-depends:       
-    base >=4.7 && <4.9,
-    singletons >= 1
-
+
+name:                singleton-nats
+version:             0.4.0.0
+synopsis:            Unary natural numbers relying on the singletons infrastructure.         
+license:             BSD3
+license-file:        LICENSE
+author:              András Kovács
+maintainer:          puttamalac@gmail.com
+copyright:           2015 András Kovács
+category:            Data
+build-type:          Simple
+
+cabal-version:       >=1.10
+
+library
+  exposed-modules:
+    Data.Nat
+
+  build-depends:       
+    base >=4.7 && <4.9,
+    singletons >= 2.0.1
+
   default-language:    Haskell2010