diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Hiromi ISHII (c) 2016
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Hiromi ISHII nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/examples/simple-arith.hs b/examples/simple-arith.hs
new file mode 100644
--- /dev/null
+++ b/examples/simple-arith.hs
@@ -0,0 +1,120 @@
+{-# LANGUAGE CPP, DataKinds, FlexibleContexts, GADTs, PolyKinds     #-}
+{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeApplications #-}
+{-# LANGUAGE TypeFamilies, TypeInType, TypeOperators                #-}
+{-# OPTIONS_GHC -fplugin Data.Singletons.TypeNats.Presburger #-}
+{-# OPTIONS_GHC -dcore-lint #-}
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 806
+{-# LANGUAGE NoStarIsType #-}
+#endif
+
+module Main where
+import Data.Singletons.Decide
+import Data.Singletons.Prelude
+import Data.Singletons.Prelude.Enum
+import Data.Singletons.Prelude.List
+import Data.Singletons.TH
+import Data.Singletons.TypeLits
+import Data.Type.Equality
+import GHC.TypeLits                 (type (<=?), CmpNat, Nat)
+import Proof.Propositional          (Empty (..), withEmpty)
+import Proof.Propositional          (IsTrue (Witness))
+
+#if !MIN_VERSION_singletons(2,4,0)
+import Data.Promotion.Prelude.Num
+
+type l <= m = l :<= m
+type l *  m = l :* m
+type l +  m = l :+ m
+type l -  m = l :- m
+infix 4 <=
+infixl 6 +, -
+infixl 7 *
+#endif
+
+type n <=! m = IsTrue (n <=? m)
+infix 4 <=!
+
+natLen :: (Length xs <= Length ys) ~ 'True
+       => proxy xs -> proxy ys -> (Length ys - Length xs) + Length xs :~: Length ys
+natLen _ _ = Refl
+
+
+-- The following three cases fails >= GHC 8.6.
+natLeqZero' :: ((n <= 0) ~ 'True) => proxy n -> n :~: 0
+natLeqZero' _ = Refl
+
+leqSucc :: proxy n -> proxy m -> IsTrue ((n + 1) <= m) -> CmpNat n m :~: 'LT
+leqSucc _ _ Witness = Refl
+
+leqEquiv :: (n <= m) ~ 'True => Sing n -> Sing m -> IsTrue (n <=? m)
+leqEquiv _ _ = Witness
+
+data NatView (n :: Nat) where
+  IsZero :: NatView 0
+  IsSucc :: Sing n -> NatView (n + 1)
+
+viewNat :: Sing n -> NatView n
+viewNat sn =
+  case sn %~ (sing :: Sing 0) of
+    Proved Refl    -> IsZero
+    Disproved _emp -> withEmpty _emp $ IsSucc $ sPred sn
+
+plusLeq :: (n <= m) ~ 'True => proxy (n :: Nat) -> proxy m -> ((m - n) + n :~: m)
+plusLeq _ _ = Refl
+
+minusLeq :: (n <= m) ~ 'True => proxy (n :: Nat) -> proxy m -> IsTrue ((m - n) + n <= m)
+minusLeq _ _ = Witness
+
+(%:<=?) :: Sing n -> Sing m -> Sing (n <=? m)
+n %:<=? m = case sCompare n m of
+  SLT -> STrue
+  SEQ -> STrue
+  SGT -> SFalse
+
+hoge :: ((n + 1 <=? n) ~ 'False) => proxy n -> ()
+hoge _ = ()
+
+hoge' :: (((n + 1) <= n) ~ 'False) => proxy n -> ()
+hoge' _ = ()
+
+bar :: ((2 * (n + 1)) ~ ((2 * n) + 2)) => proxy n -> ()
+bar _ = ()
+
+trans :: proxy n -> proxy m -> n <=! m -> (n + 1) <=! (m + 1)
+trans _ _  Witness = Witness
+
+eqv :: proxy n -> proxy m -> (n <=? m) :~: ((n + 1) <=? (m + 1))
+eqv _ _ = Refl
+
+predSucc :: forall proxy n. Empty (n <=! 0) => proxy n -> IsTrue (n + 1 <=? 2 * n)
+predSucc _ = Witness
+
+succLEqLTSucc :: Sing m -> Compare 0 (m + 1) :~: 'LT
+succLEqLTSucc _ = Refl
+
+succCompare :: Sing (n :: Nat) -> Sing m -> CmpNat n m :~: CmpNat (n + 1) (m + 1)
+succCompare _ _ = Refl
+
+eqToRefl :: Sing (n :: Nat) -> Sing (m :: Nat) -> CmpNat n m :~: 'EQ -> n :~: m
+eqToRefl _n _m Refl = Refl
+
+singletonsOnly [d|
+  flipOrdering :: Ordering -> Ordering
+  flipOrdering EQ = EQ
+  flipOrdering LT = GT
+  flipOrdering GT = LT
+ |]
+
+flipCompare
+  :: forall n m. (KnownNat n, KnownNat m)
+  => Sing n -> Sing m -> FlipOrdering (Compare n m) :~: Compare m n
+flipCompare n m = $(sCases ''Ordering [|sCompare n m|] [|Refl|])
+
+ltCompare
+  :: forall n m. (KnownNat n, KnownNat m, CmpNat n m ~ LT)
+  => Sing n -> Sing m -> Compare m n :~: GT
+ltCompare _ _ = Refl
+
+main :: IO ()
+main = putStrLn "finished"
+
diff --git a/singletons-presburger.cabal b/singletons-presburger.cabal
new file mode 100644
--- /dev/null
+++ b/singletons-presburger.cabal
@@ -0,0 +1,69 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.31.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 1398143e2ff5a7650c68eda0c0513d0db5b5ed760488ce49e28425fa4f97830c
+
+name:           singletons-presburger
+version:        0.3.0.0
+synopsis:       Presburger Arithmetic Solver for GHC Type-level natural numbers with Singletons package.
+description:    The @singletons-presburger@ plugin augments GHC type-system with Presburger
+                Arithmetic Solver for Type-level natural numbers, with integration with <https://hackage.haskell.org/package/singletons singletons> package.
+                .
+                You can use by adding this package to @dependencies@ and add the following pragma
+                to the head of .hs files:
+                .
+                > OPTIONS_GHC -fplugin Data.Singletons.TypeNats.Presburger
+category:       Math, Type System
+homepage:       https://github.com/konn/ghc-typelits-presburger#readme
+bug-reports:    https://github.com/konn/ghc-typelits-presburger/issues
+author:         Hiromi ISHII
+maintainer:     konn.jinro _at_ gmail.com
+copyright:      2015 (c) Hiromi ISHII
+license:        BSD3
+license-file:   LICENSE
+tested-with:    GHC==8.4.3 GHC==8.6.3 GHC==8.8.2
+build-type:     Simple
+
+source-repository head
+  type: git
+  location: https://github.com/konn/ghc-typelits-presburger
+
+flag examples
+  description: Builds example
+  manual: False
+  default: False
+
+library
+  exposed-modules:
+      Data.Singletons.TypeNats.Presburger
+  other-modules:
+      Paths_singletons_presburger
+  hs-source-dirs:
+      src
+  ghc-options: -Wall -Wno-dodgy-imports
+  build-depends:
+      base >=4.7 && <5
+    , ghc >=7.10 && <8.11
+    , ghc-typelits-presburger
+    , reflection
+    , singletons
+  default-language: Haskell2010
+
+executable simple-arith
+  main-is: simple-arith.hs
+  other-modules:
+      Paths_singletons_presburger
+  hs-source-dirs:
+      examples
+  ghc-options: -Wall -Wno-dodgy-imports -Wno-unused-imports
+  build-depends:
+      base
+    , equational-reasoning
+    , singletons
+    , singletons-presburger
+  if !(flag(examples))
+    buildable: False
+  default-language: Haskell2010
diff --git a/src/Data/Singletons/TypeNats/Presburger.hs b/src/Data/Singletons/TypeNats/Presburger.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Singletons/TypeNats/Presburger.hs
@@ -0,0 +1,138 @@
+{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances      #-}
+{-# LANGUAGE MultiWayIf, OverloadedStrings, PatternGuards, RankNTypes #-}
+{-# LANGUAGE RecordWildCards, TypeOperators, ViewPatterns             #-}
+module Data.Singletons.TypeNats.Presburger
+  (plugin, singletonTranslation
+  ) where
+import GHC.TypeLits.Presburger.Compat
+import GHC.TypeLits.Presburger.Types
+
+import Control.Monad
+import Data.Reflection (Given, give, given)
+import TcPluginM       (lookupOrig, matchFam)
+import Type            (splitTyConApp)
+
+plugin :: Plugin
+plugin = pluginWith $
+  (<>) <$> defaultTranslation <*> singletonTranslation
+
+data SingletonCons
+  = SingletonCons
+      { singNatLeq         :: TyCon
+      , singNatGeq         :: TyCon
+      , singNatLt          :: TyCon
+      , singNatGt          :: TyCon
+      , singNatPlus        :: TyCon
+      , singNatMinus       :: TyCon
+      , singNatTimes       :: TyCon
+      , singNatCompare     :: TyCon
+      , caseNameForSingLeq :: TyCon
+      , caseNameForSingGeq :: TyCon
+      , caseNameForSingLt  :: TyCon
+      , caseNameForSingGt  :: TyCon
+      }
+
+singletonTranslation
+  :: TcPluginM Translation
+singletonTranslation = toTranslation <$> genSingletonCons
+
+toTranslation
+  :: SingletonCons -> Translation
+toTranslation scs@SingletonCons{..} =
+  give scs $
+    mempty
+    { natLeqBool = [singNatLeq]
+    , natGeqBool = [singNatGeq]
+    , natLtBool  = [singNatLt]
+    , natGtBool  = [singNatGt]
+    , natCompare = [singNatCompare]
+    , natPlus = [singNatPlus]
+    , natMinus = [singNatMinus]
+    , natTimes = [singNatTimes]
+    , parsePred = parseSingPred
+    }
+
+genSingletonCons :: TcPluginM SingletonCons
+genSingletonCons = do
+  singletonOrd <- lookupModule (mkModuleName "Data.Singletons.Prelude.Ord") (fsLit "singletons")
+  singletonsNum <- lookupModule (mkModuleName "Data.Singletons.Prelude.Num") (fsLit "singletons")
+  -- prel <- lookupModule (mkModuleName "Data.Singletons.Prelude") (fsLit "singletons")
+  -- singTrueSym0 <- tcLookupTyCon =<< lookupOrig prel (mkTcOcc "TrueSym0")
+#if MIN_VERSION_singletons(2,4,1)
+  singNatLeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "<=")
+  singNatLt <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "<")
+  singNatGeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ">=")
+  singNatGt <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ">")
+  singNatPlus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc "+")
+  singNatTimes <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc "*")
+  singNatMinus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc "-")
+#else
+  singNatLeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ":<=")
+  singNatLt <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ":<")
+  singNatGeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ":>=")
+  singNatGt <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ":>")
+  singNatPlus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc ":+")
+  singNatTimes <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc ":*")
+  singNatMinus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc ":-")
+#endif
+  caseNameForSingLeq <- getCaseNameForSingletonOp singNatLeq
+  caseNameForSingLt <- getCaseNameForSingletonOp singNatLt
+  caseNameForSingGeq <- getCaseNameForSingletonOp singNatGeq
+  caseNameForSingGt <- getCaseNameForSingletonOp singNatGt
+  singNatCompare <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "Compare")
+  return SingletonCons{..}
+
+getCaseNameForSingletonOp :: TyCon -> TcPluginM TyCon
+getCaseNameForSingletonOp con = do
+  let vars = [typeNatKind, LitTy (NumTyLit 0), LitTy (NumTyLit 0)]
+  tcPluginTrace "matching... for " (ppr con)
+  Just (appTy0, [n,b,bdy,r]) <- fmap (splitTyConApp . snd) <$> matchFam  con vars
+  let (appTy, args) = splitTyConApp bdy
+  Just innermost <- fmap snd <$> matchFam appTy args
+  Just (_, dat) <- matchFam appTy0 [n,b,innermost,r]
+  Just dat' <- fmap snd <$> uncurry matchFam (splitTyConApp dat)
+  tcPluginTrace "matched. (orig, inner) = " (ppr (con, fst $ splitTyConApp dat'))
+  return $ fst $ splitTyConApp dat'
+
+lastTwo :: [a] -> [a]
+lastTwo = drop <$> subtract 2 . length <*> id
+
+parseSingPred
+  :: (Given SingletonCons)
+  => (Type -> Machine Expr) -> Type -> Machine Prop
+parseSingPred toExp ty
+  | isEqPred ty = parseSingPredTree toExp $ classifyPredType ty
+  | Just (con, [_,_,_,_,cmpTy]) <- splitTyConApp_maybe ty
+  , Just bin <- lookup con compCaseDic
+  , Just (cmp, lastTwo -> [l, r]) <- splitTyConApp_maybe cmpTy
+  , cmp `elem` [singNatCompare given, typeNatCmpTyCon] =
+      bin <$> toExp l <*> toExp r
+  | otherwise = mzero
+
+compCaseDic :: Given SingletonCons => [(TyCon, Expr -> Expr -> Prop)]
+compCaseDic =
+  [ (caseNameForSingLeq given, (:<=))
+  , (caseNameForSingLt given, (:<))
+  , (caseNameForSingGeq given, (:>=))
+  , (caseNameForSingGt given, (:>))
+  ]
+
+
+parseSingPredTree
+  :: Given SingletonCons
+  => (Type -> Machine Expr)
+  -> PredTree -> Machine Prop
+parseSingPredTree toExp (EqPred NomEq p b)  -- (n :<=? m) ~ 'True
+  | Just promotedTrueDataCon  == tyConAppTyCon_maybe b -- Singleton's <=...
+  , Just (con, [_,_,_,_,cmpTy]) <- splitTyConApp_maybe p
+  , Just bin <- lookup con compCaseDic
+  , Just (cmp, lastTwo -> [l, r]) <- splitTyConApp_maybe cmpTy
+  , cmp `elem` [singNatCompare given, typeNatCmpTyCon] =
+    bin <$> toExp l <*> toExp r
+  | Just promotedFalseDataCon  == tyConAppTyCon_maybe b -- Singleton's <=...
+  , Just (con, [_,_,_,_,cmpTy]) <- splitTyConApp_maybe p
+  , Just bin <- lookup con compCaseDic
+  , Just (cmp, lastTwo -> [l, r]) <- splitTyConApp_maybe cmpTy
+  , cmp `elem` [singNatCompare given, typeNatCmpTyCon] =
+    fmap Not . bin <$> toExp l <*> toExp r
+parseSingPredTree _ _ = mzero