{-# 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)