diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,10 @@
 # Revision history for fin
 
+## 0.1
+
+- Rename `Fin` constructors to `FZ` and `FS`.
+  Now you can have both `Nat` and `Fin` imported unqualified in a single module.
+
 ## 0.0.3
 
 - Add `Data.Type.Nat.LE`, `Data.Type.Nat.LT` and `Data.Type.Nat.LE.ReflStep`
diff --git a/fin.cabal b/fin.cabal
--- a/fin.cabal
+++ b/fin.cabal
@@ -1,6 +1,6 @@
 cabal-version:      >=1.10
 name:               fin
-version:            0.0.3
+version:            0.1
 synopsis:           Nat and Fin: peano naturals and finite numbers
 category:           Data, Dependent Types, Singletons
 description:
diff --git a/src/Data/Fin.hs b/src/Data/Fin.hs
--- a/src/Data/Fin.hs
+++ b/src/Data/Fin.hs
@@ -8,7 +8,13 @@
 {-# LANGUAGE UndecidableInstances #-}
 -- | Finite numbers.
 --
--- This module is designed to be imported qualified.
+-- This module is designed to be imported as
+--
+-- @
+-- import Data.Fin (Fin (..))
+-- import qualified Data.Fin as Fin
+-- @
+--
 module Data.Fin (
     Fin (..),
     cata,
@@ -45,14 +51,15 @@
 import Data.Typeable      (Typeable)
 import GHC.Exception      (ArithException (..), throw)
 import Numeric.Natural    (Natural)
+import Data.Type.Nat (Nat (..))
 
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Type.Nat      as N
 
 -- | Finite numbers: @[0..n-1]@.
-data Fin (n :: N.Nat) where
-    Z :: Fin ('N.S n)
-    S :: Fin n -> Fin ('N.S n)
+data Fin (n :: Nat) where
+    FZ :: Fin ('S n)
+    FS :: Fin n -> Fin ('S n)
   deriving (Typeable)
 
 -------------------------------------------------------------------------------
@@ -77,7 +84,7 @@
 -- *** Exception: divide by zero
 -- ...
 --
--- >>> signum (Z :: Fin N.Nat1)
+-- >>> signum (FZ :: Fin N.Nat1)
 -- 0
 --
 -- >>> signum (3 :: Fin N.Nat4)
@@ -92,9 +99,9 @@
 instance N.SNatI n => Num (Fin n) where
     abs = id
 
-    signum Z         = Z
-    signum (S Z)     = S Z
-    signum (S (S _)) = S Z
+    signum FZ          = FZ
+    signum (FS FZ)     = FS FZ
+    signum (FS (FS _)) = FS FZ
 
     fromInteger = unsafeFromNum . (`mod` (N.reflectToNum (Proxy :: Proxy n)))
 
@@ -140,22 +147,22 @@
 instance N.SNatI n => Enum (Fin n) where
     fromEnum = go where
         go :: Fin m -> Int
-        go Z     = 0
-        go (S n) = succ (go n)
+        go FZ     = 0
+        go (FS n) = succ (go n)
 
     toEnum = unsafeFromNum
 
-instance (n ~ 'N.S m, N.SNatI m) => Bounded (Fin n) where
-    minBound = Z
+instance (n ~ 'S m, N.SNatI m) => Bounded (Fin n) where
+    minBound = FZ
     maxBound = getMaxBound $ N.induction
-        (MaxBound Z)
-        (MaxBound . S . getMaxBound)
+        (MaxBound FZ)
+        (MaxBound . FS . getMaxBound)
 
-newtype MaxBound n = MaxBound { getMaxBound :: Fin ('N.S n) }
+newtype MaxBound n = MaxBound { getMaxBound :: Fin ('S n) }
 
 instance NFData (Fin n) where
-    rnf Z     = ()
-    rnf (S n) = rnf n
+    rnf FZ     = ()
+    rnf (FS n) = rnf n
 
 instance Hashable (Fin n) where
     hashWithSalt salt = hashWithSalt salt . cata (0 :: Integer) succ
@@ -167,19 +174,19 @@
 -- | 'show' displaying a structure of 'Fin'.
 --
 -- >>> explicitShow (0 :: Fin N.Nat1)
--- "Z"
+-- "FZ"
 --
 -- >>> explicitShow (2 :: Fin N.Nat3)
--- "S (S Z)"
+-- "FS (FS FZ)"
 --
 explicitShow :: Fin n -> String
 explicitShow n = explicitShowsPrec 0 n ""
 
 -- | 'showsPrec' displaying a structure of 'Fin'.
 explicitShowsPrec :: Int -> Fin n -> ShowS
-explicitShowsPrec _ Z     = showString "Z"
-explicitShowsPrec d (S n) = showParen (d > 10)
-    $ showString "S "
+explicitShowsPrec _ FZ     = showString "FZ"
+explicitShowsPrec d (FS n) = showParen (d > 10)
+    $ showString "FS "
     . explicitShowsPrec 11 n
 
 -------------------------------------------------------------------------------
@@ -190,12 +197,12 @@
 cata :: forall a n. a -> (a -> a) -> Fin n -> a
 cata z f = go where
     go :: Fin m -> a
-    go Z = z
-    go (S n) = f (go n)
+    go FZ = z
+    go (FS n) = f (go n)
 
 -- | Convert to 'Nat'.
 toNat :: Fin n -> N.Nat
-toNat = cata N.Z N.S
+toNat = cata Z S
 
 -- | Convert from 'Nat'.
 --
@@ -207,13 +214,13 @@
 --
 fromNat :: N.SNatI n => N.Nat -> Maybe (Fin n)
 fromNat = appNatToFin (N.induction start step) where
-    start :: NatToFin 'N.Z
+    start :: NatToFin 'Z
     start = NatToFin $ const Nothing
 
-    step :: NatToFin n -> NatToFin ('N.S n)
+    step :: NatToFin n -> NatToFin ('S n)
     step (NatToFin f) = NatToFin $ \n -> case n of
-        N.Z   -> Just Z
-        N.S m -> fmap S (f m)
+        Z   -> Just FZ
+        S m -> fmap FS (f m)
 
 newtype NatToFin n = NatToFin { appNatToFin :: N.Nat -> Maybe (Fin n) }
 
@@ -224,16 +231,16 @@
 -- | Convert from any 'Ord' 'Num'.
 unsafeFromNum :: forall n i. (Num i, Ord i, N.SNatI n) => i -> Fin n
 unsafeFromNum = appUnsafeFromNum (N.induction start step) where
-    start :: UnsafeFromNum i 'N.Z
+    start :: UnsafeFromNum i 'Z
     start = UnsafeFromNum $ \n -> case compare n 0 of
         LT -> throw Underflow
         EQ -> throw Overflow
         GT -> throw Overflow
 
-    step :: UnsafeFromNum i m -> UnsafeFromNum i ('N.S m)
+    step :: UnsafeFromNum i m -> UnsafeFromNum i ('S m)
     step (UnsafeFromNum f) = UnsafeFromNum $ \n -> case compare n 0 of
-        EQ -> Z
-        GT -> S (f (n - 1))
+        EQ -> FZ
+        GT -> FS (f (n - 1))
         LT -> throw Underflow
 
 newtype UnsafeFromNum i n = UnsafeFromNum { appUnsafeFromNum :: i -> Fin n }
@@ -248,17 +255,17 @@
 -- [0,1,2]
 universe :: N.SNatI n => [Fin n]
 universe = getUniverse $ N.induction (Universe []) step where
-    step :: Universe n -> Universe ('N.S n)
-    step (Universe xs) = Universe (Z : map S xs)
+    step :: Universe n -> Universe ('S n)
+    step (Universe xs) = Universe (FZ : map FS xs)
 
 -- | Like 'universe' but 'NonEmpty'.
 --
 -- >>> universe1 :: NonEmpty (Fin N.Nat3)
 -- 0 :| [1,2]
-universe1 :: N.SNatI n => NonEmpty (Fin ('N.S n))
-universe1 = getUniverse1 $ N.induction (Universe1 (Z :| [])) step where
-    step :: Universe1 n -> Universe1 ('N.S n)
-    step (Universe1 xs) = Universe1 (NE.cons Z (fmap S xs))
+universe1 :: N.SNatI n => NonEmpty (Fin ('S n))
+universe1 = getUniverse1 $ N.induction (Universe1 (FZ :| [])) step where
+    step :: Universe1 n -> Universe1 ('S n)
+    step (Universe1 xs) = Universe1 (NE.cons FZ (fmap FS xs))
 
 -- | 'universe' which will be fully inlined, if @n@ is known at compile time.
 --
@@ -266,18 +273,18 @@
 -- [0,1,2]
 inlineUniverse :: N.InlineInduction n => [Fin n]
 inlineUniverse = getUniverse $ N.inlineInduction (Universe []) step where
-    step :: Universe n -> Universe ('N.S n)
-    step (Universe xs) = Universe (Z : map S xs)
+    step :: Universe n -> Universe ('S n)
+    step (Universe xs) = Universe (FZ : map FS xs)
 
 -- | >>> inlineUniverse1 :: NonEmpty (Fin N.Nat3)
 -- 0 :| [1,2]
-inlineUniverse1 :: N.InlineInduction n => NonEmpty (Fin ('N.S n))
-inlineUniverse1 = getUniverse1 $ N.inlineInduction (Universe1 (Z :| [])) step where
-    step :: Universe1 n -> Universe1 ('N.S n)
-    step (Universe1 xs) = Universe1 (NE.cons Z (fmap S xs))
+inlineUniverse1 :: N.InlineInduction n => NonEmpty (Fin ('S n))
+inlineUniverse1 = getUniverse1 $ N.inlineInduction (Universe1 (FZ :| [])) step where
+    step :: Universe1 n -> Universe1 ('S n)
+    step (Universe1 xs) = Universe1 (NE.cons FZ (fmap FS xs))
 
 newtype Universe  n = Universe  { getUniverse  :: [Fin n] }
-newtype Universe1 n = Universe1 { getUniverse1 :: NonEmpty (Fin ('N.S n)) }
+newtype Universe1 n = Universe1 { getUniverse1 :: NonEmpty (Fin ('S n)) }
 
 -- | @'Fin' 'N.Nat0'@ is inhabited.
 absurd :: Fin N.Nat0 -> b
@@ -288,7 +295,7 @@
 -- >>> boring
 -- 0
 boring :: Fin N.Nat1
-boring = Z
+boring = FZ
 
 -------------------------------------------------------------------------------
 -- Append & Split
@@ -296,20 +303,20 @@
 
 weakenLeft :: forall n m. N.InlineInduction n => Proxy m -> Fin n -> Fin (N.Plus n m)
 weakenLeft _ = getWeakenLeft (N.inlineInduction start step :: WeakenLeft m n) where
-    start :: WeakenLeft m 'N.Z
+    start :: WeakenLeft m 'Z
     start = WeakenLeft absurd
 
-    step :: WeakenLeft m p -> WeakenLeft m ('N.S p)
+    step :: WeakenLeft m p -> WeakenLeft m ('S p)
     step (WeakenLeft go) = WeakenLeft $ \n -> case n of
-        Z    -> Z
-        S n' -> S (go n')
+        FZ    -> FZ
+        FS n' -> FS (go n')
 
 newtype WeakenLeft m n = WeakenLeft { getWeakenLeft :: Fin n -> Fin (N.Plus n m) }
 
 weakenRight :: forall n m. N.InlineInduction n => Proxy n -> Fin m -> Fin (N.Plus n m)
 weakenRight _ = getWeakenRight (N.inlineInduction start step :: WeakenRight m n) where
     start = WeakenRight id
-    step (WeakenRight go) = WeakenRight $ \x -> S $ go x
+    step (WeakenRight go) = WeakenRight $ \x -> FS $ go x
 
 newtype WeakenRight m n = WeakenRight { getWeakenRight :: Fin m -> Fin (N.Plus n m) }
 
@@ -338,13 +345,13 @@
 --
 split :: forall n m. N.InlineInduction n => Fin (N.Plus n m) -> Either (Fin n) (Fin m)
 split = getSplit (N.inlineInduction start step) where
-    start :: Split m 'N.Z
+    start :: Split m 'Z
     start = Split Right
 
-    step :: Split m p -> Split m ('N.S p)
+    step :: Split m p -> Split m ('S p)
     step (Split go) = Split $ \x -> case x of
-        Z    -> Left Z
-        S x' -> bimap S id $ go x'
+        FZ    -> Left FZ
+        FS x' -> bimap FS id $ go x'
 
 newtype Split m n = Split { getSplit :: Fin (N.Plus n m) -> Either (Fin n) (Fin m) }
 
@@ -352,24 +359,24 @@
 -- Aliases
 -------------------------------------------------------------------------------
 
-fin0 :: Fin (N.Plus N.Nat0 ('N.S n))
-fin1 :: Fin (N.Plus N.Nat1 ('N.S n))
-fin2 :: Fin (N.Plus N.Nat2 ('N.S n))
-fin3 :: Fin (N.Plus N.Nat3 ('N.S n))
-fin4 :: Fin (N.Plus N.Nat4 ('N.S n))
-fin5 :: Fin (N.Plus N.Nat5 ('N.S n))
-fin6 :: Fin (N.Plus N.Nat6 ('N.S n))
-fin7 :: Fin (N.Plus N.Nat7 ('N.S n))
-fin8 :: Fin (N.Plus N.Nat8 ('N.S n))
-fin9 :: Fin (N.Plus N.Nat9 ('N.S n))
+fin0 :: Fin (N.Plus N.Nat0 ('S n))
+fin1 :: Fin (N.Plus N.Nat1 ('S n))
+fin2 :: Fin (N.Plus N.Nat2 ('S n))
+fin3 :: Fin (N.Plus N.Nat3 ('S n))
+fin4 :: Fin (N.Plus N.Nat4 ('S n))
+fin5 :: Fin (N.Plus N.Nat5 ('S n))
+fin6 :: Fin (N.Plus N.Nat6 ('S n))
+fin7 :: Fin (N.Plus N.Nat7 ('S n))
+fin8 :: Fin (N.Plus N.Nat8 ('S n))
+fin9 :: Fin (N.Plus N.Nat9 ('S n))
 
-fin0 = Z
-fin1 = S fin0
-fin2 = S fin1
-fin3 = S fin2
-fin4 = S fin3
-fin5 = S fin4
-fin6 = S fin5
-fin7 = S fin6
-fin8 = S fin7
-fin9 = S fin8
+fin0 = FZ
+fin1 = FS fin0
+fin2 = FS fin1
+fin3 = FS fin2
+fin4 = FS fin3
+fin5 = FS fin4
+fin6 = FS fin5
+fin7 = FS fin6
+fin8 = FS fin7
+fin9 = FS fin8
diff --git a/src/Data/Fin/Enum.hs b/src/Data/Fin/Enum.hs
--- a/src/Data/Fin/Enum.hs
+++ b/src/Data/Fin/Enum.hs
@@ -28,8 +28,8 @@
 import Prelude hiding (Enum (..))
 
 import Data.Bifunctor (bimap)
-import Data.Fin       (Fin)
-import Data.Nat       (Nat)
+import Data.Fin       (Fin (..))
+import Data.Nat       (Nat (..))
 import Data.Proxy     (Proxy (..))
 import GHC.Generics   ((:+:) (..), M1 (..), U1 (..), V1)
 
@@ -106,7 +106,7 @@
     EnumSizeRep (a :+: b )   n = EnumSizeRep a (EnumSizeRep b n)
     EnumSizeRep V1           n = n
     EnumSizeRep (M1 _d _c a) n = EnumSizeRep a n
-    EnumSizeRep U1           n = 'N.S n
+    EnumSizeRep U1           n = 'S n
     -- No instance for K1 or :*:
 
 -------------------------------------------------------------------------------
@@ -139,8 +139,8 @@
     gfromSkip _ n = n
 
 instance GFromRep U1 where
-    gfromRep U1 _ = F.Z
-    gfromSkip _ n = F.S n
+    gfromRep U1 _ = FZ
+    gfromSkip _ n = FS n
 
 -------------------------------------------------------------------------------
 -- To
@@ -166,5 +166,5 @@
     gtoRep n _ k = k n
 
 instance GToRep U1 where
-    gtoRep F.Z     s _ = s U1
-    gtoRep (F.S n) _ k = k n
+    gtoRep FZ     s _ = s U1
+    gtoRep (FS n) _ k = k n
diff --git a/src/Data/Type/Nat/LE/ReflStep.hs b/src/Data/Type/Nat/LE/ReflStep.hs
--- a/src/Data/Type/Nat/LE/ReflStep.hs
+++ b/src/Data/Type/Nat/LE/ReflStep.hs
@@ -124,9 +124,8 @@
 
 -- | \(\forall n\, m\, p : \mathbb{N}, n \le m \to m \le p \to n \le p \)
 leTrans :: LEProof n m -> LEProof m p -> LEProof n p
-leTrans LERefl     q          = q
-leTrans p          LERefl     = p
-leTrans (LEStep p) (LEStep q) = LEStep $ leTrans p $ leStepL q
+leTrans p LERefl     = p
+leTrans p (LEStep q) = LEStep $ leTrans p q
 
 -- | \(\forall n\, m : \mathbb{N}, \neg (n \le m) \to 1 + m \le n \)
 leSwap :: forall n m. (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof ('S m) n
diff --git a/test/Inspection.hs b/test/Inspection.hs
--- a/test/Inspection.hs
+++ b/test/Inspection.hs
@@ -6,6 +6,7 @@
 {-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-}
 module Main (main) where
 
+import Data.Fin           (Fin (..))
 import Data.Function      (fix)
 import Data.Proxy         (Proxy (..))
 import Data.Tagged        (Tagged (..), retag)
@@ -51,9 +52,9 @@
 lhsEnum = E.gfrom
 
 rhsEnum :: Ordering' -> F.Fin N.Nat3
-rhsEnum LT' = F.Z
-rhsEnum EQ' = F.S F.Z
-rhsEnum GT' = F.S (F.S F.Z)
+rhsEnum LT' = FZ
+rhsEnum EQ' = FS FZ
+rhsEnum GT' = FS (FS FZ)
 
 inspect $ 'lhsEnum ==- 'rhsEnum