diff --git a/src/Data/Type/Natural/Core.hs b/src/Data/Type/Natural/Core.hs
--- a/src/Data/Type/Natural/Core.hs
+++ b/src/Data/Type/Natural/Core.hs
@@ -19,6 +19,7 @@
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE NoStarIsType #-}
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
 
 module Data.Type.Natural.Core
@@ -73,7 +74,6 @@
 import GHC.TypeNats
 import Math.NumberTheory.Logarithms (naturalLog2)
 import Numeric.Natural (Natural)
-import Proof.Propositional (Empty)
 import Type.Reflection (Typeable)
 import Unsafe.Coerce (unsafeCoerce)
 
@@ -132,7 +132,7 @@
 
 equalAbsurdFromBool ::
   (x === y) ~ 'False => x :~: y -> a
-equalAbsurdFromBool = \case
+equalAbsurdFromBool = \case {}
 
 type family a === b where
   a === a = 'True
diff --git a/src/Data/Type/Natural/Lemma/Order.hs b/src/Data/Type/Natural/Lemma/Order.hs
--- a/src/Data/Type/Natural/Lemma/Order.hs
+++ b/src/Data/Type/Natural/Lemma/Order.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE ExplicitForAll #-}
 {-# LANGUAGE ExplicitNamespaces #-}
@@ -157,7 +158,6 @@
     start,
     sym,
     trans,
-    withRefl,
     (===),
     (=~=),
   )
@@ -267,8 +267,6 @@
 
 newtype LeqWitPf n = LeqWitPf {leqWitPf :: forall m. SNat m -> IsTrue (n <=? m) -> DiffNat n m}
 
-newtype LeqStepPf n = LeqStepPf {leqStepPf :: forall m l. SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m)}
-
 succDiffNat :: SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m)
 succDiffNat _ _ (DiffNat n m) = gcastWith (plusSuccL n m) $ DiffNat (sSucc n) m
 
@@ -302,16 +300,6 @@
 sLeqCongR :: SNat a -> b :~: c -> (a <= b) :~: (a <= c)
 sLeqCongR _ Refl = Refl
 
