diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs
--- a/Data/Type/Ordinal.hs
+++ b/Data/Type/Ordinal.hs
@@ -7,7 +7,9 @@
        ( -- * Data-types
          Ordinal (..),
          -- * Conversion from cardinals to ordinals.
-         sNatToOrd', sNatToOrd, ordToInt, ordToSNat, unsafeFromInt,
+         sNatToOrd', sNatToOrd, ordToInt, ordToSNat,
+         ordToSNat', CastedOrdinal(..),
+         unsafeFromInt,
          -- * Ordinal arithmetics
          (@+), enumOrdinal
        ) where
@@ -86,6 +88,16 @@
 -- | 'sNatToOrd'' with @n@ inferred.
 sNatToOrd :: (SingRep n, (S m :<<= n) ~ True) => SNat m -> Ordinal n
 sNatToOrd = sNatToOrd' sing
+
+data CastedOrdinal n where
+  CastedOrdinal :: (S m :<<= n) ~ True => SNat m -> CastedOrdinal n
+
+-- | Convert @Ordinal n@ into @SNat m@ with the proof of @S m :<<= n@.
+ordToSNat' :: Ordinal n -> CastedOrdinal n
+ordToSNat' OZ = CastedOrdinal sZ
+ordToSNat' (OS on) =
+  case ordToSNat' on of
+    CastedOrdinal m -> CastedOrdinal (sS m)
 
 -- | Convert @Ordinal n@ into monomorphic @SNat@
 ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *)
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.0.5.0
+version:             0.0.6.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