diff --git a/Data/Type/Natural/Class/Arithmetic.hs b/Data/Type/Natural/Class/Arithmetic.hs
--- a/Data/Type/Natural/Class/Arithmetic.hs
+++ b/Data/Type/Natural/Class/Arithmetic.hs
@@ -8,7 +8,7 @@
         plusCong, plusCongR, plusCongL, succCong,
         multCong, multCongL, multCongR,
         minusCong, minusCongL, minusCongR,
-        IsPeano(..), pattern Zero, pattern Succ
+        IsPeano(..), pattern Zero, pattern Succ,
        ) where
 import Data.Singletons.Decide
 import Data.Singletons.Prelude
@@ -16,7 +16,6 @@
 import Data.Type.Equality
 import Data.Void
 import Proof.Equational
-import Proof.Propositional
 
 type family Zero nat :: nat where
   Zero nat = FromInteger 0
@@ -131,6 +130,12 @@
   induction     :: p (Zero nat) -> (forall n. Sing n -> p n -> p (S n)) -> Sing k -> p k
   plusMinus :: Sing (n :: nat) -> Sing m -> n :+ m :- m :~: n
 
+  plusMinus' :: Sing (n :: nat) -> Sing m -> n :+ m :- n :~: m
+  plusMinus'  n m =
+    start (n %:+ m %:- n)
+      === m %:+ n %:- n   `because` minusCongL (plusComm n m) n
+      === m               `because` plusMinus m n
+
   plusZeroL :: Sing n -> (Zero nat :+ n) :~: n
   plusZeroL sn = idLProof (induction base step sn)
     where
@@ -383,7 +388,6 @@
       === (sZero %:+ n) %:- n  `because` minusCongL (sym $ plusZeroL n) n
       === sZero                `because` plusMinus sZero n
 
-
   multAssoc :: Sing (n :: nat) -> Sing m -> Sing l
             -> (n :* m) :* l :~: n :* (m :* l)
   multAssoc sn0 = assocProof $ induction base step sn0
@@ -484,6 +488,13 @@
   multEqSuccElimR n m l nmEsl =
     multEqSuccElimL m n l (multComm m n `trans` nmEsl)
 
+  minusZero :: Sing n -> n :- Zero nat :~: n
+  minusZero n =
+    start (n %:- sZero)
+      === (n %:+ sZero) %:- sZero
+             `because` minusCongL (sym $ plusZeroR n) sZero
+      === n  `because` plusMinus n sZero
+
   multEqCancelR :: Sing (n :: nat) -> Sing m -> Sing l -> n :* Succ l :~: m :* Succ l -> n :~: m
   multEqCancelR = proofMultEqCancelR . induction base step
     where
@@ -526,14 +537,6 @@
   sPred' :: proxy n -> Sing (Succ n) -> Sing (n :: nat)
   sPred' pxy sn = coerce (succInj $ succCong $ predSucc (sPred' pxy sn)) (sPred sn)
 
-refute [t| 'LT :~: 'GT |]
-refute [t| 'LT :~: 'EQ |]
-refute [t| 'EQ :~: 'LT |]
-refute [t| 'EQ :~: 'GT |]
-refute [t| 'GT :~: 'LT |]
-refute [t| 'GT :~: 'EQ |]
-refute [t| 'True :~: 'False |]
-
 pattern Zero :: forall nat (n :: nat). IsPeano nat => n ~ Zero nat => Sing n
 pattern Zero <- (zeroOrSucc -> IsZero) where
   Zero = sZero
@@ -541,3 +544,4 @@
 pattern Succ :: forall nat (n :: nat). IsPeano nat => forall (n1 :: nat). n ~ Succ n1 => Sing n1 -> Sing n
 pattern Succ n <- (zeroOrSucc -> IsSucc n) where
   Succ n = sSucc n
+
diff --git a/Data/Type/Natural/Class/Order.hs b/Data/Type/Natural/Class/Order.hs
--- a/Data/Type/Natural/Class/Order.hs
+++ b/Data/Type/Natural/Class/Order.hs
@@ -5,7 +5,8 @@
 module Data.Type.Natural.Class.Order
        (PeanoOrder(..), DiffNat(..), LeqView(..),
         FlipOrdering, sFlipOrdering, coerceLeqL, coerceLeqR,
-        sLeqCongL, sLeqCongR, sLeqCong
+        sLeqCongL, sLeqCongR, sLeqCong,
+        (:-.), (%:-.), minPlusTruncMinus, truncMinusLeq
        ) where
 import Data.Type.Natural.Class.Arithmetic
 
@@ -657,3 +658,51 @@
   lneqZeroAbsurd :: Sing n -> IsTrue (n :< Zero nat) -> Void
   lneqZeroAbsurd n leq =
     succLeqZeroAbsurd n (coerce (lneqSuccLeq n sZero) leq)
+
+  minusPlus :: forall (n :: nat) m .PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue (m :<= n)
+            -> n :- m :+ m :~: n
+  minusPlus n m mLEQn =
+    case leqWitness m n mLEQn of
+      DiffNat _ k ->
+        start (n %:- m %:+ m)
+          =~= m %:+ k %:- m %:+ m
+          === k %:+ m %:- m %:+ m  `because` plusCongL (minusCongL (plusComm m k) m) m
+          === k %:+ m              `because` plusCongL (plusMinus k m) m
+          === m %:+ k              `because` plusComm  k m
+          =~= n
+
+-- | Natural subtraction, truncated to zero if m > n.
+type n :-. m = Subt n m (m :<= n)
+type family Subt (n :: nat) (m :: nat) (b :: Bool) :: nat where
+  Subt n          m 'True  = n :- m
+  Subt (n :: nat) m 'False = Zero nat
+infixl 6 :-.
+
+(%:-.) :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> Sing (n :-. m)
+n %:-. m =
+  case m %:<= n of
+    STrue -> n %:- m
+    SFalse -> sZero
+
+minPlusTruncMinus :: (PeanoOrder nat) => Sing (n :: nat) -> Sing (m :: nat)
+                  -> Min n m :+ (n :-. m) :~: n
+minPlusTruncMinus n m =
+  case m %:<= n of
+    STrue ->
+      start (sMin n m %:+ (n %:-. m))
+        === m %:+ (n %:-. m) `because` plusCongL (geqToMin n m Witness) (n %:-. m)
+        =~= m %:+ (n %:- m)
+        === (n %:- m) %:+ m  `because` plusComm m (n %:- m)
+        === n                `because` minusPlus n m Witness
+    SFalse ->
+      start (sMin n m %:+ (n %:-. m))
+        =~= sMin n m %:+ sZero
+        === sMin n m  `because` plusZeroR (sMin n m)
+        === n         `because` leqToMin n m (notLeqToLeq m n)
+
+truncMinusLeq :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue (n :-. m :<= n)
+truncMinusLeq n m =
+  case m %:<= n of
+    STrue  -> leqStep (n %:-. m) n m $ minusPlus n m Witness
+    SFalse -> leqZero n
+
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.6.0.0
+version:             0.6.1.0
 synopsis:            Type-level natural and proofs of their properties.
 description:         Type-level natural numbers and proofs of their properties.
                      .
@@ -39,7 +39,7 @@
                      , Data.Type.Natural.Core
                      , Data.Type.Natural.Compat
   build-depends:       base                      >= 4       && < 5
-                     , equational-reasoning      == 0.4.*
+                     , equational-reasoning      >= 0.4.1   && < 1
                      , monomorphic               >= 0.0.3
                      , template-haskell          >= 2.8     && < 3
                      , constraints               >= 0.3     && < 0.9