diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
index 7689de2..20875d1 100644
--- a/src/Quox/Context.idr
+++ b/src/Quox/Context.idr
@@ -2,6 +2,7 @@ module Quox.Context
 
 import Quox.Syntax.Shift
 import Quox.Pretty
+import Quox.NatExtra
 
 import Data.DPair
 import Data.Nat
@@ -151,38 +152,10 @@ export %inline
 ftel <*> xtel = runIdentity $ (pure .) <$> ftel `app` xtel
 -- ...but can't write pure without `from,to` being ω, so no idiom brackets ☹
 
-
-namespace Nat
-  public export
-  data LTE' : Nat -> Nat -> Type where
-    LTERefl  : n `LTE'` n
-    LTESuccR : m `LTE'` n -> m `LTE'` S n
-  %builtin Natural LTE'
-
-  export %hint
-  lteZero' : {n : Nat} -> 0 `LTE'` n
-  lteZero' {n = 0}   = LTERefl
-  lteZero' {n = S n} = LTESuccR lteZero'
-
-  export
-  lteSucc' : m `LTE'` n -> S m `LTE'` S n
-  lteSucc' LTERefl      = LTERefl
-  lteSucc' (LTESuccR p) = LTESuccR (lteSucc' p)
-
-  export
-  lteToLte' : {n : Nat} -> m `LTE` n -> m `LTE'` n
-  lteToLte' LTEZero     = lteZero'
-  lteToLte' (LTESucc p) = lteSucc' (lteToLte' p)
-
-  export
-  lte'ToLte : {n : Nat} -> m `LTE'` n -> m `LTE` n
-  lte'ToLte LTERefl      = reflexive
-  lte'ToLte (LTESuccR p) = lteSuccRight (lte'ToLte p)
-
-  export
-  teleLte' : Telescope tm from to -> from `LTE'` to
-  teleLte' [<]        = LTERefl
-  teleLte' (tel :< _) = LTESuccR (teleLte' tel)
+export
+teleLte' : Telescope tm from to -> from `LTE'` to
+teleLte' [<]        = LTERefl
+teleLte' (tel :< _) = LTESuccR (teleLte' tel)
 
 
 export
diff --git a/src/Quox/NatExtra.idr b/src/Quox/NatExtra.idr
new file mode 100644
index 0000000..0e7bec7
--- /dev/null
+++ b/src/Quox/NatExtra.idr
@@ -0,0 +1,30 @@
+module Quox.NatExtra
+
+import public Data.Nat
+
+
+public export
+data LTE' : Nat -> Nat -> Type where
+  LTERefl  : LTE' n n
+  LTESuccR : LTE' m n -> LTE' m (S n)
+%builtin Natural LTE'
+
+public export
+lteZero' : {n : Nat} -> LTE' 0 n
+lteZero' {n = 0}   = LTERefl
+lteZero' {n = S n} = LTESuccR lteZero'
+
+public export
+lteSucc' : LTE' m n -> LTE' (S m) (S n)
+lteSucc' LTERefl      = LTERefl
+lteSucc' (LTESuccR p) = LTESuccR $ lteSucc' p
+
+public export
+fromLTE : {n : Nat} -> LTE m n -> LTE' m n
+fromLTE LTEZero     = lteZero'
+fromLTE (LTESucc p) = lteSucc' $ fromLTE p
+
+public export
+toLte : {n : Nat} -> m `LTE'` n -> m `LTE` n
+toLte LTERefl      = reflexive
+toLte (LTESuccR p) = lteSuccRight (toLte p)
diff --git a/src/Quox/OPE.idr b/src/Quox/OPE.idr
index 51cf042..c57cac0 100644
--- a/src/Quox/OPE.idr
+++ b/src/Quox/OPE.idr
@@ -2,6 +2,8 @@
 ||| a smaller scope and part of a larger one.
 module Quox.OPE
 
+import Quox.NatExtra
+
 import Data.Nat
 
 
@@ -35,30 +37,9 @@ toLTE (Drop p) = lteSuccRight $ toLTE p
 toLTE (Keep p) = LTESucc      $ toLTE p
 
 
-public export
-data LTE' : Nat -> Nat -> Type where
-  LTERefl  : (n : Nat) -> LTE' n n
-  LTESuccR : Lazy (LTE' m n) -> LTE' m (S n)
-
-public export
-lteZero' : {n : Nat} -> LTE' 0 n
-lteZero' {n = 0}   = LTERefl 0
-lteZero' {n = S n} = LTESuccR $ delay lteZero'
-
-public export
-lteSucc' : LTE' m n -> LTE' (S m) (S n)
-lteSucc' (LTERefl n)  = LTERefl (S n)
-lteSucc' (LTESuccR p) = LTESuccR $ delay $ lteSucc' p
-
-public export
-fromLTE : {n : Nat} -> LTE m n -> LTE' m n
-fromLTE LTEZero     = lteZero'
-fromLTE (LTESucc p) = lteSucc' $ fromLTE p
-
-
 public export
 dropInner' : LTE' m n -> OPE m n
-dropInner' (LTERefl  n) = Id
+dropInner' LTERefl      = Id
 dropInner' (LTESuccR p) = Drop $ dropInner' $ force p
 
 public export