diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,7 @@
-# 0.1.0.0
+# 0.2.0 (2021-11-05)
+
+* Remove `Cmp` in favor of the new `type-compare` compatibility layer.
+
+# 0.1.0.0 (2021-09-08)
 
 Initial version.
diff --git a/numeric-kinds.cabal b/numeric-kinds.cabal
--- a/numeric-kinds.cabal
+++ b/numeric-kinds.cabal
@@ -1,14 +1,12 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.33.0.
+-- This file has been generated from package.yaml by hpack version 0.34.4.
 --
 -- see: https://github.com/sol/hpack
---
--- hash: 05ac8c3fea5a45f8da84a8ec3977066bf0902c70969070e7baab2643ef9c665b
 
 name:           numeric-kinds
-version:        0.1.0.0
-synopsis:       Type-level numeric types, classes, and instances.
+version:        0.2.0
+synopsis:       Type-level numeric types and classes
 description:    This provides numeric types meant for use at the type level with -XDataKinds,
                 along with type families that act like type-level typeclasses providing
                 various operations.
@@ -38,10 +36,9 @@
   exposed-modules:
     Kinds.Integer
     Kinds.Num
-  other-modules:
-    Paths_numeric_kinds
   hs-source-dirs:
     src
   build-depends:
-    base >=4.12 && <4.16
+    base >=4.12 && <4.17,
+    type-compare ==0.1.*
   default-language: Haskell2010
diff --git a/src/Kinds/Integer.hs b/src/Kinds/Integer.hs
--- a/src/Kinds/Integer.hs
+++ b/src/Kinds/Integer.hs
@@ -52,9 +52,6 @@
            -- * Axioms
          , plusMinusInverseL, plusMinusInverseR
          , mulCommutes
-
-           -- * Utility
-         , CaseOrdering
          ) where
 
 import Prelude hiding (Integer)
