diff --git a/Data/TypeNat/Nat.hs b/Data/TypeNat/Nat.hs
--- a/Data/TypeNat/Nat.hs
+++ b/Data/TypeNat/Nat.hs
@@ -1,12 +1,13 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
--- TBD can we get around incoherent instances!?!
 {-# LANGUAGE IncoherentInstances #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeFamilies #-}
 
 module Data.TypeNat.Nat (
 
@@ -14,6 +15,7 @@
   , IsNat(..)
 
   , LTE(..)
+  , StrongLTE
 
   , Zero
   , One
@@ -29,8 +31,22 @@
 
   ) where
 
+import Data.Proxy
+import GHC.Exts (Constraint)
+
 data Nat = Z | S Nat
 
+instance Eq Nat where
+    Z == Z = True
+    (S n) == (S m) = n == m
+    _ == _ = False
+
+instance Ord Nat where
+    Z `compare` Z = EQ
+    S n `compare` S m = n `compare` m
+    S n `compare` Z = GT
+    Z `compare` S m = LT
+
 type Zero = Z
 type One = S Z
 type Two = S One
@@ -54,22 +70,34 @@
 instance IsNat n => IsNat (S n) where
   natRecursion ifS ifZ reduce x = ifS x (natRecursion ifS ifZ reduce (reduce x))
 
+-- | A constrint which includes LTE k m for every k <= m.
+type family StrongLTE (n :: Nat) (m :: Nat) :: Constraint where
+  StrongLTE Z m = LTE Z m
+  StrongLTE (S n) m = (LTE (S n) m, StrongLTE n m)
+
 -- | Nat @n@ is less than or equal to nat @m@.
 --   Comes with functions to do type-directed computation for Nat-indexed
 --   datatypes.
 class LTE (n :: Nat) (m :: Nat) where
-  lteInduction :: (forall k . LTE (S k) m => d k -> d (S k)) -> d n -> d m
+  lteInduction
+    :: StrongLTE m l
+    => Proxy l
+    -> (forall k . LTE (S k) l => d k -> d (S k))
+    -- ^ The parameter l is fixed by any call to lteInduction, but due to
+    --   the StrongLTE m l constraint, we have LTE j l for every j <= m.
+    --   This allows us to implement the nontrivial case in the
+    --     @LTE p q => LTE p (S q)@
+    --   instance, where we need to use this function to get @x :: d p@ and then
+    --   again to get @f x :: d (S p)@. So long as @p@ and @S p@ are both
+    --   less or equal to @l@, this can be done.
+    -> d n
+    -> d m
   lteRecursion :: (forall k . LTE n k => d (S k) -> d k) -> d m -> d n
 
 instance LTE n n where
-  lteInduction f x = x
+  lteInduction _ f x = x
   lteRecursion f x = x
 
 instance LTE n m => LTE n (S m) where
-
-  -- Use the LTE n m instance to get  lteInduction f x :: d m
-  -- With this in hand, we can apply f again because
-  -- LTE (S m) (S m) is true so that f :: d m -> d (S m) and we're there!
-  lteInduction f x = f (lteInduction f x)
-
+  lteInduction (proxy :: Proxy l) f (x :: d n) = f (lteInduction proxy f x)
   lteRecursion f x = lteRecursion f (f x)
diff --git a/Data/TypeNat/Vect.hs b/Data/TypeNat/Vect.hs
--- a/Data/TypeNat/Vect.hs
+++ b/Data/TypeNat/Vect.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneDeriving #-}
 
 module Data.TypeNat.Vect (
 
@@ -22,6 +23,9 @@
 data Vect :: * -> Nat -> * where
   VNil :: Vect a Z
   VCons :: a -> Vect a n -> Vect a (S n)
+
+deriving instance Eq t => Eq (Vect t n)
+deriving instance Show t => Show (Vect t n)
 
 -- | A kind of fmap for Vect.
 vectMap :: (a -> b) -> Vect a n -> Vect b n
diff --git a/TypeNat.cabal b/TypeNat.cabal
--- a/TypeNat.cabal
+++ b/TypeNat.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                TypeNat
-version:             0.2.1.0
+version:             0.4.0.0
 synopsis:            Some Nat-indexed types for GHC
 -- description:         
 homepage:            https://github.com/avieth/TypeNat
@@ -18,7 +18,19 @@
 library
   exposed-modules:     Data.TypeNat.Fin, Data.TypeNat.Nat, Data.TypeNat.Vect
   -- other-modules:       
-  other-extensions:    DataKinds, KindSignatures, GADTs, Rank2Types
-  build-depends:       base >=4.7 && <4.8
+  other-extensions:    DataKinds
+                     , KindSignatures
+                     , GADTs
+                     , RankNTypes
+                     , MultiParamTypeClasses
+                     , FlexibleInstances
+                     , FlexibleContexts
+                     , ScopedTypeVariables
+                     , IncoherentInstances
+                     , ConstraintKinds
+                     , TypeFamilies
+                     , KindSignatures
+
+  build-depends:       base >=4.7 && < 4.8
   -- hs-source-dirs:      
   default-language:    Haskell2010