    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE MagicHash #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE AllowAmbiguousTypes #-}
    {-# LANGUAGE Trustworthy #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# LANGUAGE NoStarIsType #-}
    -- | Utilities for working with 'KnownNat' constraints.
    --
    -- This module is only available on GHC 8.0 or later.
    module Data.Constraint.Nat
      ( Min, Max, Lcm, Gcd, Divides, Div, Mod, Log2
      , plusNat, minusNat, timesNat, powNat, minNat, maxNat, gcdNat, lcmNat, divNat, modNat, log2Nat
      , plusZero, minusZero, timesZero, timesOne, powZero, powOne, maxZero, minZero, gcdZero, gcdOne, lcmZero, lcmOne
      , plusAssociates, timesAssociates, minAssociates, maxAssociates, gcdAssociates, lcmAssociates
      , plusCommutes, timesCommutes, minCommutes, maxCommutes, gcdCommutes, lcmCommutes
      , plusDistributesOverTimes, timesDistributesOverPow, timesDistributesOverGcd, timesDistributesOverLcm
      , minDistributesOverPlus, minDistributesOverTimes, minDistributesOverPow1, minDistributesOverPow2, minDistributesOverMax
      , maxDistributesOverPlus, maxDistributesOverTimes, maxDistributesOverPow1, maxDistributesOverPow2, maxDistributesOverMin
      , gcdDistributesOverLcm, lcmDistributesOverGcd
      , minIsIdempotent, maxIsIdempotent, lcmIsIdempotent, gcdIsIdempotent
      , plusIsCancellative, timesIsCancellative
      , dividesPlus, dividesTimes, dividesMin, dividesMax, dividesPow, dividesGcd, dividesLcm
      , plusMonotone1, plusMonotone2
      , timesMonotone1, timesMonotone2
      , powMonotone1, powMonotone2
      , minMonotone1, minMonotone2
      , maxMonotone1, maxMonotone2
      , divMonotone1, divMonotone2
      , euclideanNat
      , plusMod, timesMod
      , modBound
      , log2Pow
      , dividesDef
      , timesDiv
      , eqLe, leEq, leId, leTrans
      , leZero, zeroLe
      , plusMinusInverse1, plusMinusInverse2, plusMinusInverse3
      ) where

    import Data.Constraint
    import Data.Constraint.Unsafe
    import Data.Proxy
    import Data.Type.Bool
    import GHC.TypeNats
    import qualified Numeric.Natural as Nat

    #if MIN_VERSION_base(4,15,0)
    import GHC.Num.Natural (naturalLog2)
    #else
    import GHC.Exts (Int(..))
    import GHC.Integer.Logarithms (integerLog2#)
    #endif

    #if !MIN_VERSION_base(4,18,0)
    import Unsafe.Coerce
    #endif

    type family Min (m::Nat) (n::Nat) :: Nat where
        Min m n = If (n <=? m) n m
    type family Max (m::Nat) (n::Nat) :: Nat where
        Max m n = If (n <=? m) m n
    type family Gcd (m::Nat) (n::Nat) :: Nat where
        Gcd m m = m
    type family Lcm (m::Nat) (n::Nat) :: Nat where
       Lcm m m = m

    type Divides n m = n ~ Gcd n m

    #if !MIN_VERSION_base(4,18,0)
    newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))
    #endif

    magicNNN :: forall n m o. (Nat.Natural -> Nat.Natural -> Nat.Natural) -> (KnownNat n, KnownNat m) :- KnownNat o
    #if MIN_VERSION_base(4,18,0)
    magicNNN :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    (Nat -> Nat -> Nat) -> (KnownNat n, KnownNat m) :- KnownNat o
    magicNNN Nat -> Nat -> Nat
    f = ((KnownNat n, KnownNat m) => Dict (KnownNat o))
    -> (KnownNat n, KnownNat m) :- KnownNat o
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub (((KnownNat n, KnownNat m) => Dict (KnownNat o))
     -> (KnownNat n, KnownNat m) :- KnownNat o)
    -> ((KnownNat n, KnownNat m) => Dict (KnownNat o))
    -> (KnownNat n, KnownNat m) :- KnownNat o
    forall a b. (a -> b) -> a -> b
    $ forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
    withKnownNat @o (Nat -> SNat o
    forall (n :: Nat). Nat -> SNat n
    unsafeSNat (Proxy n -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n) Nat -> Nat -> Nat
    `f` Proxy m -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @m))) Dict (KnownNat o)
    KnownNat o => Dict (KnownNat o)
    forall (a :: Constraint). a => Dict a
    Dict
    #else
    magicNNN f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy @n) `f` natVal (Proxy @m))
    #endif

    magicNN :: forall n m. (Nat.Natural -> Nat.Natural) -> KnownNat n :- KnownNat m
    #if MIN_VERSION_base(4,18,0)
    magicNN :: forall (n :: Nat) (m :: Nat).
    (Nat -> Nat) -> KnownNat n :- KnownNat m
    magicNN Nat -> Nat
    f = (KnownNat n => Dict (KnownNat m)) -> KnownNat n :- KnownNat m
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub ((KnownNat n => Dict (KnownNat m)) -> KnownNat n :- KnownNat m)
    -> (KnownNat n => Dict (KnownNat m)) -> KnownNat n :- KnownNat m
    forall a b. (a -> b) -> a -> b
    $ forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
    withKnownNat @m (Nat -> SNat m
    forall (n :: Nat). Nat -> SNat n
    unsafeSNat (Nat -> Nat
    f (Proxy n -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n)))) Dict (KnownNat m)
    KnownNat m => Dict (KnownNat m)
    forall (a :: Constraint). a => Dict a
    Dict
    #else
    magicNN f = Sub $ unsafeCoerce (Magic Dict) (f (natVal (Proxy :: Proxy n)))
    #endif

    axiomLe :: forall (a :: Nat) (b :: Nat). Dict (a <= b)
    axiomLe :: forall (a :: Nat) (b :: Nat). Dict (a <= b)
    axiomLe = Dict
      (Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...))
    Dict
      (Assert (OrdCond (Compare a b) 'True 'True 'False) (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    eqLe :: forall (a :: Nat) (b :: Nat). (a ~ b) :- (a <= b)
    eqLe :: forall (a :: Nat) (b :: Nat). (a ~ b) :- (a <= b)
    eqLe = ((a ~ b) =>
     Dict
       (Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...)))
    -> (a ~ b)
       :- Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict
      (Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...))
    (a ~ b) =>
    Dict
      (Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...))
    forall (a :: Constraint). a => Dict a
    Dict

    dividesGcd :: forall a b c. (Divides a b, Divides a c) :- Divides a (Gcd b c)
    dividesGcd :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (Divides a b, Divides a c) :- Divides a (Gcd b c)
    dividesGcd = ((a ~ Gcd a b, a ~ Gcd a c) => Dict (a ~ Gcd a (Gcd b c)))
    -> (a ~ Gcd a b, a ~ Gcd a c) :- (a ~ Gcd a (Gcd b c))
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (a ~ Gcd a (Gcd b c))
    (a ~ Gcd a b, a ~ Gcd a c) => Dict (a ~ Gcd a (Gcd b c))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    dividesLcm :: forall a b c. (Divides a c, Divides b c) :- Divides (Lcm a b) c
    dividesLcm :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (Divides a c, Divides b c) :- Divides (Lcm a b) c
    dividesLcm = ((a ~ Gcd a c, b ~ Gcd b c) => Dict (Lcm a b ~ Gcd (Lcm a b) c))
    -> (a ~ Gcd a c, b ~ Gcd b c) :- (Lcm a b ~ Gcd (Lcm a b) c)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (Lcm a b ~ Gcd (Lcm a b) c)
    (a ~ Gcd a c, b ~ Gcd b c) => Dict (Lcm a b ~ Gcd (Lcm a b) c)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    gcdCommutes :: forall a b. Dict (Gcd a b ~ Gcd b a)
    gcdCommutes :: forall (a :: Nat) (b :: Nat). Dict (Gcd a b ~ Gcd b a)
    gcdCommutes = Dict (Gcd a b ~ Gcd b a)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    lcmCommutes :: forall a b. Dict (Lcm a b ~ Lcm b a)
    lcmCommutes :: forall (a :: Nat) (b :: Nat). Dict (Lcm a b ~ Lcm b a)
    lcmCommutes = Dict (Lcm a b ~ Lcm b a)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    gcdZero :: forall a. Dict (Gcd 0 a ~ a)
    gcdZero :: forall (a :: Nat). Dict (Gcd 0 a ~ a)
    gcdZero = Dict (Gcd 0 a ~ a)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    gcdOne :: forall a. Dict (Gcd 1 a ~ 1)
    gcdOne :: forall (a :: Nat). Dict (Gcd 1 a ~ 1)
    gcdOne = Dict (Gcd 1 a ~ 1)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    lcmZero :: forall a. Dict (Lcm 0 a ~ 0)
    lcmZero :: forall (a :: Nat). Dict (Lcm 0 a ~ 0)
    lcmZero = Dict (Lcm 0 a ~ 0)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    lcmOne :: forall a. Dict (Lcm 1 a ~ a)
    lcmOne :: forall (a :: Nat). Dict (Lcm 1 a ~ a)
    lcmOne = Dict (Lcm 1 a ~ a)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    gcdNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Gcd n m)
    gcdNat :: forall (n :: Nat) (m :: Nat).
    (KnownNat n, KnownNat m) :- KnownNat (Gcd n m)
    gcdNat = (Nat -> Nat -> Nat)
    -> (KnownNat n, KnownNat m) :- KnownNat (Gcd n m)
    forall (n :: Nat) (m :: Nat) (o :: Nat).
    (Nat -> Nat -> Nat) -> (KnownNat n, KnownNat m) :- KnownNat o
    magicNNN Nat -> Nat -> Nat
    forall a. Integral a => a -> a -> a
    gcd

    lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
    lcmNat :: forall (n :: Nat) (m :: Nat).
    (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
    lcmNat = (Nat -> Nat -> Nat)
    -> (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
    forall (n :: Nat) (m :: Nat) (o :: Nat).
    (Nat -> Nat -> Nat) -> (KnownNat n, KnownNat m) :- KnownNat o
    magicNNN Nat -> Nat -> Nat
    forall a. Integral a => a -> a -> a
    lcm

    plusNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m)
    plusNat :: forall (n :: Nat) (m :: Nat).
    (KnownNat n, KnownNat m) :- KnownNat (n + m)
    plusNat = (Nat -> Nat -> Nat) -> (KnownNat n, KnownNat m) :- KnownNat (n + m)
    forall (n :: Nat) (m :: Nat) (o :: Nat).
    (Nat -> Nat -> Nat) -> (KnownNat n, KnownNat m) :- KnownNat o
    magicNNN Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    (+)

    minusNat :: forall n m. (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
    minusNat :: forall (n :: Nat) (m :: Nat).
    (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
    minusNat = ((KnownNat n, KnownNat m, m <= n) => Dict (KnownNat (n - m)))
    -> (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub (((KnownNat n, KnownNat m, m <= n) => Dict (KnownNat (n - m)))
     -> (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m))
    -> ((KnownNat n, KnownNat m, m <= n) => Dict (KnownNat (n - m)))
    -> (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
    forall a b. (a -> b) -> a -> b
    $ case forall (n :: Nat) (m :: Nat) (o :: Nat).
    (Nat -> Nat -> Nat) -> (KnownNat n, KnownNat m) :- KnownNat o
    magicNNN @n @m (-) of Sub (KnownNat n, KnownNat m) => Dict (KnownNat (n - m))
    r -> Dict (KnownNat (n - m))
    (KnownNat n, KnownNat m) => Dict (KnownNat (n - m))
    r

    minNat   :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Min n m)
    minNat :: forall (n :: Nat) (m :: Nat).
    (KnownNat n, KnownNat m) :- KnownNat (Min n m)
    minNat = (Nat -> Nat -> Nat)
    -> (KnownNat n, KnownNat m)
       :- KnownNat (If (OrdCond (CmpNat m n) 'True 'True 'False) m n)
    forall (n :: Nat) (m :: Nat) (o :: Nat).
    (Nat -> Nat -> Nat) -> (KnownNat n, KnownNat m) :- KnownNat o
    magicNNN Nat -> Nat -> Nat
    forall a. Ord a => a -> a -> a
    min

    maxNat   :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Max n m)
    maxNat :: forall (n :: Nat) (m :: Nat).
    (KnownNat n, KnownNat m) :- KnownNat (Max n m)
    maxNat = (Nat -> Nat -> Nat)
    -> (KnownNat n, KnownNat m)
       :- KnownNat (If (OrdCond (CmpNat m n) 'True 'True 'False) n m)
    forall (n :: Nat) (m :: Nat) (o :: Nat).
    (Nat -> Nat -> Nat) -> (KnownNat n, KnownNat m) :- KnownNat o
    magicNNN Nat -> Nat -> Nat
    forall a. Ord a => a -> a -> a
    max

    timesNat  :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n * m)
    timesNat :: forall (n :: Nat) (m :: Nat).
    (KnownNat n, KnownNat m) :- KnownNat (n * m)
    timesNat = (Nat -> Nat -> Nat) -> (KnownNat n, KnownNat m) :- KnownNat (n * m)
    forall (n :: Nat) (m :: Nat) (o :: Nat).
    (Nat -> Nat -> Nat) -> (KnownNat n, KnownNat m) :- KnownNat o
    magicNNN Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    (*)

    powNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n ^ m)
    powNat :: forall (n :: Nat) (m :: Nat).
    (KnownNat n, KnownNat m) :- KnownNat (n ^ m)
    powNat = (Nat -> Nat -> Nat) -> (KnownNat n, KnownNat m) :- KnownNat (n ^ m)
    forall (n :: Nat) (m :: Nat) (o :: Nat).
    (Nat -> Nat -> Nat) -> (KnownNat n, KnownNat m) :- KnownNat o
    magicNNN Nat -> Nat -> Nat
    forall a b. (Num a, Integral b) => a -> b -> a
    (^)

    divNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
    divNat :: forall (n :: Nat) (m :: Nat).
    (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
    divNat = ((KnownNat n, KnownNat m, 1 <= m) => Dict (KnownNat (Div n m)))
    -> (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub (((KnownNat n, KnownNat m, 1 <= m) => Dict (KnownNat (Div n m)))
     -> (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m))
    -> ((KnownNat n, KnownNat m, 1 <= m) => Dict (KnownNat (Div n m)))
    -> (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
    forall a b. (a -> b) -> a -> b
    $ case forall (n :: Nat) (m :: Nat) (o :: Nat).
    (Nat -> Nat -> Nat) -> (KnownNat n, KnownNat m) :- KnownNat o
    magicNNN @n @m Nat -> Nat -> Nat
    forall a. Integral a => a -> a -> a
    div of Sub (KnownNat n, KnownNat m) => Dict (KnownNat (Div n m))
    r -> Dict (KnownNat (Div n m))
    (KnownNat n, KnownNat m) => Dict (KnownNat (Div n m))
    r

    modNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)
    modNat :: forall (n :: Nat) (m :: Nat).
    (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)
    modNat = ((KnownNat n, KnownNat m, 1 <= m) => Dict (KnownNat (Mod n m)))
    -> (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub (((KnownNat n, KnownNat m, 1 <= m) => Dict (KnownNat (Mod n m)))
     -> (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m))
    -> ((KnownNat n, KnownNat m, 1 <= m) => Dict (KnownNat (Mod n m)))
    -> (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)
    forall a b. (a -> b) -> a -> b
    $ case forall (n :: Nat) (m :: Nat) (o :: Nat).
    (Nat -> Nat -> Nat) -> (KnownNat n, KnownNat m) :- KnownNat o
    magicNNN @n @m Nat -> Nat -> Nat
    forall a. Integral a => a -> a -> a
    mod of Sub (KnownNat n, KnownNat m) => Dict (KnownNat (Mod n m))
    r -> Dict (KnownNat (Mod n m))
    (KnownNat n, KnownNat m) => Dict (KnownNat (Mod n m))
    r

    log2Nat :: forall n. (KnownNat n, 1 <= n) :- KnownNat (Log2 n)
    log2Nat :: forall (n :: Nat). (KnownNat n, 1 <= n) :- KnownNat (Log2 n)
    log2Nat = ((KnownNat n, 1 <= n) => Dict (KnownNat (Log2 n)))
    -> (KnownNat n, 1 <= n) :- KnownNat (Log2 n)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub (((KnownNat n, 1 <= n) => Dict (KnownNat (Log2 n)))
     -> (KnownNat n, 1 <= n) :- KnownNat (Log2 n))
    -> ((KnownNat n, 1 <= n) => Dict (KnownNat (Log2 n)))
    -> (KnownNat n, 1 <= n) :- KnownNat (Log2 n)
    forall a b. (a -> b) -> a -> b
    $ case forall (n :: Nat) (m :: Nat).
    (Nat -> Nat) -> KnownNat n :- KnownNat m
    magicNN @n Nat -> Nat
    log2 of Sub KnownNat n => Dict (KnownNat (Log2 n))
    r -> Dict (KnownNat (Log2 n))
    KnownNat n => Dict (KnownNat (Log2 n))
    r
      where
        log2 :: Nat.Natural -> Nat.Natural
    #if MIN_VERSION_base(4,15,0)
        log2 :: Nat -> Nat
    log2 Nat
    n = Word -> Nat
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Nat -> Word
    naturalLog2 Nat
    n)
    #else
        log2 n = fromIntegral (I# (integerLog2# (toInteger n)))
    #endif

    plusZero :: forall n. Dict ((n + 0) ~ n)
    plusZero :: forall (n :: Nat). Dict ((n + 0) ~ n)
    plusZero = Dict (n ~ n)
    Dict ((n + 0) ~ n)
    forall (a :: Constraint). a => Dict a
    Dict

    minusZero :: forall n. Dict ((n - 0) ~ n)
    minusZero :: forall (n :: Nat). Dict ((n - 0) ~ n)
    minusZero = Dict (n ~ n)
    Dict ((n - 0) ~ n)
    forall (a :: Constraint). a => Dict a
    Dict

    timesZero :: forall n. Dict ((n * 0) ~ 0)
    timesZero :: forall (n :: Nat). Dict ((n * 0) ~ 0)
    timesZero = Dict (0 ~ 0)
    Dict ((n * 0) ~ 0)
    forall (a :: Constraint). a => Dict a
    Dict

    timesOne :: forall n. Dict ((n * 1) ~ n)
    timesOne :: forall (n :: Nat). Dict ((n * 1) ~ n)
    timesOne = Dict (n ~ n)
    Dict ((n * 1) ~ n)
    forall (a :: Constraint). a => Dict a
    Dict

    minZero :: forall n. Dict (Min n 0 ~ 0)
    #if MIN_VERSION_base(4,16,0)
    minZero :: forall (n :: Nat). Dict (Min n 0 ~ 0)
    minZero = Dict (If (OrdCond (CmpNat 0 n) 'True 'True 'False) 0 n ~ 0)
    Dict (Min n 0 ~ 0)
    forall (c :: Constraint). Dict c
    unsafeAxiom
    #else
    minZero = Dict
    #endif

    maxZero :: forall n. Dict (Max n 0 ~ n)
    #if MIN_VERSION_base(4,16,0)
    maxZero :: forall (n :: Nat). Dict (Max n 0 ~ n)
    maxZero = Dict (If (OrdCond (CmpNat 0 n) 'True 'True 'False) n 0 ~ n)
    Dict (Max n 0 ~ n)
    forall (c :: Constraint). Dict c
    unsafeAxiom
    #else
    maxZero = Dict
    #endif

    powZero :: forall n. Dict ((n ^ 0) ~ 1)
    powZero :: forall (n :: Nat). Dict ((n ^ 0) ~ 1)
    powZero = Dict (1 ~ 1)
    Dict ((n ^ 0) ~ 1)
    forall (a :: Constraint). a => Dict a
    Dict

    leZero :: forall a. (a <= 0) :- (a ~ 0)
    leZero :: forall (a :: Nat). (a <= 0) :- (a ~ 0)
    leZero = (Assert
       (OrdCond (CmpNat a 0) 'True 'True 'False) (TypeError ...) =>
     Dict (a ~ 0))
    -> Assert (OrdCond (CmpNat a 0) 'True 'True 'False) (TypeError ...)
       :- (a ~ 0)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (a ~ 0)
    Assert (OrdCond (CmpNat a 0) 'True 'True 'False) (TypeError ...) =>
    Dict (a ~ 0)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    zeroLe :: forall (a :: Nat). Dict (0 <= a)
    #if MIN_VERSION_base(4,16,0)
    zeroLe :: forall (a :: Nat). Dict (0 <= a)
    zeroLe = Dict
      (Assert (OrdCond (CmpNat 0 a) 'True 'True 'False) (TypeError ...))
    Dict
      (Assert (OrdCond (Compare 0 a) 'True 'True 'False) (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom
    #else
    zeroLe = Dict
    #endif

    plusMinusInverse1 :: forall n m. Dict (((m + n) - n) ~ m)
    plusMinusInverse1 :: forall (n :: Nat) (m :: Nat). Dict (((m + n) - n) ~ m)
    plusMinusInverse1 = Dict (((m + n) - n) ~ m)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    plusMinusInverse2 :: forall n m. (m <= n) :- (((m + n) - m) ~ n)
    plusMinusInverse2 :: forall (n :: Nat) (m :: Nat). (m <= n) :- (((m + n) - m) ~ n)
    plusMinusInverse2 = (Assert
       (OrdCond (CmpNat m n) 'True 'True 'False) (TypeError ...) =>
     Dict (((m + n) - m) ~ n))
    -> Assert (OrdCond (CmpNat m n) 'True 'True 'False) (TypeError ...)
       :- (((m + n) - m) ~ n)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (((m + n) - m) ~ n)
    Assert (OrdCond (CmpNat m n) 'True 'True 'False) (TypeError ...) =>
    Dict (((m + n) - m) ~ n)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    plusMinusInverse3 :: forall n m. (n <= m) :- (((m - n) + n) ~ m)
    plusMinusInverse3 :: forall (n :: Nat) (m :: Nat). (n <= m) :- (((m - n) + n) ~ m)
    plusMinusInverse3 = (Assert
       (OrdCond (CmpNat n m) 'True 'True 'False) (TypeError ...) =>
     Dict (((m - n) + n) ~ m))
    -> Assert (OrdCond (CmpNat n m) 'True 'True 'False) (TypeError ...)
       :- (((m - n) + n) ~ m)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (((m - n) + n) ~ m)
    Assert (OrdCond (CmpNat n m) 'True 'True 'False) (TypeError ...) =>
    Dict (((m - n) + n) ~ m)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    plusMonotone1 :: forall a b c. (a <= b) :- (a + c <= b + c)
    plusMonotone1 :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (a <= b) :- ((a + c) <= (b + c))
    plusMonotone1 = (Assert
       (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...) =>
     Dict
       (Assert
          (OrdCond (CmpNat (a + c) (b + c)) 'True 'True 'False)
          (TypeError ...)))
    -> Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...)
       :- Assert
            (OrdCond (CmpNat (a + c) (b + c)) 'True 'True 'False)
            (TypeError ...)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict
      (Assert
         (OrdCond (CmpNat (a + c) (b + c)) 'True 'True 'False)
         (TypeError ...))
    Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...) =>
    Dict
      (Assert
         (OrdCond (CmpNat (a + c) (b + c)) 'True 'True 'False)
         (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    plusMonotone2 :: forall a b c. (b <= c) :- (a + b <= a + c)
    plusMonotone2 :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (b <= c) :- ((a + b) <= (a + c))
    plusMonotone2 = (Assert
       (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...) =>
     Dict
       (Assert
          (OrdCond (CmpNat (a + b) (a + c)) 'True 'True 'False)
          (TypeError ...)))
    -> Assert (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...)
       :- Assert
            (OrdCond (CmpNat (a + b) (a + c)) 'True 'True 'False)
            (TypeError ...)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict
      (Assert
         (OrdCond (CmpNat (a + b) (a + c)) 'True 'True 'False)
         (TypeError ...))
    Assert (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...) =>
    Dict
      (Assert
         (OrdCond (CmpNat (a + b) (a + c)) 'True 'True 'False)
         (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    powMonotone1 :: forall a b c. (a <= b) :- ((a^c) <= (b^c))
    powMonotone1 :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (a <= b) :- ((a ^ c) <= (b ^ c))
    powMonotone1 = (Assert
       (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...) =>
     Dict
       (Assert
          (OrdCond (CmpNat (a ^ c) (b ^ c)) 'True 'True 'False)
          (TypeError ...)))
    -> Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...)
       :- Assert
            (OrdCond (CmpNat (a ^ c) (b ^ c)) 'True 'True 'False)
            (TypeError ...)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict
      (Assert
         (OrdCond (CmpNat (a ^ c) (b ^ c)) 'True 'True 'False)
         (TypeError ...))
    Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...) =>
    Dict
      (Assert
         (OrdCond (CmpNat (a ^ c) (b ^ c)) 'True 'True 'False)
         (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    powMonotone2 :: forall a b c. (b <= c) :- ((a^b) <= (a^c))
    powMonotone2 :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (b <= c) :- ((a ^ b) <= (a ^ c))
    powMonotone2 = (Assert
       (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...) =>
     Dict
       (Assert
          (OrdCond (CmpNat (a ^ b) (a ^ c)) 'True 'True 'False)
          (TypeError ...)))
    -> Assert (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...)
       :- Assert
            (OrdCond (CmpNat (a ^ b) (a ^ c)) 'True 'True 'False)
            (TypeError ...)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict
      (Assert
         (OrdCond (CmpNat (a ^ b) (a ^ c)) 'True 'True 'False)
         (TypeError ...))
    Assert (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...) =>
    Dict
      (Assert
         (OrdCond (CmpNat (a ^ b) (a ^ c)) 'True 'True 'False)
         (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    divMonotone1 :: forall a b c. (a <= b) :- (Div a c <= Div b c)
    divMonotone1 :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (a <= b) :- (Div a c <= Div b c)
    divMonotone1 = (Assert
       (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...) =>
     Dict
       (Assert
          (OrdCond (CmpNat (Div a c) (Div b c)) 'True 'True 'False)
          (TypeError ...)))
    -> Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...)
       :- Assert
            (OrdCond (CmpNat (Div a c) (Div b c)) 'True 'True 'False)
            (TypeError ...)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict
      (Assert
         (OrdCond (CmpNat (Div a c) (Div b c)) 'True 'True 'False)
         (TypeError ...))
    Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...) =>
    Dict
      (Assert
         (OrdCond (CmpNat (Div a c) (Div b c)) 'True 'True 'False)
         (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    divMonotone2 :: forall a b c. (b <= c) :- (Div a c <= Div a b)
    divMonotone2 :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (b <= c) :- (Div a c <= Div a b)
    divMonotone2 = (Assert
       (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...) =>
     Dict
       (Assert
          (OrdCond (CmpNat (Div a c) (Div a b)) 'True 'True 'False)
          (TypeError ...)))
    -> Assert (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...)
       :- Assert
            (OrdCond (CmpNat (Div a c) (Div a b)) 'True 'True 'False)
            (TypeError ...)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict
      (Assert
         (OrdCond (CmpNat (Div a c) (Div a b)) 'True 'True 'False)
         (TypeError ...))
    Assert (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...) =>
    Dict
      (Assert
         (OrdCond (CmpNat (Div a c) (Div a b)) 'True 'True 'False)
         (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    timesMonotone1 :: forall a b c. (a <= b) :- (a * c <= b * c)
    timesMonotone1 :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (a <= b) :- ((a * c) <= (b * c))
    timesMonotone1 = (Assert
       (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...) =>
     Dict
       (Assert
          (OrdCond (CmpNat (a * c) (b * c)) 'True 'True 'False)
          (TypeError ...)))
    -> Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...)
       :- Assert
            (OrdCond (CmpNat (a * c) (b * c)) 'True 'True 'False)
            (TypeError ...)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict
      (Assert
         (OrdCond (CmpNat (a * c) (b * c)) 'True 'True 'False)
         (TypeError ...))
    Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...) =>
    Dict
      (Assert
         (OrdCond (CmpNat (a * c) (b * c)) 'True 'True 'False)
         (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    timesMonotone2 :: forall a b c. (b <= c) :- (a * b <= a * c)
    timesMonotone2 :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (b <= c) :- ((a * b) <= (a * c))
    timesMonotone2 = (Assert
       (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...) =>
     Dict
       (Assert
          (OrdCond (CmpNat (a * b) (a * c)) 'True 'True 'False)
          (TypeError ...)))
    -> Assert (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...)
       :- Assert
            (OrdCond (CmpNat (a * b) (a * c)) 'True 'True 'False)
            (TypeError ...)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict
      (Assert
         (OrdCond (CmpNat (a * b) (a * c)) 'True 'True 'False)
         (TypeError ...))
    Assert (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...) =>
    Dict
      (Assert
         (OrdCond (CmpNat (a * b) (a * c)) 'True 'True 'False)
         (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    minMonotone1 :: forall a b c. (a <= b) :- (Min a c <= Min b c)
    minMonotone1 :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (a <= b) :- (Min a c <= Min b c)
    minMonotone1 = (Assert
       (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...) =>
     Dict
       (Assert
          (OrdCond
             (CmpNat
                (If (OrdCond (CmpNat c a) 'True 'True 'False) c a)
                (If (OrdCond (CmpNat c b) 'True 'True 'False) c b))
             'True
             'True
             'False)
          (TypeError ...)))
    -> Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...)
       :- Assert
            (OrdCond
               (CmpNat
                  (If (OrdCond (CmpNat c a) 'True 'True 'False) c a)
                  (If (OrdCond (CmpNat c b) 'True 'True 'False) c b))
               'True
               'True
               'False)
            (TypeError ...)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict
      (Assert
         (OrdCond
            (CmpNat
               (If (OrdCond (CmpNat c a) 'True 'True 'False) c a)
               (If (OrdCond (CmpNat c b) 'True 'True 'False) c b))
            'True
            'True
            'False)
         (TypeError ...))
    Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...) =>
    Dict
      (Assert
         (OrdCond
            (CmpNat
               (If (OrdCond (CmpNat c a) 'True 'True 'False) c a)
               (If (OrdCond (CmpNat c b) 'True 'True 'False) c b))
            'True
            'True
            'False)
         (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    minMonotone2 :: forall a b c. (b <= c) :- (Min a b <= Min a c)
    minMonotone2 :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (b <= c) :- (Min a b <= Min a c)
    minMonotone2 = (Assert
       (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...) =>
     Dict
       (Assert
          (OrdCond
             (CmpNat
                (If (OrdCond (CmpNat b a) 'True 'True 'False) b a)
                (If (OrdCond (CmpNat c a) 'True 'True 'False) c a))
             'True
             'True
             'False)
          (TypeError ...)))
    -> Assert (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...)
       :- Assert
            (OrdCond
               (CmpNat
                  (If (OrdCond (CmpNat b a) 'True 'True 'False) b a)
                  (If (OrdCond (CmpNat c a) 'True 'True 'False) c a))
               'True
               'True
               'False)
            (TypeError ...)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict
      (Assert
         (OrdCond
            (CmpNat
               (If (OrdCond (CmpNat b a) 'True 'True 'False) b a)
               (If (OrdCond (CmpNat c a) 'True 'True 'False) c a))
            'True
            'True
            'False)
         (TypeError ...))
    Assert (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...) =>
    Dict
      (Assert
         (OrdCond
            (CmpNat
               (If (OrdCond (CmpNat b a) 'True 'True 'False) b a)
               (If (OrdCond (CmpNat c a) 'True 'True 'False) c a))
            'True
            'True
            'False)
         (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    maxMonotone1 :: forall a b c. (a <= b) :- (Max a c <= Max b c)
    maxMonotone1 :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (a <= b) :- (Max a c <= Max b c)
    maxMonotone1 = (Assert
       (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...) =>
     Dict
       (Assert
          (OrdCond
             (CmpNat
                (If (OrdCond (CmpNat c a) 'True 'True 'False) a c)
                (If (OrdCond (CmpNat c b) 'True 'True 'False) b c))
             'True
             'True
             'False)
          (TypeError ...)))
    -> Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...)
       :- Assert
            (OrdCond
               (CmpNat
                  (If (OrdCond (CmpNat c a) 'True 'True 'False) a c)
                  (If (OrdCond (CmpNat c b) 'True 'True 'False) b c))
               'True
               'True
               'False)
            (TypeError ...)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict
      (Assert
         (OrdCond
            (CmpNat
               (If (OrdCond (CmpNat c a) 'True 'True 'False) a c)
               (If (OrdCond (CmpNat c b) 'True 'True 'False) b c))
            'True
            'True
            'False)
         (TypeError ...))
    Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...) =>
    Dict
      (Assert
         (OrdCond
            (CmpNat
               (If (OrdCond (CmpNat c a) 'True 'True 'False) a c)
               (If (OrdCond (CmpNat c b) 'True 'True 'False) b c))
            'True
            'True
            'False)
         (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    maxMonotone2 :: forall a b c. (b <= c) :- (Max a b <= Max a c)
    maxMonotone2 :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (b <= c) :- (Max a b <= Max a c)
    maxMonotone2 = (Assert
       (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...) =>
     Dict
       (Assert
          (OrdCond
             (CmpNat
                (If (OrdCond (CmpNat b a) 'True 'True 'False) a b)
                (If (OrdCond (CmpNat c a) 'True 'True 'False) a c))
             'True
             'True
             'False)
          (TypeError ...)))
    -> Assert (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...)
       :- Assert
            (OrdCond
               (CmpNat
                  (If (OrdCond (CmpNat b a) 'True 'True 'False) a b)
                  (If (OrdCond (CmpNat c a) 'True 'True 'False) a c))
               'True
               'True
               'False)
            (TypeError ...)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict
      (Assert
         (OrdCond
            (CmpNat
               (If (OrdCond (CmpNat b a) 'True 'True 'False) a b)
               (If (OrdCond (CmpNat c a) 'True 'True 'False) a c))
            'True
            'True
            'False)
         (TypeError ...))
    Assert (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...) =>
    Dict
      (Assert
         (OrdCond
            (CmpNat
               (If (OrdCond (CmpNat b a) 'True 'True 'False) a b)
               (If (OrdCond (CmpNat c a) 'True 'True 'False) a c))
            'True
            'True
            'False)
         (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    powOne :: forall n. Dict ((n ^ 1) ~ n)
    powOne :: forall (n :: Nat). Dict ((n ^ 1) ~ n)
    powOne = Dict (n ~ n)
    Dict ((n ^ 1) ~ n)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    plusMod :: forall a b c. (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)
    plusMod :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)
    plusMod = (Assert
       (OrdCond (CmpNat 1 c) 'True 'True 'False) (TypeError ...) =>
     Dict (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c))
    -> Assert (OrdCond (CmpNat 1 c) 'True 'True 'False) (TypeError ...)
       :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)
    Assert (OrdCond (CmpNat 1 c) 'True 'True 'False) (TypeError ...) =>
    Dict (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    timesMod :: forall a b c. (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)
    timesMod :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)
    timesMod = (Assert
       (OrdCond (CmpNat 1 c) 'True 'True 'False) (TypeError ...) =>
     Dict (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c))
    -> Assert (OrdCond (CmpNat 1 c) 'True 'True 'False) (TypeError ...)
       :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)
    Assert (OrdCond (CmpNat 1 c) 'True 'True 'False) (TypeError ...) =>
    Dict (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    modBound :: forall m n. (1 <= n) :- (Mod m n <= n)
    modBound :: forall (m :: Nat) (n :: Nat). (1 <= n) :- (Mod m n <= n)
    modBound = (Assert
       (OrdCond (CmpNat 1 n) 'True 'True 'False) (TypeError ...) =>
     Dict
       (Assert
          (OrdCond (CmpNat (Mod m n) n) 'True 'True 'False) (TypeError ...)))
    -> Assert (OrdCond (CmpNat 1 n) 'True 'True 'False) (TypeError ...)
       :- Assert
            (OrdCond (CmpNat (Mod m n) n) 'True 'True 'False) (TypeError ...)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict
      (Assert
         (OrdCond (CmpNat (Mod m n) n) 'True 'True 'False) (TypeError ...))
    Assert (OrdCond (CmpNat 1 n) 'True 'True 'False) (TypeError ...) =>
    Dict
      (Assert
         (OrdCond (CmpNat (Mod m n) n) 'True 'True 'False) (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    log2Pow :: forall n. Dict (Log2 (2 ^ n) ~ n)
    log2Pow :: forall (n :: Nat). Dict (Log2 (2 ^ n) ~ n)
    log2Pow = Dict (Log2 (2 ^ n) ~ n)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    euclideanNat :: (1 <= c) :- (a ~ (c * Div a c + Mod a c))
    euclideanNat :: forall (c :: Nat) (a :: Nat).
    (1 <= c) :- (a ~ ((c * Div a c) + Mod a c))
    euclideanNat = (Assert
       (OrdCond (CmpNat 1 c) 'True 'True 'False) (TypeError ...) =>
     Dict (a ~ ((c * Div a c) + Mod a c)))
    -> Assert (OrdCond (CmpNat 1 c) 'True 'True 'False) (TypeError ...)
       :- (a ~ ((c * Div a c) + Mod a c))
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (a ~ ((c * Div a c) + Mod a c))
    Assert (OrdCond (CmpNat 1 c) 'True 'True 'False) (TypeError ...) =>
    Dict (a ~ ((c * Div a c) + Mod a c))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    plusCommutes :: forall n m. Dict ((m + n) ~ (n + m))
    plusCommutes :: forall (n :: Nat) (m :: Nat). Dict ((m + n) ~ (n + m))
    plusCommutes = Dict ((m + n) ~ (n + m))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    timesCommutes :: forall n m. Dict ((m * n) ~ (n * m))
    timesCommutes :: forall (n :: Nat) (m :: Nat). Dict ((m * n) ~ (n * m))
    timesCommutes = Dict ((m * n) ~ (n * m))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    minCommutes :: forall n m. Dict (Min m n ~ Min n m)
    minCommutes :: forall (n :: Nat) (m :: Nat). Dict (Min m n ~ Min n m)
    minCommutes = Dict
      (If (OrdCond (CmpNat n m) 'True 'True 'False) n m
       ~ If (OrdCond (CmpNat m n) 'True 'True 'False) m n)
    Dict (Min m n ~ Min n m)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    maxCommutes :: forall n m. Dict (Max m n ~ Max n m)
    maxCommutes :: forall (n :: Nat) (m :: Nat). Dict (Max m n ~ Max n m)
    maxCommutes = Dict
      (If (OrdCond (CmpNat n m) 'True 'True 'False) m n
       ~ If (OrdCond (CmpNat m n) 'True 'True 'False) n m)
    Dict (Max m n ~ Max n m)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    plusAssociates :: forall m n o. Dict (((m + n) + o) ~ (m + (n + o)))
    plusAssociates :: forall (m :: Nat) (n :: Nat) (o :: Nat).
    Dict (((m + n) + o) ~ (m + (n + o)))
    plusAssociates = Dict (((m + n) + o) ~ (m + (n + o)))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    timesAssociates :: forall m n o. Dict (((m * n) * o) ~ (m * (n * o)))
    timesAssociates :: forall (m :: Nat) (n :: Nat) (o :: Nat).
    Dict (((m * n) * o) ~ (m * (n * o)))
    timesAssociates = Dict (((m * n) * o) ~ (m * (n * o)))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    minAssociates :: forall m n o. Dict (Min (Min m n) o ~ Min m (Min n o))
    minAssociates :: forall (m :: Nat) (n :: Nat) (o :: Nat).
    Dict (Min (Min m n) o ~ Min m (Min n o))
    minAssociates = Dict
      (If
         (OrdCond
            (CmpNat o (If (OrdCond (CmpNat n m) 'True 'True 'False) n m))
            'True
            'True
            'False)
         o
         (If (OrdCond (CmpNat n m) 'True 'True 'False) n m)
       ~ If
           (OrdCond
              (CmpNat (If (OrdCond (CmpNat o n) 'True 'True 'False) o n) m)
              'True
              'True
              'False)
           (If (OrdCond (CmpNat o n) 'True 'True 'False) o n)
           m)
    Dict (Min (Min m n) o ~ Min m (Min n o))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    maxAssociates :: forall m n o. Dict (Max (Max m n) o ~ Max m (Max n o))
    maxAssociates :: forall (m :: Nat) (n :: Nat) (o :: Nat).
    Dict (Max (Max m n) o ~ Max m (Max n o))
    maxAssociates = Dict
      (If
         (OrdCond
            (CmpNat o (If (OrdCond (CmpNat n m) 'True 'True 'False) m n))
            'True
            'True
            'False)
         (If (OrdCond (CmpNat n m) 'True 'True 'False) m n)
         o
       ~ If
           (OrdCond
              (CmpNat (If (OrdCond (CmpNat o n) 'True 'True 'False) n o) m)
              'True
              'True
              'False)
           m
           (If (OrdCond (CmpNat o n) 'True 'True 'False) n o))
    Dict (Max (Max m n) o ~ Max m (Max n o))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    gcdAssociates :: forall a b c. Dict (Gcd (Gcd a b) c  ~ Gcd a (Gcd b c))
    gcdAssociates :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    Dict (Gcd (Gcd a b) c ~ Gcd a (Gcd b c))
    gcdAssociates = Dict (Gcd (Gcd a b) c ~ Gcd a (Gcd b c))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    lcmAssociates :: forall a b c. Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c))
    lcmAssociates :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c))
    lcmAssociates = Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    minIsIdempotent :: forall n. Dict (Min n n ~ n)
    minIsIdempotent :: forall (n :: Nat). Dict (Min n n ~ n)
    minIsIdempotent = Dict (n ~ n)
    Dict (Min n n ~ n)
    forall (a :: Constraint). a => Dict a
    Dict

    maxIsIdempotent :: forall n. Dict (Max n n ~ n)
    maxIsIdempotent :: forall (n :: Nat). Dict (Max n n ~ n)
    maxIsIdempotent = Dict (n ~ n)
    Dict (Max n n ~ n)
    forall (a :: Constraint). a => Dict a
    Dict

    gcdIsIdempotent :: forall n. Dict (Gcd n n ~ n)
    gcdIsIdempotent :: forall (n :: Nat). Dict (Gcd n n ~ n)
    gcdIsIdempotent = Dict (n ~ n)
    Dict (Gcd n n ~ n)
    forall (a :: Constraint). a => Dict a
    Dict

    lcmIsIdempotent :: forall n. Dict (Lcm n n ~ n)
    lcmIsIdempotent :: forall (n :: Nat). Dict (Lcm n n ~ n)
    lcmIsIdempotent = Dict (n ~ n)
    Dict (Lcm n n ~ n)
    forall (a :: Constraint). a => Dict a
    Dict

    minDistributesOverPlus :: forall n m o. Dict ((n + Min m o) ~ Min (n + m) (n + o))
    minDistributesOverPlus :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    Dict ((n + Min m o) ~ Min (n + m) (n + o))
    minDistributesOverPlus = Dict
      ((n + If (OrdCond (CmpNat o m) 'True 'True 'False) o m)
       ~ If
           (OrdCond (CmpNat (n + o) (n + m)) 'True 'True 'False)
           (n + o)
           (n + m))
    Dict ((n + Min m o) ~ Min (n + m) (n + o))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    minDistributesOverTimes :: forall n m o. Dict ((n * Min m o) ~ Min (n * m) (n * o))
    minDistributesOverTimes :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    Dict ((n * Min m o) ~ Min (n * m) (n * o))
    minDistributesOverTimes = Dict
      ((n * If (OrdCond (CmpNat o m) 'True 'True 'False) o m)
       ~ If
           (OrdCond (CmpNat (n * o) (n * m)) 'True 'True 'False)
           (n * o)
           (n * m))
    Dict ((n * Min m o) ~ Min (n * m) (n * o))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    minDistributesOverPow1 :: forall n m o. Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o))
    minDistributesOverPow1 :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o))
    minDistributesOverPow1 = Dict
      ((If (OrdCond (CmpNat m n) 'True 'True 'False) m n ^ o)
       ~ If
           (OrdCond (CmpNat (m ^ o) (n ^ o)) 'True 'True 'False)
           (m ^ o)
           (n ^ o))
    Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    minDistributesOverPow2 :: forall n m o. Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o))
    minDistributesOverPow2 :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o))
    minDistributesOverPow2 = Dict
      ((n ^ If (OrdCond (CmpNat o m) 'True 'True 'False) o m)
       ~ If
           (OrdCond (CmpNat (n ^ o) (n ^ m)) 'True 'True 'False)
           (n ^ o)
           (n ^ m))
    Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    minDistributesOverMax :: forall n m o. Dict (Max n (Min m o) ~ Min (Max n m) (Max n o))
    minDistributesOverMax :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    Dict (Max n (Min m o) ~ Min (Max n m) (Max n o))
    minDistributesOverMax = Dict
      (If
         (OrdCond
            (CmpNat (If (OrdCond (CmpNat o m) 'True 'True 'False) o m) n)
            'True
            'True
            'False)
         n
         (If (OrdCond (CmpNat o m) 'True 'True 'False) o m)
       ~ If
           (OrdCond
              (CmpNat
                 (If (OrdCond (CmpNat o n) 'True 'True 'False) n o)
                 (If (OrdCond (CmpNat m n) 'True 'True 'False) n m))
              'True
              'True
              'False)
           (If (OrdCond (CmpNat o n) 'True 'True 'False) n o)
           (If (OrdCond (CmpNat m n) 'True 'True 'False) n m))
    Dict (Max n (Min m o) ~ Min (Max n m) (Max n o))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    maxDistributesOverPlus :: forall n m o. Dict ((n + Max m o) ~ Max (n + m) (n + o))
    maxDistributesOverPlus :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    Dict ((n + Max m o) ~ Max (n + m) (n + o))
    maxDistributesOverPlus = Dict
      ((n + If (OrdCond (CmpNat o m) 'True 'True 'False) m o)
       ~ If
           (OrdCond (CmpNat (n + o) (n + m)) 'True 'True 'False)
           (n + m)
           (n + o))
    Dict ((n + Max m o) ~ Max (n + m) (n + o))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    maxDistributesOverTimes :: forall n m o. Dict ((n * Max m o) ~ Max (n * m) (n * o))
    maxDistributesOverTimes :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    Dict ((n * Max m o) ~ Max (n * m) (n * o))
    maxDistributesOverTimes = Dict
      ((n * If (OrdCond (CmpNat o m) 'True 'True 'False) m o)
       ~ If
           (OrdCond (CmpNat (n * o) (n * m)) 'True 'True 'False)
           (n * m)
           (n * o))
    Dict ((n * Max m o) ~ Max (n * m) (n * o))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    maxDistributesOverPow1 :: forall n m o. Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o))
    maxDistributesOverPow1 :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o))
    maxDistributesOverPow1 = Dict
      ((If (OrdCond (CmpNat m n) 'True 'True 'False) n m ^ o)
       ~ If
           (OrdCond (CmpNat (m ^ o) (n ^ o)) 'True 'True 'False)
           (n ^ o)
           (m ^ o))
    Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    maxDistributesOverPow2 :: forall n m o. Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o))
    maxDistributesOverPow2 :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o))
    maxDistributesOverPow2 = Dict
      ((n ^ If (OrdCond (CmpNat o m) 'True 'True 'False) m o)
       ~ If
           (OrdCond (CmpNat (n ^ o) (n ^ m)) 'True 'True 'False)
           (n ^ m)
           (n ^ o))
    Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    maxDistributesOverMin :: forall n m o. Dict (Min n (Max m o) ~ Max (Min n m) (Min n o))
    maxDistributesOverMin :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    Dict (Min n (Max m o) ~ Max (Min n m) (Min n o))
    maxDistributesOverMin = Dict
      (If
         (OrdCond
            (CmpNat (If (OrdCond (CmpNat o m) 'True 'True 'False) m o) n)
            'True
            'True
            'False)
         (If (OrdCond (CmpNat o m) 'True 'True 'False) m o)
         n
       ~ If
           (OrdCond
              (CmpNat
                 (If (OrdCond (CmpNat o n) 'True 'True 'False) o n)
                 (If (OrdCond (CmpNat m n) 'True 'True 'False) m n))
              'True
              'True
              'False)
           (If (OrdCond (CmpNat m n) 'True 'True 'False) m n)
           (If (OrdCond (CmpNat o n) 'True 'True 'False) o n))
    Dict (Min n (Max m o) ~ Max (Min n m) (Min n o))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    plusDistributesOverTimes :: forall n m o. Dict ((n * (m + o)) ~ (n * m + n * o))
    plusDistributesOverTimes :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    Dict ((n * (m + o)) ~ ((n * m) + (n * o)))
    plusDistributesOverTimes = Dict ((n * (m + o)) ~ ((n * m) + (n * o)))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    timesDistributesOverPow  :: forall n m o. Dict ((n ^ (m + o)) ~ (n ^ m * n ^ o))
    timesDistributesOverPow :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    Dict ((n ^ (m + o)) ~ ((n ^ m) * (n ^ o)))
    timesDistributesOverPow = Dict ((n ^ (m + o)) ~ ((n ^ m) * (n ^ o)))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    timesDistributesOverGcd :: forall n m o. Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o))
    timesDistributesOverGcd :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o))
    timesDistributesOverGcd = Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    timesDistributesOverLcm :: forall n m o. Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o))
    timesDistributesOverLcm :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o))
    timesDistributesOverLcm = Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    plusIsCancellative :: forall n m o. ((n + m) ~ (n + o)) :- (m ~ o)
    plusIsCancellative :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    ((n + m) ~ (n + o)) :- (m ~ o)
    plusIsCancellative = (((n + m) ~ (n + o)) => Dict (m ~ o))
    -> ((n + m) ~ (n + o)) :- (m ~ o)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (m ~ o)
    ((n + m) ~ (n + o)) => Dict (m ~ o)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    timesIsCancellative :: forall n m o. (1 <= n, (n * m) ~ (n * o)) :- (m ~ o)
    timesIsCancellative :: forall (n :: Nat) (m :: Nat) (o :: Nat).
    (1 <= n, (n * m) ~ (n * o)) :- (m ~ o)
    timesIsCancellative = ((Assert (OrdCond (CmpNat 1 n) 'True 'True 'False) (TypeError ...),
      (n * m) ~ (n * o)) =>
     Dict (m ~ o))
    -> (Assert
          (OrdCond (CmpNat 1 n) 'True 'True 'False) (TypeError ...),
        (n * m) ~ (n * o))
       :- (m ~ o)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (m ~ o)
    (Assert (OrdCond (CmpNat 1 n) 'True 'True 'False) (TypeError ...),
     (n * m) ~ (n * o)) =>
    Dict (m ~ o)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    gcdDistributesOverLcm :: forall a b c. Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c))
    gcdDistributesOverLcm :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c))
    gcdDistributesOverLcm = Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    lcmDistributesOverGcd :: forall a b c. Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c))
    lcmDistributesOverGcd :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c))
    lcmDistributesOverGcd = Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    dividesPlus :: (Divides a b, Divides a c) :- Divides a (b + c)
    dividesPlus :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (Divides a b, Divides a c) :- Divides a (b + c)
    dividesPlus = ((a ~ Gcd a b, a ~ Gcd a c) => Dict (a ~ Gcd a (b + c)))
    -> (a ~ Gcd a b, a ~ Gcd a c) :- (a ~ Gcd a (b + c))
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (a ~ Gcd a (b + c))
    (a ~ Gcd a b, a ~ Gcd a c) => Dict (a ~ Gcd a (b + c))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    dividesTimes :: Divides a b :- Divides a (b * c)
    dividesTimes :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    Divides a b :- Divides a (b * c)
    dividesTimes = ((a ~ Gcd a b) => Dict (a ~ Gcd a (b * c)))
    -> (a ~ Gcd a b) :- (a ~ Gcd a (b * c))
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (a ~ Gcd a (b * c))
    (a ~ Gcd a b) => Dict (a ~ Gcd a (b * c))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    dividesMin :: (Divides a b, Divides a c) :- Divides a (Min b c)
    dividesMin :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (Divides a b, Divides a c) :- Divides a (Min b c)
    dividesMin = ((a ~ Gcd a b, a ~ Gcd a c) =>
     Dict
       (a ~ Gcd a (If (OrdCond (CmpNat c b) 'True 'True 'False) c b)))
    -> (a ~ Gcd a b, a ~ Gcd a c)
       :- (a ~ Gcd a (If (OrdCond (CmpNat c b) 'True 'True 'False) c b))
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (a ~ Gcd a (If (OrdCond (CmpNat c b) 'True 'True 'False) c b))
    (a ~ Gcd a b, a ~ Gcd a c) =>
    Dict (a ~ Gcd a (If (OrdCond (CmpNat c b) 'True 'True 'False) c b))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    dividesMax :: (Divides a b, Divides a c) :- Divides a (Max b c)
    dividesMax :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (Divides a b, Divides a c) :- Divides a (Max b c)
    dividesMax = ((a ~ Gcd a b, a ~ Gcd a c) =>
     Dict
       (a ~ Gcd a (If (OrdCond (CmpNat c b) 'True 'True 'False) b c)))
    -> (a ~ Gcd a b, a ~ Gcd a c)
       :- (a ~ Gcd a (If (OrdCond (CmpNat c b) 'True 'True 'False) b c))
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (a ~ Gcd a (If (OrdCond (CmpNat c b) 'True 'True 'False) b c))
    (a ~ Gcd a b, a ~ Gcd a c) =>
    Dict (a ~ Gcd a (If (OrdCond (CmpNat c b) 'True 'True 'False) b c))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    -- This `dividesDef` is simpler and more convenient than Divides a b :- ((a * Div b a) ~ b)
    -- because the latter can be easily derived via 'euclideanNat', but not vice versa.

    dividesDef :: forall a b. Divides a b :- (Mod b a ~ 0)
    dividesDef :: forall (a :: Nat) (b :: Nat). Divides a b :- (Mod b a ~ 0)
    dividesDef = ((a ~ Gcd a b) => Dict (Mod b a ~ 0))
    -> (a ~ Gcd a b) :- (Mod b a ~ 0)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (Mod b a ~ 0)
    (a ~ Gcd a b) => Dict (Mod b a ~ 0)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    dividesPow :: (1 <= n, Divides a b) :- Divides a (b^n)
    dividesPow :: forall (n :: Nat) (a :: Nat) (b :: Nat).
    (1 <= n, Divides a b) :- Divides a (b ^ n)
    dividesPow = ((Assert (OrdCond (CmpNat 1 n) 'True 'True 'False) (TypeError ...),
      a ~ Gcd a b) =>
     Dict (a ~ Gcd a (b ^ n)))
    -> (Assert
          (OrdCond (CmpNat 1 n) 'True 'True 'False) (TypeError ...),
        a ~ Gcd a b)
       :- (a ~ Gcd a (b ^ n))
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (a ~ Gcd a (b ^ n))
    (Assert (OrdCond (CmpNat 1 n) 'True 'True 'False) (TypeError ...),
     a ~ Gcd a b) =>
    Dict (a ~ Gcd a (b ^ n))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    timesDiv :: forall a b. Dict ((a * Div b a) <= b)
    timesDiv :: forall (a :: Nat) (b :: Nat). Dict ((a * Div b a) <= b)
    timesDiv = Dict
      (Assert
         (OrdCond (CmpNat (a * Div b a) b) 'True 'True 'False)
         (TypeError ...))
    Dict
      (Assert
         (OrdCond (Compare (a * Div b a) b) 'True 'True 'False)
         (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    -- (<=) is an internal category in the category of constraints.

    leId :: forall (a :: Nat). Dict (a <= a)
    leId :: forall (a :: Nat). Dict (a <= a)
    leId = Dict (() :: Constraint)
    Dict
      (Assert (OrdCond (Compare a a) 'True 'True 'False) (TypeError ...))
    forall (a :: Constraint). a => Dict a
    Dict

    leEq :: forall (a :: Nat) (b :: Nat). (a <= b, b <= a) :- (a ~ b)
    leEq :: forall (a :: Nat) (b :: Nat). (a <= b, b <= a) :- (a ~ b)
    leEq = ((Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...),
      Assert
        (OrdCond (CmpNat b a) 'True 'True 'False) (TypeError ...)) =>
     Dict (a ~ b))
    -> (Assert
          (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...),
        Assert (OrdCond (CmpNat b a) 'True 'True 'False) (TypeError ...))
       :- (a ~ b)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (a ~ b)
    (Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...),
     Assert
       (OrdCond (CmpNat b a) 'True 'True 'False) (TypeError ...)) =>
    Dict (a ~ b)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    leTrans :: forall (a :: Nat) (b :: Nat) (c :: Nat). (b <= c, a <= b) :- (a <= c)
    leTrans :: forall (a :: Nat) (b :: Nat) (c :: Nat).
    (b <= c, a <= b) :- (a <= c)
    leTrans = ((Assert (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...),
      Assert
        (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...)) =>
     Dict
       (Assert (OrdCond (CmpNat a c) 'True 'True 'False) (TypeError ...)))
    -> (Assert
          (OrdCond (CmpNat b c) 'True 'True 'False) (TypeError ...),
        Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...))
       :- Assert (OrdCond (CmpNat a c) 'True 'True 'False) (TypeError ...)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub (forall (a :: Nat) (b :: Nat). Dict (a <= b)
    axiomLe @a @c)