-newtype LTSucc n = LTSucc {proofLTSucc :: CmpNat n (Succ n) :~: 'LT}
-
-newtype CmpSuccStepR n = CmpSuccStepR
-  { proofCmpSuccStepR ::
-      forall m.
-      SNat m ->
-      CmpNat n m :~: 'LT ->
-      CmpNat n (Succ m) :~: 'LT
-  }
-
 newtype LeqViewRefl n = LeqViewRefl {proofLeqViewRefl :: LeqView n n}
 
 leqToCmp ::
@@ -355,25 +343,7 @@
 leqNeqToLT a b aLEQb aNEQb = either (absurd . aNEQb) id $ leqToCmp a b aLEQb
 
 succLeqToLT :: SNat a -> SNat b -> IsTrue (S a <=? b) -> CmpNat a b :~: 'LT
-succLeqToLT a b saLEQb =
-  case leqWitness (sSucc a) b saLEQb of
-    DiffNat _ k ->
-      let aLEQb =
-            leqStep a b (sSucc k) $
-              start (a %+ sSucc k)
-                === sSucc (a %+ k) `because` plusSuccR a k
-                === sSucc a %+ k `because` sym (plusSuccL a k)
-                =~= b
-          aNEQb aeqb =
-            succNonCyclic k $
-              plusEqCancelL a (sSucc k) sZero $
-                start (a %+ sSucc k)
-                  === sSucc (a %+ k) `because` plusSuccR a k
-                  === sSucc a %+ k `because` sym (plusSuccL a k)
-                  =~= b
-                  === a `because` sym aeqb
-                  === a %+ sZero `because` sym (plusZeroR a)
-       in leqNeqToLT a b aLEQb aNEQb
+succLeqToLT _ _ Witness = Refl
 
 ltToLeq ::
   SNat a ->
@@ -387,11 +357,7 @@
   SNat b ->
   CmpNat a b :~: 'GT ->
   IsTrue (b <=? a)
-gtToLeq n m nGTm =
-  ltToLeq m n $
-    start (sCmpNat m n) === sFlipOrdering (sCmpNat n m) `because` sym (flipCmpNat n m)
-      === sFlipOrdering SGT `because` congFlipOrdering nGTm
-      =~= SLT
+gtToLeq _ _ Refl = Witness
 
 congFlipOrdering ::
   a :~: b -> FlipOrdering a :~: FlipOrdering b
@@ -402,27 +368,17 @@
   SNat b ->
   CmpNat a b :~: 'LT ->
   IsTrue (Succ a <=? b)
-ltToSuccLeq n m nLTm =
-  leqNeqToSuccLeq n m (ltToLeq n m nLTm) (ltToNeq n m nLTm)
+ltToSuccLeq _ _ Refl = Witness
 
 cmpZero :: SNat a -> CmpNat 0 (Succ a) :~: 'LT
-cmpZero sn =
-  leqToLT sZero (sSucc sn) $
-    leqStep (sSucc sZero) (sSucc sn) sn $
-      start (sSucc sZero %+ sn)
-        === sSucc (sZero %+ sn) `because` plusSuccL sZero sn
-        === sSucc sn `because` succCong (plusZeroL sn)
+cmpZero _ = Refl
 
 leqToGT ::
   SNat a ->
   SNat b ->
   IsTrue (Succ b <=? a) ->
   CmpNat a b :~: 'GT
-leqToGT a b sbLEQa =
-  start (sCmpNat a b)
-    === sFlipOrdering (sCmpNat b a) `because` sym (flipCmpNat b a)
-    === sFlipOrdering SLT `because` congFlipOrdering (leqToLT b a sbLEQa)
-    =~= SGT
+leqToGT _ _ Witness = Refl
 
 cmpZero' :: SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
 cmpZero' n =
@@ -449,57 +405,13 @@
           === SLT `because` cmp0nLT
 
 ltRightPredSucc :: SNat a -> SNat b -> CmpNat a b :~: 'LT -> b :~: Succ (Pred b)
-ltRightPredSucc a b aLTb =
-  case zeroOrSucc b of
-    IsZero -> absurd $ zeroNoLT a aLTb
-    IsSucc b' ->
-      sym $
-        start (sSucc (sPred b))
-          =~= sSucc (sPred (sSucc b'))
-          === sSucc b' `because` succCong (predSucc b')
-          =~= b
+ltRightPredSucc _ _ Refl = Refl
 
 cmpSucc :: SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
-cmpSucc n m =
-  case sCmpNat n m of
-    SEQ ->
-      let nEQm = eqToRefl n m Refl
-       in sym $ eqlCmpEQ (sSucc n) (sSucc m) $ succCong nEQm
-    SLT -> case leqWitness (sSucc n) m $ ltToSuccLeq n m Refl of
-      DiffNat _ k ->
-        sym $
-          succLeqToLT (sSucc n) (sSucc m) $
-            leqStep (sSucc (sSucc n)) (sSucc m) k $
-              start (sSucc (sSucc n) %+ k)
-                === sSucc (sSucc n %+ k) `because` plusSuccL (sSucc n) k
-                =~= sSucc m
-    SGT -> case leqWitness (sSucc m) n $ ltToSuccLeq m n (sym $ flipCmpNat n m) of
-      DiffNat _ k ->
-        let pf =
-              ( succLeqToLT (sSucc m) (sSucc n) $
-                  leqStep (sSucc (sSucc m)) (sSucc n) k $
-                    start (sSucc (sSucc m) %+ k)
-                      === sSucc (sSucc m %+ k) `because` plusSuccL (sSucc m) k
-                      =~= sSucc n
-              )
-         in start (sCmpNat n m)
-              =~= SGT
-              =~= sFlipOrdering SLT
-              === sFlipOrdering (sCmpNat (sSucc m) (sSucc n)) `because` congFlipOrdering (sym pf)
-              === sCmpNat (sSucc n) (sSucc m) `because` flipCmpNat (sSucc m) (sSucc n)
+cmpSucc _ _ = Refl
 
 ltSucc :: SNat a -> CmpNat a (Succ a) :~: 'LT
-ltSucc = proofLTSucc . induction base step
-  where
-    base :: LTSucc 0
-    base = LTSucc $ cmpZero (sZero :: SNat 0)
-
-    step :: SNat n -> LTSucc n -> LTSucc (Succ n)
-    step n (LTSucc ih) =
-      LTSucc $
-        start (sCmpNat (sSucc n) (sSucc (sSucc n)))
-          === sCmpNat n (sSucc n) `because` sym (cmpSucc n (sSucc n))
-          === SLT `because` ih
+ltSucc _ = Refl
 
 cmpSuccStepR ::
   forall n m.
@@ -507,21 +419,7 @@
   SNat m ->
   CmpNat n m :~: 'LT ->
   CmpNat n (Succ m) :~: 'LT
-cmpSuccStepR = \sn -> proofCmpSuccStepR (induction base step sn) @m
-  where
-    base :: CmpSuccStepR 0
-    base = CmpSuccStepR $ \m _ -> cmpZero m
-
-    step :: SNat x -> CmpSuccStepR x -> CmpSuccStepR (Succ x)
-    step n (CmpSuccStepR ih) = CmpSuccStepR $ \m snltm ->
-      case zeroOrSucc m of
-        IsZero -> absurd $ zeroNoLT (sSucc n) snltm
-        IsSucc m' ->
-          let nLTm' = trans (cmpSucc n m') snltm
-           in start (sCmpNat (sSucc n) (sSucc m))
-                =~= sCmpNat (sSucc n) (sSucc (sSucc m'))
-                === sCmpNat n (sSucc m') `because` sym (cmpSucc n (sSucc m'))
-                === SLT `because` ih m' nLTm'
+cmpSuccStepR _ _ Refl = Refl
 
 ltSuccLToLT ::
   SNat n ->
@@ -541,14 +439,7 @@
   SNat b ->
   IsTrue (Succ a <=? b) ->
   CmpNat a b :~: 'LT
-leqToLT n m snLEQm =
-  case leqToCmp (sSucc n) m snLEQm of
-    Left eql ->
-      withRefl eql $
-        start (sCmpNat n m)
-          =~= sCmpNat n (sSucc n)
-          === SLT `because` ltSucc n
-    Right nLTm -> ltSuccLToLT n m nLTm
+leqToLT _ _ Witness = Refl
 
 leqZero :: SNat n -> IsTrue (0 <=? n)
 leqZero _ = Witness
@@ -589,25 +480,14 @@
     step :: SNat x -> LeqWitPf x -> LeqWitPf (Succ x)
     step (n :: SNat x) (LeqWitPf ih) = LeqWitPf $ \m snLEQm ->
       case viewLeq (sSucc n) m snLEQm of
+#if !MIN_VERSION_ghc(9,2,0)
         LeqZero _ -> absurd $ succNonCyclic n Refl
+#endif
         LeqSucc (_ :: SNat n') pm nLEQpm ->
           succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: x) pm nLEQpm
 
 leqStep :: forall n m l. SNat n -> SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m)
-leqStep sn = leqStepPf (induction base step sn) @m @l
-  where
-    base :: LeqStepPf 0
-    base = LeqStepPf $ \k _ _ -> leqZero k
-
-    step :: forall k. SNat k -> LeqStepPf k -> LeqStepPf (Succ k)
-    step n (LeqStepPf ih) =
-      LeqStepPf $ \k l snPlEqk ->
-        let kEQspk =
-              start k
-                === sSucc n %+ l `because` sym snPlEqk
-                === sSucc (n %+ l) `because` plusSuccL n l
-            pk = n %+ l
-         in coerceLeqR (sSucc n) (sym kEQspk) $ leqSucc n pk $ ih pk l Refl
+leqStep _ _ _ Refl = Witness
 
 leqNeqToSuccLeq :: SNat n -> SNat m -> IsTrue (n <=? m) -> (n :~: m -> Void) -> IsTrue (Succ n <=? m)
 leqNeqToSuccLeq n m nLEQm nNEQm =
@@ -623,47 +503,22 @@
               =~= m
 
 leqRefl :: SNat n -> IsTrue (n <=? n)
-leqRefl sn = leqStep sn sn sZero (plusZeroR sn)
+leqRefl _ = Witness
 
 leqSuccStepR :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)
-leqSuccStepR n m nLEQm =
-  case leqWitness n m nLEQm of
-    DiffNat _ k ->
-      leqStep n (sSucc m) (sSucc k) $
-        start (n %+ sSucc k) === sSucc (n %+ k) `because` plusSuccR n k =~= sSucc m
+leqSuccStepR _ _ Witness = Witness
 
 leqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m)
-leqSuccStepL n m snLEQm =
-  leqTrans n (sSucc n) m (leqSuccStepR n n $ leqRefl n) snLEQm
+leqSuccStepL _ _ Witness = Witness
 
 leqReflexive :: SNat n -> SNat m -> n :~: m -> IsTrue (n <=? m)