@@ -65,7 +62,8 @@
 import GHC.TypeNats (KnownNat, Nat, natVal')
 import Unsafe.Coerce (unsafeCoerce)
 
-import Kinds.Num (type (+), type (-), type (*), Cmp, FromNat, ToInteger)
+import Kinds.Num (type (+), type (-), type (*), FromNat, ToInteger)
+import Kinds.Ord (Compare, OrdCond)
 
 -- | Type-level signed numbers
 data Integer = Pos Nat | Neg Nat
@@ -84,7 +82,7 @@
           then error "illegal KnownInteger (-0)"
           else negate $ toInteger x
 
-type instance Cmp {- k=Integer -} x y = CmpInteger x y
+type instance Compare {- k=Integer -} x y = CmpInteger x y
 type instance FromNat {- k=Integer -} n = 'Pos n
 
 type instance ToInteger {- k=Integer -} n = n
@@ -97,27 +95,17 @@
 
 -- | Comparison of type-level integers.
 type family CmpInteger m n where
-  CmpInteger ('Pos m) ('Pos n) = Cmp m n
+  CmpInteger ('Pos m) ('Pos n) = Compare m n
   CmpInteger ('Pos 0) ('Neg 0) = 'EQ
   CmpInteger ('Pos m) ('Neg n) = 'GT
   CmpInteger ('Neg 0) ('Pos 0) = 'EQ
   CmpInteger ('Neg m) ('Pos n) = 'LT
-  CmpInteger ('Neg m) ('Neg n) = Cmp n m -- Note: reversed
-
--- | Type-level eliminator for 'Ordering'.
---
--- @CaseOrdering o lt eq gt@ selects from among @lt@, @eq@, and @gt@ according
--- to @o@.  This is primarily exported so Haddock doesn't complain about being
--- unable to link it when it's mentioned in type instance clauses.
-type family CaseOrdering (o :: Ordering) (lt :: k) (eq :: k) (gt :: k) :: k where
-  CaseOrdering 'LT lt eq gt = lt
-  CaseOrdering 'EQ lt eq gt = eq
-  CaseOrdering 'GT lt eq gt = gt
+  CmpInteger ('Neg m) ('Neg n) = Compare n m -- Note: reversed
 
 -- | Given two 'Nat's @m@ and @n@, computes @m - n@ as an 'Integer'.
 type family (m :: Nat) -# (n :: Nat) where
   -- Redundant cases solely to make sure we get stuck reducing '-#' rather
-  -- than reducing @CaseOrdering (Cmp m n) tons of junk@ when the magnitude is
+  -- than reducing @OrdCond (Compare m n) tons of junk@ when the magnitude is
   -- a type variable.  This is similar to adding a bang pattern or case
   -- statement to a term-level function to make it strict in its arguments; but
   -- we don't have case statements or bang patterns in type families, so we add
@@ -125,7 +113,7 @@
   n -# 0 = 'Pos n  -- Order matters: 0 -# 0 should be 'Pos 0
   0 -# n = 'Neg n
 
-  m -# n = CaseOrdering (Cmp m n)
+  m -# n = OrdCond (Compare m n)
     ('Neg (n - m))
     ('Pos 0)
     ('Pos (m - n))
diff --git a/src/Kinds/Num.hs b/src/Kinds/Num.hs
--- a/src/Kinds/Num.hs
+++ b/src/Kinds/Num.hs
@@ -12,16 +12,17 @@
 -- See the License for the specific language governing permissions and
 -- limitations under the License.
 
--- | Type-level 'Ord' and 'Num'.
+-- | Type-level equivalent of a subset of 'Num'.
 --
 -- This provides "kindclasses" (actually open type families) with functionality
--- analogous to that provided by the typeclasses 'Ord' and 'Num'.  Since
--- type-level typeclasses don't exist, instead we translate each would-be
--- method to its own open type family; then "instances" are implemented by
--- providing clauses for each type family "method".  Unfortunately this means
--- we can't group methods into classes that must be implemented all-or-none,
--- but in practice this seems to be okay.
+-- analogous to that provided by the 'Num' typeclass.  Since type-level
+-- typeclasses don't exist, instead we translate each would-be method to its
+-- own open type family; then "instances" are implemented by providing clauses
+-- for each type family "method".  Unfortunately this means we can't group
+-- methods into classes that must be implemented all-or-none, but in practice
+-- this seems to be okay.
 
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE NoStarIsType #-}
@@ -30,40 +31,20 @@
 {-# LANGUAGE TypeOperators #-}
 
 module Kinds.Num
-         ( -- * Comparisons
-           Cmp
-         , type (<?), type (<=?), type (==?), type (/=?), type (>=?), type (>?)
-
-           -- ** Inequality Constraints
-         , type (<), type (<=), type (==), type (/=), type (>=), type (>)
-
-           -- * Conversions
-         , FromNat, ToInteger
+         ( -- * Conversions
+           FromNat, ToInteger
 
            -- * Arithmetic
          , type (+), type (-), type (*)
-
-           -- * Utility
-         , Proven, IsLT, IsLE, IsGT, IsGE, IsEQ, IsNE
          ) where
 
 import Prelude hiding (Integer)
 
-import GHC.TypeNats (CmpNat, Nat)
+import GHC.TypeNats (Nat)
 import qualified GHC.TypeNats as N (type (+), type (-), type (*))
 
 import {-# source #-}  Kinds.Integer (Integer(..))
 
--- | Type-level Ord "kindclass".
---
--- Note this has an invisible dependent @k@ parameter that makes the
--- textually-identical instances for different kinds actually different.  Neat!
-type family Cmp (x :: k) (y :: k) :: Ordering
-
--- That is, this is @Cmp {k=Nat} x y@, which is distinct from
--- @Cmp {k=Integer} x y@, even though both of them are written as @Cmp x y@.
-type instance Cmp {- k=Nat -} x y = CmpNat x y
-
 -- | Type-level numeric conversion from 'Nat'.  Like 'fromInteger' in 'Num'.
 type family FromNat (n :: Nat) :: k
 
@@ -88,54 +69,3 @@
 type family (x :: k) * (y :: k) :: k
 
 type instance x * y = (N.*) x y
-
-infix 4 <?, >?, <=?, >=?, ==?, /=?
-
-type x <?  y = IsLT (Cmp x y)
-type x >?  y = IsGT (Cmp x y)
-type x <=? y = IsLE (Cmp x y)
-type x >=? y = IsGE (Cmp x y)
-type x ==? y = IsEQ (Cmp x y)
-type x /=? y = IsNE (Cmp x y)
-
--- | Turns a type-level 'Bool' into a 'Data.Kind.Constraint' that it's 'True'.
-type Proven b = b ~ 'True
-
-infix 4 <, >, <=, >=, ==, /=
-
-type x <  y = Cmp x y ~ 'LT
-type x >  y = Cmp x y ~ 'GT
-type x == y = Cmp x y ~ 'EQ
-type x <= y = Proven (x <=? y)
-type x >= y = Proven (x >=? y)
-type x /= y = Proven (x /=? y)
-
--- | Test whether an 'Ordering' is 'LT'.
-type family IsLT o where
-  IsLT 'LT = 'True
-  IsLT o   = 'False
-
--- | Test whether an 'Ordering' is 'LT' or 'EQ'.
-type family IsLE o where
-  IsLE 'GT = 'False
-  IsLE o   = 'True
-
--- | Test whether an 'Ordering' is 'GT'.
-type family IsGT o where
-  IsGT 'GT = 'True
-  IsGT o   = 'False
-
--- | Test whether an 'Ordering' is 'GT' or 'EQ'.
-type family IsGE o where
-  IsGE 'LT = 'False
-  IsGE o   = 'True
-
--- | Test whether an 'Ordering' is 'EQ'.
-type family IsEQ o where
-  IsEQ 'EQ = 'True
-  IsEQ o   = 'False
-
--- | Test whether an 'Ordering' is 'LT' or 'GT'.
-type family IsNE o where
-  IsNE 'EQ = 'False
-  IsNE o   = 'True