diff --git a/Data/Type/Natural.hs b/Data/Type/Natural.hs
--- a/Data/Type/Natural.hs
+++ b/Data/Type/Natural.hs
@@ -75,8 +75,8 @@
 import Data.Type.Natural.Core
 import Data.Type.Natural.Definitions hiding ((:<=))
 
-import           Data.Constraint           hiding ((:-))
 import           Data.Singletons
+import qualified Data.Singletons.Prelude as S
 import           Data.Type.Monomorphic
 import           Language.Haskell.TH
 import           Language.Haskell.TH.Quote
@@ -86,6 +86,7 @@
 import           Prelude                   (Ord (..))
 import qualified Prelude                   as P
 import           Proof.Equational
+import Data.Constraint (Dict(..))
 
 --------------------------------------------------
 -- * Conversion functions.
@@ -242,7 +243,7 @@
 plusCommutative = plusComm
 {-# DEPRECATED plusCommutative "Will be removed in @0.5.0.0@. Use @'plusComm'@ instead." #-}
 
-eqSuccMinus :: ((m :<<= n) ~ 'True)
+eqSuccMinus :: ((m S.:<= n) ~ 'True)
             => SNat n -> SNat m -> ('S n :-: m) :=: ('S (n :-: m))
 eqSuccMinus _      SZ     = Refl
 eqSuccMinus (SS n) (SS m) =
diff --git a/Data/Type/Natural/Builtin.hs b/Data/Type/Natural/Builtin.hs
--- a/Data/Type/Natural/Builtin.hs
+++ b/Data/Type/Natural/Builtin.hs
@@ -36,6 +36,7 @@
 import           Data.Singletons.Decide       (Decision (..), (%~))
 import           Data.Singletons.Decide       (Void)
 import           Data.Singletons.Prelude.Bool (Sing (..))
+import           Data.Singletons.Prelude.Ord  (POrd(..), SOrd ((%:<=)))
 import           Data.Singletons.Prelude.Enum (Pred, sPred, sSucc)
 import           Data.Singletons.Prelude.Num  (SNum (..))
 import           Data.Type.Natural            (Nat (S, Z), Sing (SS, SZ))
@@ -224,10 +225,10 @@
 leqqCong :: n :=: m -> l :=: z -> (n TL.<=? l) :~: (m TL.<=? z)
 leqqCong Refl Refl = Refl
 
-leqCong :: n :=: m -> l :=: z -> (n PN.:<<= l) :~: (m PN.:<<= z)
+leqCong :: n :=: m -> l :=: z -> (n :<= l) :~: (m :<= z)
 leqCong Refl Refl = Refl
 
-fromPeanoMonotone :: ((n PN.:<<= m) ~ 'True) => Sing n -> Sing m -> (FromPeano n TL.<=? FromPeano m) :=: 'True
+fromPeanoMonotone :: ((n :<= m) ~ 'True) => Sing n -> Sing m -> (FromPeano n TL.<=? FromPeano m) :=: 'True
 fromPeanoMonotone SZ _ = Refl
 fromPeanoMonotone (SS n) (SS m) =
    start (sFromPeano (SS n) %:<=? sFromPeano (SS m))
@@ -250,7 +251,7 @@
 natSuccPred :: ((n :~: 0) -> Void) -> Succ (Pred n) :=: n
 natSuccPred _ = Refl
 
-myLeqPred :: Sing n -> Sing m -> ('S n PN.:<<= 'S m) :=: (n PN.:<<= m)
+myLeqPred :: Sing n -> Sing m -> ('S n :<= 'S m) :=: (n :<= m)
 myLeqPred SZ _ = Refl
 myLeqPred (SS _) (SS _) = Refl
 myLeqPred (SS _) SZ = Refl
@@ -259,7 +260,7 @@
 toPeanoCong Refl = Refl
 
 toPeanoMonotone :: (n TL.<= m)
-                => Sing n -> Sing m -> ((ToPeano n) PN.:<<= (ToPeano m)) :~: 'True
+                => Sing n -> Sing m -> ((ToPeano n) :<= (ToPeano m)) :~: 'True
 toPeanoMonotone sn sm =
   case sn %~ (sing :: Sing 0) of
     Proved Refl -> Refl
@@ -268,13 +269,13 @@
       Disproved mPos ->
         let pn = sPred sn
             pm = sPred sm
-        in start (sToPeano sn PN.%:<<= sToPeano sm)
-             === (sToPeano (sSucc pn) PN.%:<<= sToPeano (sSucc pm))
+        in start (sToPeano sn %:<= sToPeano sm)
+             === (sToPeano (sSucc pn) %:<= sToPeano (sSucc pm))
                  `because` leqCong (toPeanoCong $ sym $ natSuccPred nPos)
                                    (toPeanoCong $ sym $ natSuccPred mPos)
-             === (SS (sToPeano pn) PN.%:<<= SS (sToPeano pm))
+             === (SS (sToPeano pn) %:<= SS (sToPeano pm))
                  `because` leqCong (toPeanoSuccCong pn) (toPeanoSuccCong pm)
-             === (sToPeano pn PN.%:<<= sToPeano pm)
+             === (sToPeano pn %:<= sToPeano pm)
                  `because` myLeqPred (sToPeano pn) (sToPeano pm)
              === STrue `because` toPeanoMonotone pn pm
 
diff --git a/Data/Type/Natural/Core.hs b/Data/Type/Natural/Core.hs
--- a/Data/Type/Natural/Core.hs
+++ b/Data/Type/Natural/Core.hs
@@ -8,10 +8,12 @@
 import Data.Type.Natural.Compat
 #endif
 
-import Data.Constraint               hiding ((:-))
-import Data.Type.Natural.Definitions hiding ((:<=))
-import Prelude                       (Bool (..), Eq (..), Show (..), ($))
-import Unsafe.Coerce
+import           Data.Constraint               hiding ((:-))
+import qualified Data.Singletons.Prelude       as S
+import           Data.Type.Natural.Definitions hiding ((:<=))
+import           Prelude                       (Bool (..), Eq (..), Show (..),
+                                                ($))
+import           Unsafe.Coerce
 
 --------------------------------------------------
 -- ** Type-level predicate & judgements.
@@ -20,15 +22,16 @@
 class (n :: Nat) :<= (m :: Nat)
 instance 'Z :<= n
 instance (n :<= m) => 'S n :<= 'S m
+{-# DEPRECATED (:<=) "This class will be removed in 0.5.0.0. Use @(n 'Data.Singletons.Prelude.Ord.:<=' m) ~ 'True@ instead" #-}
 
 -- | Comparison via GADTs.
 data Leq (n :: Nat) (m :: Nat) where
   ZeroLeq     :: SNat m -> Leq Zero m
   SuccLeqSucc :: Leq n m -> Leq ('S n) ('S m)
 
-type LeqTrueInstance a b = Dict ((a :<<= b) ~ 'True)
+type LeqTrueInstance a b = Dict ((a S.:<= b) ~ 'True)
 
-(%-) :: (m :<<= n) ~ 'True => SNat n -> SNat m -> SNat (n :-: m)
+(%-) :: (m S.:<= n) ~ 'True => SNat n -> SNat m -> SNat (n :-: m)
 n   %- SZ    = n
 SS n %- SS m = n %- m
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
@@ -52,7 +55,7 @@
 propToBoolLeq _ = unsafeCoerce (Dict :: Dict ())
 {-# INLINE propToBoolLeq #-}
 
-boolToClassLeq :: (n :<<= m) ~ 'True => SNat n -> SNat m -> LeqInstance n m
+boolToClassLeq :: (n S.:<= m) ~ 'True => SNat n -> SNat m -> LeqInstance n m
 boolToClassLeq _ = unsafeCoerce (Dict :: Dict ())
 {-# INLINE boolToClassLeq #-}
 
@@ -78,7 +81,7 @@
 
 type LeqInstance n m = Dict (n :<= m)
 
-boolToPropLeq :: (n :<<= m) ~ 'True => SNat n -> SNat m -> Leq n m
+boolToPropLeq :: (n S.:<= m) ~ 'True => SNat n -> SNat m -> Leq n m
 boolToPropLeq SZ     m      = ZeroLeq m
 boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
diff --git a/Data/Type/Natural/Definitions.hs b/Data/Type/Natural/Definitions.hs
--- a/Data/Type/Natural/Definitions.hs
+++ b/Data/Type/Natural/Definitions.hs
@@ -153,9 +153,22 @@
  |]
 
 -- | Boolean-valued type-level comparison function.
-singletons [d|
- (<<=) :: Nat -> Nat -> Bool
- Z   <<= _   = True
- S _ <<= Z   = False
- S n <<= S m = n <<= m
- |]
+{-# DEPRECATED (<<=) "Use @'Ord'@ instance instead." #-}
+(<<=) :: Nat -> Nat -> Bool
+(<<=) = (<=)
+
+{-# DEPRECATED (:<<=) "Use @'(:<=)'@ from @'POrd'@ instead." #-}
+type n :<<= m = n :<= m
+
+{-# DEPRECATED (%:<<=) "Use @'(%:<=)'@ from @'POrd'@ instead." #-}
+(%:<<=) :: SNat n -> SNat m -> SBool (n :<<= m)
+(%:<<=) = (%:<=)
+
+type (:<<=$) = (:<=$)
+{-# DEPRECATED (:<<=$) "Use @(':<=$')@ instead." #-}
+
+type (:<<=$$) = (:<=$$)
+{-# DEPRECATED (:<<=$$) "Use @(':<=$$')@ instead." #-}
+
+type (:<<=$$$) n m = (:<=$$$) n m
+{-# DEPRECATED (:<<=$$$) "Use @(':<=$$$')@ instead." #-}
diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs
--- a/Data/Type/Ordinal.hs
+++ b/Data/Type/Ordinal.hs
@@ -22,14 +22,15 @@
 #endif
 
 import Control.Monad             (liftM)
-import Data.Constraint
 import Data.Singletons.Prelude
 import Data.Type.Monomorphic
 import Data.Type.Natural
+import Data.Constraint(Dict(..))
 import Data.Typeable             (Typeable)
 import Language.Haskell.TH
 import Language.Haskell.TH.Quote
 import Unsafe.Coerce
+import qualified Data.Singletons.Prelude as S
 
 -- | Set-theoretic (finite) ordinals:
 --
@@ -92,12 +93,12 @@
 unsafeFromInt n =
     case (promote n :: Monomorphic (Sing :: Nat -> *)) of
       Monomorphic sn ->
-           case SS sn %:<<= (sing :: SNat n) of
+           case SS sn %:<= (sing :: SNat n) of
              STrue -> sNatToOrd' (sing :: SNat n) sn
              SFalse -> error "Bound over!"
 
 -- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@.
-sNatToOrd' :: ('S m :<<= n) ~ 'True => SNat n -> SNat m -> Ordinal n
+sNatToOrd' :: ('S m S.:<= n) ~ 'True => SNat n -> SNat m -> Ordinal n
 sNatToOrd' (SS _) SZ = OZ
 sNatToOrd' (SS n) (SS m) = OS $ sNatToOrd' n m
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
@@ -105,11 +106,11 @@
 #endif
 
 -- | 'sNatToOrd'' with @n@ inferred.
-sNatToOrd :: (SingI n, ('S m :<<= n) ~ 'True) => SNat m -> Ordinal n
+sNatToOrd :: (SingI n, ('S m S.:<= n) ~ 'True) => SNat m -> Ordinal n
 sNatToOrd = sNatToOrd' sing
 
 data CastedOrdinal n where
-  CastedOrdinal :: ('S m :<<= n) ~ 'True => SNat m -> CastedOrdinal n
+  CastedOrdinal :: ('S m S.:<= n) ~ 'True => SNat m -> CastedOrdinal n
 
 -- | Convert @Ordinal n@ into @SNat m@ with the proof of @'S m :<<= n@.
 ordToSNat' :: Ordinal n -> CastedOrdinal n
@@ -134,7 +135,7 @@
 ordToInt (OS n) = 1 + ordToInt n
 
 -- | Inclusion function for ordinals.
-inclusion' :: (n :<<= m) ~ 'True => SNat m -> Ordinal n -> Ordinal m
+inclusion' :: (n S.:<= m) ~ 'True => SNat m -> Ordinal n -> Ordinal m
 inclusion' _ = unsafeCoerce
 {-# INLINE inclusion' #-}
 {-
@@ -147,7 +148,7 @@
 -}
 
 -- | Inclusion function for ordinals with codomain inferred.
-inclusion :: ((n :<<= m) ~ 'True) => Ordinal n -> Ordinal m
+inclusion :: ((n S.:<= m) ~ 'True) => Ordinal n -> Ordinal m
 inclusion on = unsafeCoerce on
 {-# INLINE inclusion #-}
 
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.4.1.1
+version:             0.4.2.0
 synopsis:            Type-level natural and proofs of their properties.
 description:         Type-level natural numbers and proofs of their properties.
 homepage:            https://github.com/konn/type-natural