diff --git a/Data/TypeNat/Nat.hs b/Data/TypeNat/Nat.hs
--- a/Data/TypeNat/Nat.hs
+++ b/Data/TypeNat/Nat.hs
@@ -1,13 +1,22 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+-- TBD can we get around incoherent instances!?!
+{-# LANGUAGE IncoherentInstances #-}
 
 module Data.TypeNat.Nat (
 
     Nat(..)
-  , IsNat
-  , natRecursion
+  , IsNat(..)
 
+  , LTE(..)
+
+  , Zero
   , One
   , Two
   , Three
@@ -23,6 +32,7 @@
 
 data Nat = Z | S Nat
 
+type Zero = Z
 type One = S Z
 type Two = S One
 type Three = S Two
@@ -44,3 +54,28 @@
 
 instance IsNat n => IsNat (S n) where
   natRecursion ifS ifZ reduce x = ifS x (natRecursion ifS ifZ reduce (reduce x))
+
+-- | 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
+  lteRecursion :: (forall k . LTE n k => d (S k) -> d k) -> d m -> d n
+
+instance LTE n n where
+  lteInduction f x = x
+  lteRecursion f x = x
+
+instance LTE n m => LTE n (S m) where
+
+  lteInduction
+    :: forall (d :: Nat -> *) .
+       (forall (k :: Nat) . LTE (S k) (S m) => d k -> d (S k))
+    -> d n
+    -> d (S m)
+  lteInduction f x =
+      let sub :: d m
+          sub = lteInduction f x
+      in  f sub
+
+  lteRecursion f x = lteRecursion f (f x)
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.1.0.0
+version:             0.2.0.0
 synopsis:            Some Nat-indexed types for GHC
 -- description:         
 homepage:            https://github.com/avieth/TypeNat