-leqReflexive n _ Refl = leqRefl n
+leqReflexive _ _ Refl = Witness
 
 leqTrans :: SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue (m <=? l) -> IsTrue (n <=? l)
-leqTrans n m k nLEm mLEk =
-  case leqWitness n m nLEm of
-    DiffNat _ mMn -> case leqWitness m k mLEk of
-      DiffNat _ kMn -> leqStep n k (mMn %+ kMn) (sym $ plusAssoc n mMn kMn)
+leqTrans _ _ _ Witness Witness = Witness
 
 leqAntisymm :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m
-leqAntisymm n m nLEm mLEn =
-  case (leqWitness n m nLEm, leqWitness m n mLEn) of
-    (DiffNat _ mMn, DiffNat _ nMm) ->
-      let pEQ0 =
-            plusEqCancelL n (mMn %+ nMm) sZero $
-              start (n %+ (mMn %+ nMm))
-                === (n %+ mMn) %+ nMm
-                  `because` sym (plusAssoc n mMn nMm)
-                =~= m %+ nMm
-                =~= n
-                === n %+ sZero
-                  `because` sym (plusZeroR n)
-          nMmEQ0 = plusEqZeroL mMn nMm pEQ0
-       in sym $
-            start m
-              =~= n %+ mMn
-              === n %+ sZero `because` plusCongR n nMmEQ0
-              === n `because` plusZeroR n
+leqAntisymm _ _ Witness Witness = Refl
 
 plusMonotone ::
   SNat n ->
@@ -673,31 +528,10 @@
   IsTrue (n <=? m) ->
   IsTrue (l <=? k) ->
   IsTrue ((n + l) <=? (m + k))
-plusMonotone n m l k nLEm lLEk =
-  case (leqWitness n m nLEm, leqWitness l k lLEk) of
-    (DiffNat _ mMINn, DiffNat _ kMINl) ->
-      let r = mMINn %+ kMINl
-       in leqStep (n %+ l) (m %+ k) r $
-            start (n %+ l %+ r)
-              === n %+ (l %+ r)
-                `because` plusAssoc n l r
-              =~= n %+ (l %+ (mMINn %+ kMINl))
-              === n %+ (l %+ (kMINl %+ mMINn))
-                `because` plusCongR n (plusCongR l (plusComm mMINn kMINl))
-              === n %+ ((l %+ kMINl) %+ mMINn)
-                `because` plusCongR n (sym $ plusAssoc l kMINl mMINn)
-              =~= n %+ (k %+ mMINn)
-              === n %+ (mMINn %+ k)
-                `because` plusCongR n (plusComm k mMINn)
-              === n %+ mMINn %+ k
-                `because` sym (plusAssoc n mMINn k)
-              =~= m %+ k
+plusMonotone _ _ _ _ Witness Witness = Witness
 
 leqZeroElim :: SNat n -> IsTrue (n <=? 0) -> n :~: 0
-leqZeroElim n nLE0 =
-  case viewLeq n sZero nLE0 of
-    LeqZero _ -> Refl
-    LeqSucc _ pZ _ -> absurd $ succNonCyclic pZ Refl
+leqZeroElim _ Witness = Refl
 
 plusMonotoneL ::
   SNat n ->
@@ -705,7 +539,7 @@
   SNat l ->
   IsTrue (n <=? m) ->
   IsTrue ((n + l) <=? (m + l))
-plusMonotoneL n m l leq = plusMonotone n m l l leq (leqRefl l)
+plusMonotoneL _ _ _ Witness = Witness
 
 plusMonotoneR ::
   SNat n ->
@@ -713,13 +547,13 @@
   SNat l ->
   IsTrue (m <=? l) ->
   IsTrue ((n + m) <=? (n + l))
-plusMonotoneR n m l leq = plusMonotone n n m l (leqRefl n) leq
+plusMonotoneR _ _ _ Witness = Witness
 
 plusLeqL :: SNat n -> SNat m -> IsTrue (n <=? (n + m))
-plusLeqL n m = leqStep n (n %+ m) m Refl
+plusLeqL _ _  = Witness
 
 plusLeqR :: SNat n -> SNat m -> IsTrue (m <=? (n + m))
-plusLeqR n m = leqStep m (n %+ m) n $ plusComm m n
+plusLeqR _ _ = Witness
 
 plusCancelLeqR ::
   SNat n ->
@@ -727,17 +561,7 @@
   SNat l ->
   IsTrue ((n + l) <=? (m + l)) ->
   IsTrue (n <=? m)
-plusCancelLeqR n m l nlLEQml =
-  case leqWitness (n %+ l) (m %+ l) nlLEQml of
-    DiffNat _ k ->
-      let pf =
-            plusEqCancelR (n %+ k) m l $
-              start ((n %+ k) %+ l)
-                === n %+ (k %+ l) `because` plusAssoc n k l
-                === n %+ (l %+ k) `because` plusCongR n (plusComm k l)
-                === n %+ l %+ k `because` sym (plusAssoc n l k)
-                =~= m %+ l
-       in leqStep n m k pf
+plusCancelLeqR _ _ _ Witness = Witness
 
 plusCancelLeqL ::
   SNat n ->
@@ -745,20 +569,14 @@
   SNat l ->
   IsTrue ((n + m) <=? (n + l)) ->
   IsTrue (m <=? l)
-plusCancelLeqL n m l nmLEQnl =
-  plusCancelLeqR m l n $
-    coerceLeqL (plusComm n m) (l %+ n) $
-      coerceLeqR (n %+ m) (plusComm n l) nmLEQnl
+plusCancelLeqL _ _ _ Witness = Witness
 
 succLeqZeroAbsurd :: SNat n -> IsTrue (S n <=? 0) -> Void
 succLeqZeroAbsurd n leq =
   succNonCyclic n (leqZeroElim (sSucc n) leq)
 
 succLeqZeroAbsurd' :: SNat n -> (S n <=? 0) :~: 'False
-succLeqZeroAbsurd' n =
-  case sSucc n %<=? sZero of
-    STrue -> absurd $ succLeqZeroAbsurd n Witness
-    SFalse -> Refl
+succLeqZeroAbsurd' _ = Refl
 
 succLeqAbsurd :: SNat n -> IsTrue (S n <=? n) -> Void
 succLeqAbsurd n snLEQn =
@@ -768,17 +586,10 @@
       === SEQ `because` eqlCmpEQ n n Refl
 
 succLeqAbsurd' :: SNat n -> (S n <=? n) :~: 'False
-succLeqAbsurd' n =
-  case sSucc n %<=? n of
-    STrue -> absurd $ succLeqAbsurd n Witness
-    SFalse -> Refl
+succLeqAbsurd' _ = Refl
 
-notLeqToLeq :: ((n <=? m) ~ 'False) => SNat n -> SNat m -> IsTrue (m <=? n)
-notLeqToLeq n m =
-  case sCmpNat n m of
-    SLT -> eliminate $ ltToLeq n m Refl
-    SEQ -> eliminate $ leqReflexive n m $ eqToRefl n m Refl
-    SGT -> gtToLeq n m Refl
+notLeqToLeq :: forall n m. ((n <=? m) ~ 'False) => SNat n -> SNat m -> IsTrue (m <=? n)
+notLeqToLeq _ _ = Witness
 
 leqSucc' :: SNat n -> SNat m -> (n <=? m) :~: (Succ n <=? Succ m)
 leqSucc' _ _ = Refl
@@ -841,12 +652,15 @@
             SFalse -> lLEQm
 
 leqToMax :: SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
-leqToMax n m nLEQm =
-  leqAntisymm (sMax n m) m (maxLeast m n m nLEQm (leqRefl m)) (maxLeqR n m)
+leqToMax n m Witness =
+  case n %>=? m of
+    STrue -> Refl
+    SFalse -> Refl
 
 geqToMax :: SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
-geqToMax n m mLEQn =
-  leqAntisymm (sMax n m) n (maxLeast n n m (leqRefl n) mLEQn) (maxLeqL n m)
+geqToMax n m Witness =
+  case n %>=? m of
+    STrue -> Refl
 
 maxComm :: SNat n -> SNat m -> Max n m :~: Max m n
 maxComm n m =
diff --git a/tests/Data/Type/Natural/Lemma/OrderSpec.hs b/tests/Data/Type/Natural/Lemma/OrderSpec.hs
new file mode 100644
--- /dev/null
+++ b/tests/Data/Type/Natural/Lemma/OrderSpec.hs
@@ -0,0 +1,476 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Data.Type.Natural.Lemma.OrderSpec where
+
+import Control.Exception (SomeException (..), evaluate, try)
+import Data.Functor ((<&>))
+import Data.List (isInfixOf, isPrefixOf)
+import Data.Type.Natural
+import Data.Type.Natural.Lemma.Order
+import Data.Void (Void)
+import Proof.Propositional (IsTrue (Witness))
+import Shared ()
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit
+import Test.Tasty.QuickCheck
+import Type.Reflection
+import Unsafe.Coerce (unsafeCoerce)
+
+someNat' :: NonNegative Integer -> SomeSNat
+someNat' = toSomeSNat . fromInteger . getNonNegative
+
+data SomeLeqNat where
+  MkSomeLeqNat :: n <= m => SNat n -> SNat m -> SomeLeqNat
+
+data SomeLtNat where
+  MkSomeLtNat ::
+    CmpNat n m ~ 'LT =>
+    SNat n ->
+    SNat m ->
+    SomeLtNat
+
+data SomeLneqNat where
+  MkSomeLneqNat ::
+    n < m =>
+    SNat n ->
+    SNat m ->
+    SomeLneqNat
+
+data SomeGtNat where
+  MkSomeGtNat ::
+    CmpNat n m ~ 'GT =>
+    SNat n ->
+    SNat m ->
+    SomeGtNat
+
+deriving instance Show SomeLeqNat
+
+deriving instance Show SomeLtNat
+
+deriving instance Show SomeLneqNat
+
+deriving instance Show SomeGtNat
+
+instance Arbitrary SomeLeqNat where
+  arbitrary = do
+    SomeSNat n <- someNat' <$> arbitrary
+    SomeSNat m <- someNat' <$> arbitrary
+    case n %<=? m of
+      STrue -> pure $ MkSomeLeqNat n m
+      SFalse ->
+        case m %<=? n of
+          STrue -> pure $ MkSomeLeqNat m n
+          SFalse -> error "Impossible!"
+
+instance Arbitrary SomeLtNat where
+  arbitrary = do
+    MkSomeLeqNat (n :: SNat n) (m :: SNat m) <- arbitrary
+    let m' = Succ m
+    case sCmpNat n m' of
+      SLT -> pure $ MkSomeLtNat n m'
+      _ -> error "impossible"
+
+instance Arbitrary SomeLneqNat where
+  arbitrary = do
+    MkSomeLtNat (n :: SNat n) (m :: SNat m) <- arbitrary
+    let m' = Succ m
+    case n %<? m' of
+      STrue -> pure $ MkSomeLneqNat n m'
+      _ -> error "impossible"
+
+instance Arbitrary SomeGtNat where
+  arbitrary = do
+    MkSomeLeqNat (n :: SNat n) (m :: SNat m) <- arbitrary
+    let m' = Succ m
+    case sCmpNat m' n of
+      SGT -> pure $ MkSomeGtNat m' n
+      _ -> error "impossible"
+
+data SomeLeqView where
+  MkSomeLeqView :: LeqView n m -> SomeLeqView
+
+instance Show SomeLeqView where
+  showsPrec d (MkSomeLeqView (LeqZero n)) =
+    showParen (d > 10) $
+      showString "LeqZero "
+        . showsPrec 11 n
+  showsPrec d (MkSomeLeqView (LeqSucc n m w)) =
+    showParen (d > 10) $
+      showString "LeqSucc "
+        . showsPrec 11 n
+        . showChar ' '
+        . showsPrec 11 m
+        . showChar ' '
+        . showsPrec 11 w
+
+instance Arbitrary SomeLeqView where
+  arbitrary = sized $ \n ->
+    if n <= 0
+      then
+        arbitrary <&> \case
+          SomeSNat sn -> MkSomeLeqView (LeqZero sn)
+      else
+        arbitrary <&> \case
+          MkSomeLeqNat sn sm -> MkSomeLeqView $ LeqSucc sn sm Witness
+
+givesImpossibleVoid :: Void -> Property
+givesImpossibleVoid contradiction = ioProperty $ do
+  eith <- try @SomeException $ evaluate contradiction
+  case eith of
+    Left someE -> do
+      pure $
+        property $
+          "Impossible" `isPrefixOf` show someE
+            || "Non-exhaustive" `isInfixOf` show someE
+    Right {} -> pure $ property False
+
+test_Lemmas :: TestTree
+test_Lemmas =
+  testGroup
+    "Lemmas"
+    [ testProperty @(SomeLeqNat -> Property) "coerceLeqL terminates" $ \(MkSomeLeqNat (_ :: SNat n) sm) -> totalWitness $ coerceLeqL (Refl :: n :~: n) sm Witness
+    , testProperty @(SomeLeqNat -> Property) "coerceLeqR terminates" $ \(MkSomeLeqNat sn (_ :: SNat m)) -> totalWitness $ coerceLeqR sn (Refl :: m :~: m) Witness
+    , testProperty @(SomeSNat -> SomeSNat -> Property) "sLeqCong terminates" $
+        \(SomeSNat (_ :: SNat n)) (SomeSNat (_ :: SNat m)) ->
+          totalRefl $ sLeqCong (Refl @n) (Refl @m)
+    , testProperty @(SomeSNat -> SomeSNat -> Property) "succDiffNat terminates and gives the correct value" $
+        \(SomeSNat sn) (SomeSNat sm) ->
+          case succDiffNat sn (sn %+ sm) (DiffNat sn sm) of
+            DiffNat sns sms ->
+              toNatural (sns %+ sms)
+                === toNatural sn + toNatural sm + 1
+    , testProperty @(SomeSNat -> SomeSNat -> Property)
+        "compareCongR terminates"
+        $ \(SomeSNat a) (SomeSNat (_ :: SNat b)) ->
+          totalRefl $ compareCongR a (Refl @b)
+    , testProperty @(SomeLeqNat -> Property)
+        "leqToCmp works properly"
+        $ \case
+          MkSomeLeqNat a b ->
+            case leqToCmp a b Witness of
+              Left Refl -> toNatural a === toNatural b
+              Right Refl ->
+                property $ toNatural a < toNatural b
+    , testProperty @(SomeSNat -> Property)
+        "eqlCmpEQ terminates"
+        $ \(SomeSNat n) ->
+          totalRefl $ eqlCmpEQ n n Refl
+    , testProperty @(SomeSNat -> Property)
+        "eqToRefl terminates"
+        $ \(SomeSNat n) ->
+          totalRefl $ eqToRefl n n Refl
+    , testProperty @(SomeSNat -> SomeSNat -> Property)
+        "flipCmpNat terminates"
+        $ \(SomeSNat n) (SomeSNat m) ->
+          totalRefl $ flipCmpNat n m
+    , testProperty @(SomeSNat -> Property)
+        "ltToNeq works as expected"
+        $ \(SomeSNat n) ->
+          givesImpossibleVoid $
+            ltToNeq n n (unsafeCoerce $ Refl @()) Refl
+    , testProperty @(SomeLeqNat -> Property)
+        "leqNeqToLT terminates"
+        $ \(MkSomeLeqNat n m) ->
+          case n %~ m of
+            Equal -> discard
+            NonEqual ->
+              totalRefl $ leqNeqToLT n m Witness (\case {})
+    , testProperty @(SomeLeqNat -> Property)
+        "succLeqToLT terminates"
+        $ \(MkSomeLeqNat n' m) ->
+          case n' of
+            Succ n ->
+              totalRefl $ succLeqToLT n m Witness
+            _ -> discard
+    , testProperty @(SomeLtNat -> Property)
+        "ltToLeq terminates"
+        $ \(MkSomeLtNat n m) ->
+          totalWitness $ ltToLeq n m Refl
+    , testProperty @(SomeGtNat -> Property)
+        "gtToLeq terminates"
+        $ \(MkSomeGtNat n m) ->
+          totalWitness $ gtToLeq n m Refl
+    , testCase "congFlipOrdering" $ do
+        Refl <- evaluate (congFlipOrdering (Refl @( 'LT)))
+        Refl <- evaluate (congFlipOrdering (Refl @( 'GT)))
+        Refl <- evaluate (congFlipOrdering (Refl @( 'EQ)))
+        pure ()
+    , testProperty @(SomeLtNat -> Property) "ltToSuccLeq terminates" $ \(MkSomeLtNat n m) ->
+        totalWitness $ ltToSuccLeq n m Refl
+    , testProperty @(SomeSNat -> Property) "cmpZero terminates" $ \(SomeSNat n) ->
+        totalRefl $ cmpZero n
+    , testProperty @(SomeLeqNat -> Property) "leqToGT terminates" $ \(MkSomeLeqNat b0 a) ->
+        case b0 of
+          Succ b ->
+            totalRefl $ leqToGT a b Witness
+          Zero -> discard
+    , testProperty @(SomeSNat -> Property) "cmpZero' works as expected" $ \(SomeSNat n) ->
+        case n of
+          Zero -> cmpZero' n === Left Refl
+          Succ {} -> case cmpZero' n of
+            Right Refl -> property True
+            l -> counterexample ("Left Refl expected, but got: " <> show l) False
+    , testProperty @(SomeSNat -> Property)
+        "zeroNoLT works as expected"
+        $ \(SomeSNat n) ->
+          givesImpossibleVoid $ zeroNoLT n (unsafeCoerce $ Refl @())
+    , testProperty @(SomeLtNat -> Property) "ltRightPredSucc terminates" $ \(MkSomeLtNat a b) ->
+        totalRefl $ ltRightPredSucc a b Refl
+    , testProperty @(SomeSNat -> SomeSNat -> Property) "cmpSucc terminates" $ \(SomeSNat a) (SomeSNat b) ->
+        totalRefl $ cmpSucc a b
+    , testProperty @(SomeSNat -> Property) "ltSucc terminates" $ \(SomeSNat a) ->
+        totalRefl $ ltSucc a
+    , testProperty @(SomeLtNat -> Property) "cmpSuccStepR terminates" $ \(MkSomeLtNat a b) ->
+        totalRefl $ cmpSuccStepR a b Refl
+    , testProperty @(SomeLtNat -> Property) "ltSuccLToLT terminates" $ \(MkSomeLtNat a0 b) ->
+        case a0 of
+          Succ a -> totalRefl $ ltSuccLToLT a b Refl
+          Zero -> discard
+    , testProperty @(SomeLeqNat -> Property) "leqToLT terminates" $ \(MkSomeLeqNat a0 b) ->
+        case a0 of
+          Succ a -> totalRefl $ leqToLT a b Witness
+          Zero -> discard
+    , testProperty @(SomeSNat -> Property) "leqZero terminates" $ \(SomeSNat n) ->
+        totalWitness $ leqZero n
+    , testProperty @(SomeLeqNat -> Property) "leqSucc terminates" $ \(MkSomeLeqNat n m) ->
+        totalWitness $ leqSucc n m Witness
+    , testProperty @(SomeLeqView -> Property) "fromLeqView terminates" $ \(MkSomeLeqView lview) ->
+        totalWitness $ fromLeqView lview
+    , testProperty @(SomeSNat -> Property) "leqViewRefl works properly" $ \(SomeSNat sn) ->
+        case leqViewRefl sn of
+          LeqZero sn' ->
+            toNatural sn' === toNatural sn .&&. toNatural sn' === 0
+          LeqSucc sn' sm' Witness ->
+            toNatural sn' === toNatural sm'
+              .&&. toNatural sn' + 1 === toNatural sn
+    , testProperty @(SomeLeqNat -> Property) "viewLeq works properly" $ \(MkSomeLeqNat sn sm) ->
+        case viewLeq sn sm Witness of
+          LeqZero sm' ->
+            toNatural sn === 0 .&&. toNatural sm === toNatural sm'
+          LeqSucc sn' sm' Witness ->
+            toNatural sn' + 1 === toNatural sn
+              .&&. toNatural sm' + 1 === toNatural sm
+              .&&. toNatural sn' <= toNatural sm'
+    , testProperty @(SomeLeqNat -> Property) "leqWitness gives the difference as a witness" $
+        \(MkSomeLeqNat sn sm) ->
+          case leqWitness sn sm Witness of
+            DiffNat sn' delta ->
+              toNatural sn === toNatural sn'
+                .&&. toNatural sn' + toNatural delta === toNatural sm
+    , testProperty @(SomeSNat -> SomeSNat -> Property)
+        "leqStep terminates"
+        $ \(SomeSNat n) (SomeSNat l) ->
+          let m = n %+ l
+           in totalWitness $ leqStep n m l Refl
+    , testProperty @(SomeLeqNat -> Property) "leqNeqToSuccLeq terminates" $
+        \(MkSomeLeqNat n m) ->
+          case n %~ m of
+            Equal -> discard
+            NonEqual ->
+              totalWitness $ leqNeqToSuccLeq n m Witness (\case {})
+    , testProperty @(SomeSNat -> Property) "leqRefl terminates" $
+        \(SomeSNat n) ->
+          totalWitness $ leqRefl n
+    , testProperty @(SomeLeqNat -> Property) "leqSuccStepR and leqSuccStepL terminates" $
+        \(MkSomeLeqNat n m) ->
+          totalWitness (leqSuccStepR n m Witness)
+            .&&. case n of
+              Succ n' ->
+                label "leqSuccStepL tested" $
+                  totalWitness (leqSuccStepL n' m Witness)
+              _ -> property True
+    , testProperty @(SomeSNat -> Property) "leqReflexive terminates" $
+        \(SomeSNat n) ->
+          totalWitness $ leqReflexive n n Refl
+    , testProperty @(SomeLeqNat -> SomeSNat -> Property) "leqTrans terminates" $
+        \(MkSomeLeqNat (n :: SNat n) (m :: SNat m)) (SomeSNat (l0 :: SNat lMinsM)) ->
+          let l = m %+ l0
+           in case m %<=? l of
+                STrue ->
+                  totalWitness $
+                    leqTrans n m l Witness (Witness :: IsTrue (m <=? (m + lMinsM)))
+                SFalse -> error "impossible"
+    , testProperty @(SomeSNat -> Property) "leqAntisymm terminates" $
+        \(SomeSNat n) ->
+          totalRefl $ leqAntisymm n n Witness Witness
+    , testProperty @(SomeLeqNat -> SomeLeqNat -> Property) "plusMonotone terminates" $
+        \(MkSomeLeqNat n m) (MkSomeLeqNat l k) ->
+          totalWitness $ plusMonotone n m l k Witness Witness
+    , testCase "leqZeroElim terminates" $
+        leqZeroElim (sNat @0) Witness @?= Refl
+    , testProperty @(SomeLeqNat -> SomeSNat -> Property) "plusMonotoneL terminates" $
+        \(MkSomeLeqNat n m) (SomeSNat l) ->
+          totalWitness $ plusMonotoneL n m l Witness
+    , testProperty @(SomeLeqNat -> SomeSNat -> Property) "plusMonotoneR terminates" $
+        \(MkSomeLeqNat n m) (SomeSNat l) ->
+          totalWitness $ plusMonotoneR l n m Witness
+    , testProperty @(SomeSNat -> SomeSNat -> Property) "plusLeqL terminates" $
+        \(SomeSNat n) (SomeSNat m) ->
+          totalWitness $ plusLeqL n m
+    , testProperty @(SomeSNat -> SomeSNat -> Property) "plusLeqR terminates" $
+        \(SomeSNat n) (SomeSNat m) ->
+          totalWitness $ plusLeqR n m
+    , testProperty @(SomeLeqNat -> SomeSNat -> Property) "plusCancelLeqL terminates" $
+        \(MkSomeLeqNat (m :: SNat m) (l :: SNat l)) (SomeSNat n) ->
+          totalWitness $
+            plusCancelLeqR
+              n
+              m
+              l
+              (unsafeCoerce (Witness :: IsTrue (m <=? l)))
+    , testProperty @(SomeLeqNat -> SomeSNat -> Property) "plusCancelLeqR terminates" $
+        \(MkSomeLeqNat (n :: SNat n) (m :: SNat m)) (SomeSNat l) ->
+          totalWitness $
+            plusCancelLeqR
+              n
+              m
+              l
+              (unsafeCoerce (Witness :: IsTrue (n <=? m)))
+    , testProperty @(SomeSNat -> Property) "succLeqZeroAbsurd works properly" $ \(SomeSNat n) ->
+        givesImpossibleVoid $ succLeqZeroAbsurd n (unsafeCoerce Witness)
+    , testProperty @(SomeSNat -> Property) "succLeqZeroAbsurd' works properly" $ \(SomeSNat n) ->
+        totalRefl $ succLeqZeroAbsurd' n
+    , testProperty @(SomeSNat -> Property) "succLeqAbsurd works properly" $ \(SomeSNat n) ->
+        givesImpossibleVoid $ succLeqAbsurd n (unsafeCoerce Witness)
+    , testProperty @(SomeSNat -> Property) "succLeqAbsurd' works properly" $ \(SomeSNat n) ->
+        totalRefl $ succLeqAbsurd' n
+    , testProperty @(SomeGtNat -> Property)
+        "notLeqToLeq terminates"
+        $ \(MkSomeGtNat n m) ->
+          case n %<=? m of
+            STrue -> error "impossible!"
+            SFalse ->
+              totalWitness $ notLeqToLeq n m
+    , testProperty
+        @(SomeSNat -> SomeSNat -> Property)
+        "leqSucc' terminates"
+        $ \(SomeSNat n) (SomeSNat m) ->
+          totalRefl $ leqSucc' n m
+    , testProperty @(SomeLeqNat -> Property) "leqToMin terminates" $
+        \(MkSomeLeqNat n m) ->
+          totalRefl $ leqToMin n m Witness
+    , testProperty @(SomeLeqNat -> Property) "geqToMin terminates" $
+        \(MkSomeLeqNat n m) ->
+          totalRefl $ geqToMin m n Witness
+    , testProperty @(SomeSNat -> SomeSNat -> Property) "minComm terminates" $
+        \(SomeSNat n) (SomeSNat m) ->
+          totalRefl $ minComm n m
+    , testProperty @(SomeSNat -> SomeSNat -> Property) "minLeqL terminates" $
+        \(SomeSNat n) (SomeSNat m) ->
+          totalWitness $ minLeqL n m
+    , testProperty @(SomeSNat -> SomeSNat -> Property) "minLeqR terminates" $
+        \(SomeSNat n) (SomeSNat m) ->
+          totalWitness $ minLeqR n m
+    , testProperty @(SomeLeqNat -> SomeSNat -> Property) "minLargest terminates" $
+        \(MkSomeLeqNat l n) (SomeSNat lm) ->
+          let m = l %+ lm
+           in totalWitness $
+                minLargest l n m Witness (unsafeCoerce Witness)
+    , testProperty @(SomeLeqNat -> Property) "leqToMax termaxates" $
+        \(MkSomeLeqNat n m) ->
+          totalRefl $ leqToMax n m Witness
+    , testProperty @(SomeLeqNat -> Property) "geqToMax termaxates" $
+        \(MkSomeLeqNat n m) ->
+          totalRefl $ geqToMax m n Witness
+    , testProperty @(SomeSNat -> SomeSNat -> Property) "maxComm termaxates" $
+        \(SomeSNat n) (SomeSNat m) ->
+          totalRefl $ maxComm n m
+    , testProperty @(SomeSNat -> SomeSNat -> Property) "maxLeqL termaxates" $
+        \(SomeSNat n) (SomeSNat m) ->
+          totalWitness $ maxLeqL n m
+    , testProperty @(SomeSNat -> SomeSNat -> Property) "maxLeqR termaxates" $
+        \(SomeSNat n) (SomeSNat m) ->
+          totalWitness $ maxLeqR n m
+    , testProperty @(SomeLeqNat -> Property) "maxLeast termaxates" $
+        \(MkSomeLeqNat n l) ->
+          forAll (elements [0 .. toNatural l]) $ \m0 ->
+            case toSomeSNat m0 of
+              SomeSNat m ->
+                totalWitness $
+                  maxLeast l n m Witness (unsafeCoerce Witness)
+    , testProperty @(SomeSNat -> SomeSNat -> Property) "lneqSuccLeq terminates" $
+        \(SomeSNat n) (SomeSNat m) ->
+          totalRefl $ lneqSuccLeq n m
+    , testProperty @(SomeSNat -> SomeSNat -> Property) "lneqReversed terminates" $
+        \(SomeSNat n) (SomeSNat m) ->
+          totalRefl $ lneqReversed n m
+    , testProperty @(SomeLneqNat -> Property) "lneqToLT terminates" $
+        \(MkSomeLneqNat n m) ->
+          totalRefl $ lneqToLT n m Witness
+    , testProperty @(SomeLtNat -> Property) "ltToLneq terminates" $
+        \(MkSomeLtNat n m) ->
+          totalWitness $ ltToLneq n m Refl
+    , testProperty @(SomeSNat -> Property) "lneqZero terminates" $
+        \(SomeSNat n) -> totalWitness $ lneqZero n
+    , testProperty @(SomeSNat -> Property) "lneqSucc terminates" $
+        \(SomeSNat n) -> totalWitness $ lneqSucc n
+    , testProperty @(SomeSNat -> SomeSNat -> Property) "succLneqSucc terminates" $
+        \(SomeSNat n) (SomeSNat m) -> totalRefl $ succLneqSucc n m
+    , testProperty @(SomeLneqNat -> Property) "lneqRightPredSucc terminates" $
+        \(MkSomeLneqNat n m) ->
+          totalRefl $ lneqRightPredSucc n m Witness
+    , testProperty @(SomeLneqNat -> Property) "lneqSuccStepL and lneqSuccStepR works properly" $
+        \(MkSomeLneqNat n m) ->
+          conjoin
+            [ totalWitness (lneqSuccStepR n m Witness)
+            , case n of
+                Succ n' ->
+                  label "lneqSuccStepL checked" $
+                    totalWitness (lneqSuccStepL n' m Witness)
+                Zero -> property True
+            ]
+    , testProperty @(SomeLneqNat -> SomeLneqNat -> Property)
+        "plusStrictMonotone terminates"
+        $ \(MkSomeLneqNat n m) (MkSomeLneqNat l k) ->
+          totalWitness $
+            plusStrictMonotone n m l k Witness Witness
+    , testProperty @(SomeSNat -> Property) "maxZeroL terminates" $
+        \(SomeSNat n) -> totalRefl $ maxZeroL n
+    , testProperty @(SomeSNat -> Property) "maxZeroR terminates" $
+        \(SomeSNat n) -> totalRefl $ maxZeroR n
+    , testProperty @(SomeSNat -> Property) "minZeroL terminates" $
+        \(SomeSNat n) -> totalRefl $ minZeroL n
+    , testProperty @(SomeSNat -> Property) "minZeroR terminates" $
+        \(SomeSNat n) -> totalRefl $ minZeroR n
+    , testProperty @(SomeLeqNat -> Property) "minusSucc terminates" $
+        \(MkSomeLeqNat m n) ->
+          totalRefl $ minusSucc n m Witness
+    , testProperty @(SomeSNat -> Property) "lneqZeroAbsurd is absurd" $
+        \(SomeSNat n) ->
+          givesImpossibleVoid $
+            lneqZeroAbsurd n $ unsafeCoerce Witness
+    , testProperty @(SomeLeqNat -> Property)
+        "minusPlus terminates"
+        $ \(MkSomeLeqNat m n) ->
+          totalRefl $
+            minusPlus n m Witness
+    , testProperty @(SomeSNat -> SomeSNat -> Property)
+        "minPlusTruncMinus terminates"
+        $ \(SomeSNat n) (SomeSNat m) ->
+          totalRefl $ minPlusTruncMinus n m
+    , testProperty @(SomeSNat -> SomeSNat -> Property)
+        "truncMinusLeq terminates"
+        $ \(SomeSNat n) (SomeSNat m) ->
+          totalWitness $ truncMinusLeq n m
+    ]
+
+totalWitness :: IsTrue p -> Property
+totalWitness w =
+  counterexample "Witness is not totalRefl!" $
+    within
+      10000
+      ( (case w of Witness -> True :: Bool) ::
+          Bool
+      )
+
+totalRefl :: a :~: b -> Property
+totalRefl = total
diff --git a/type-natural.cabal b/type-natural.cabal
--- a/type-natural.cabal
+++ b/type-natural.cabal
@@ -1,96 +1,105 @@
 cabal-version: >=1.10
 name:          type-natural
-version:       1.1.0.0
+version:       1.1.0.1
 license:       BSD3
 license-file:  LICENSE
 copyright:     (C) Hiromi ISHII 2013-2014
 maintainer:    konn.jinro_at_gmail.com
 author:        Hiromi ISHII
-tested-with:
-    ghc ==8.4.3 ghc ==8.6.5 ghc ==8.8.3 ghc ==8.10.3
-
+tested-with:   GHC ==8.6.5 || ==8.8.4 || ==8.10.7 || ==9.0.1 || ==9.2.1
 homepage:      https://github.com/konn/type-natural
 synopsis:      Type-level natural and proofs of their properties.
 description:
-    Type-level natural numbers and proofs of their properties.
-    .
-    Version 0.6+ supports __GHC 8+ only__.
-    .
-    __Use 0.5.* with ~ GHC 7.10.3__.
+  Type-level natural numbers and proofs of their properties.
+  .
+  Version 0.6+ supports __GHC 8+ only__.
+  .
+  __Use 0.5.* with ~ GHC 7.10.3__.
 
 category:      Math
 build-type:    Simple
 
 source-repository head
-    type:     git
-    location: git://github.com/konn/type-natural.git
+  type:     git
+  location: git://github.com/konn/type-natural.git
 
 library
-    exposed-modules:
-        Data.Type.Natural
-        Data.Type.Ordinal
-        Data.Type.Ordinal.Builtin
-        Data.Type.Natural.Builtin
-        Data.Type.Natural.Lemma.Arithmetic
-        Data.Type.Natural.Lemma.Order
-        Data.Type.Natural.Presburger.MinMaxSolver
+  exposed-modules:
+    Data.Type.Natural
+    Data.Type.Natural.Builtin
+    Data.Type.Natural.Lemma.Arithmetic
+    Data.Type.Natural.Lemma.Order
+    Data.Type.Natural.Presburger.MinMaxSolver
+    Data.Type.Ordinal
+    Data.Type.Ordinal.Builtin
 
-    hs-source-dirs:     src
-    other-modules:
-        Data.Type.Natural.Core
-        Data.Type.Natural.Utils
-        Data.Type.Natural.Lemma.Presburger
+  hs-source-dirs:     src
+  other-modules:
+    Data.Type.Natural.Core
+    Data.Type.Natural.Lemma.Presburger
+    Data.Type.Natural.Utils
 
-    default-language:   Haskell2010
-    default-extensions:
-        DataKinds PolyKinds ConstraintKinds GADTs ScopedTypeVariables
-        TemplateHaskell TypeFamilies TypeOperators MultiParamTypeClasses
-        UndecidableInstances FlexibleContexts FlexibleInstances
+  default-language:   Haskell2010
+  default-extensions:
+    ConstraintKinds
+    DataKinds
+    FlexibleContexts
+    FlexibleInstances
+    GADTs
+    MultiParamTypeClasses
+    PolyKinds
+    ScopedTypeVariables
+    TemplateHaskell
+    TypeFamilies
+    TypeOperators
+    UndecidableInstances
 
-    ghc-options:        -Wall -O2 -fno-warn-orphans
-    build-depends:
-        base ==4.*,
-        ghc,
-        equational-reasoning >=0.4.1.1,
-        template-haskell >=2.8,
-        constraints >=0.3,
-        ghc-typelits-natnormalise >=0.4,
-        ghc-typelits-presburger >=0.5.1,
-        ghc-typelits-knownnat -any,
-        integer-logarithms -any
+  ghc-options:        -Wall -O2 -fno-warn-orphans
+  build-depends:
+      base                       >=4       && <5
+    , constraints                >=0.3
+    , equational-reasoning       >=0.4.1.1
+    , ghc
+    , ghc-typelits-knownnat
+    , ghc-typelits-natnormalise  >=0.4
+    , ghc-typelits-presburger    >=0.5.1
+    , integer-logarithms
+    , template-haskell           >=2.8
 
-    if impl(ghc >=8.0.0)
-        ghc-options: -Wno-redundant-constraints
+  if impl(ghc >=8.0.0)
+    ghc-options: -Wno-redundant-constraints
 
-    if impl(ghc >=8.6)
-        default-extensions: NoStarIsType
+  if impl(ghc >=8.6)
+    default-extensions: NoStarIsType
 
 test-suite type-natural-test
-    type:           exitcode-stdio-1.0
-    main-is:        test.hs
-    build-tools:    tasty-discover -any
-    hs-source-dirs: tests
-    default-language:   Haskell2010
-    other-modules:
-        Shared
-        Data.Type.NaturalSpec
-        Data.Type.NaturalSpec.TH
-        Data.Type.Natural.Presburger.MinMaxSolverSpec
-        Data.Type.Natural.Presburger.Cases
-        Data.Type.OrdinalSpec
+  type:             exitcode-stdio-1.0
+  main-is:          test.hs
+  build-tools:      tasty-discover -any
+  hs-source-dirs:   tests
+  default-language: Haskell2010
+  ghc-options:      -Wall
+  other-modules:
+    Data.Type.Natural.Lemma.OrderSpec
+    Data.Type.Natural.Presburger.Cases
+    Data.Type.Natural.Presburger.MinMaxSolverSpec
+    Data.Type.NaturalSpec
+    Data.Type.NaturalSpec.TH
+    Data.Type.OrdinalSpec
+    Shared
 
-    build-depends:
-        tasty -any,
-        QuickCheck -any,
-        tasty-quickcheck -any,
-        quickcheck-instances -any,
-        integer-logarithms -any,
-        tasty-hunit -any,
-        tasty-discover -any,
-        template-haskell -any,
-        base -any,
-        type-natural -any,
-        equational-reasoning -any
+  build-depends:
+      base
+    , equational-reasoning
+    , integer-logarithms
+    , QuickCheck
+    , quickcheck-instances
+    , tasty
+    , tasty-discover
+    , tasty-hunit
+    , tasty-quickcheck
+    , template-haskell
+    , type-natural
 
-    if impl(ghc >=8.6)
-        default-extensions: NoStarIsType
+  if impl(ghc >=8.6)
+    default-extensions: NoStarIsType