Data.Type.Natural.Builtin

Coercion between Peano Numerals Nat and builtin naturals Nat

Sysnonym to avoid confusion

type Peano = Nat

Type synonym for Nat to avoid confusion with built-in Nat.

Coercion between builtin type-level natural and peano numerals

type family FromPeano (n :: Nat) :: Nat where ...

Equations

FromPeano Z = 0

FromPeano (S n) = Succ (FromPeano n)

type family ToPeano (n :: Nat) :: Nat where ...

Equations

ToPeano 0 = Z

ToPeano n = S (ToPeano (Pred n))

sFromPeano :: Sing n -> Sing (FromPeano n)

sToPeano :: Sing n -> Sing (ToPeano n)

Properties of FromPeano and ToPeano.

fromPeanoInjective :: forall n m. (SingI n, SingI m) => (FromPeano n :~: FromPeano m) -> n :~: m

toPeanoInjective :: forall n m. (KnownNat n, KnownNat m) => (ToPeano n :~: ToPeano m) -> n :~: m

Bijection

fromToPeano :: Sing n -> FromPeano (ToPeano n) :~: n

toFromPeano :: Sing n -> ToPeano (FromPeano n) :~: n

Algebraic isomorphisms

fromPeanoZeroCong :: FromPeano Z :~: 0

toPeanoZeroCong :: ToPeano 0 :~: Z

fromPeanoOneCong :: FromPeano One :~: 1

toPeanoOneCong :: ToPeano 1 :~: One

fromPeanoSuccCong :: Sing n -> FromPeano (S n) :~: Succ (FromPeano n)

toPeanoSuccCong :: Sing n -> ToPeano (Succ n) :~: S (ToPeano n)

fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n + m) :~: (FromPeano n + FromPeano m)

toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n + m) :~: (ToPeano n + ToPeano m)

fromPeanoMultCong :: Sing n -> Sing m -> FromPeano (n * m) :~: (FromPeano n * FromPeano m)

toPeanoMultCong :: Sing n -> Sing m -> ToPeano (n * m) :~: (ToPeano n * ToPeano m)

fromPeanoMonotone :: (n <= m) ~ True => Sing n -> Sing m -> (FromPeano n <=? FromPeano m) :~: True

toPeanoMonotone :: n <= m => Sing n -> Sing m -> (ToPeano n <= ToPeano m) :~: True

Peano and commutative ring axioms for built-in Nat

class (SDecide nat, SNum nat, SEnum nat, SingKind nat, SingKind nat) => IsPeano nat where

Minimal complete definition

succOneCong, succNonCyclic, predSucc, plusMinus, succInj, (plusZeroL, plusSuccL | plusZeroR, plusZeroL), (multZeroL, multSuccL | multZeroR, multSuccR), induction

Methods

succOneCong :: Succ (Zero nat) :~: One nat

succInj :: (Succ n :~: Succ (m :: nat)) -> n :~: m

succInj' :: proxy n -> proxy' m -> (Succ n :~: Succ (m :: nat)) -> n :~: m

succNonCyclic :: Sing n -> (Succ n :~: Zero nat) -> Void

induction :: p (Zero nat) -> (forall n. Sing n -> p n -> p (S n)) -> Sing k -> p k

plusMinus :: Sing (n :: nat) -> Sing m -> ((n + m) - m) :~: n

plusMinus' :: Sing (n :: nat) -> Sing m -> ((n + m) - n) :~: m

plusZeroL :: Sing n -> (Zero nat + n) :~: n

plusSuccL :: Sing n -> Sing m -> (S n + m) :~: S (n + m :: nat)

plusZeroR :: Sing n -> (n + Zero nat) :~: n

plusSuccR :: Sing n -> Sing m -> (n + S m) :~: S (n + m :: nat)

plusComm :: Sing n -> Sing m -> (n + m) :~: ((m :: nat) + n)

plusAssoc :: forall n m l. Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) + l) :~: (n + (m + l))

multZeroL :: Sing n -> (Zero nat * n) :~: Zero nat

multSuccL :: Sing (n :: nat) -> Sing m -> (S n * m) :~: ((n * m) + m)

multZeroR :: Sing n -> (n * Zero nat) :~: Zero nat

multSuccR :: Sing n -> Sing m -> (n * S m) :~: ((n * m) + (n :: nat))

multComm :: Sing (n :: nat) -> Sing m -> (n * m) :~: (m * n)

multOneR :: Sing n -> (n * One nat) :~: n

multOneL :: Sing n -> (One nat * n) :~: n

plusMultDistrib :: Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) * l) :~: ((n * l) + (m * l))

multPlusDistrib :: Sing (n :: nat) -> Sing m -> Sing l -> (n * (m + l)) :~: ((n * m) + (n * l))

minusNilpotent :: Sing n -> (n - n) :~: Zero nat

multAssoc :: Sing (n :: nat) -> Sing m -> Sing l -> ((n * m) * l) :~: (n * (m * l))

plusEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) :~: (n + l)) -> m :~: l

plusEqCancelR :: forall n m l. Sing (n :: nat) -> Sing m -> Sing l -> ((n + l) :~: (m + l)) -> n :~: m

succAndPlusOneL :: Sing n -> Succ n :~: (One nat + n)

succAndPlusOneR :: Sing n -> Succ n :~: (n + One nat)

predSucc :: Sing n -> Pred (Succ n) :~: (n :: nat)

zeroOrSucc :: Sing (n :: nat) -> ZeroOrSucc n

plusEqZeroL :: Sing n -> Sing m -> ((n + m) :~: Zero nat) -> n :~: Zero nat

plusEqZeroR :: Sing n -> Sing m -> ((n + m) :~: Zero nat) -> m :~: Zero nat

predUnique :: Sing (n :: nat) -> Sing m -> (Succ n :~: m) -> n :~: Pred m

multEqSuccElimL :: Sing (n :: nat) -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> n :~: Succ (Pred n)

multEqSuccElimR :: Sing (n :: nat) -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> m :~: Succ (Pred m)

minusZero :: Sing n -> (n - Zero nat) :~: n

multEqCancelR :: Sing (n :: nat) -> Sing m -> Sing l -> ((n * Succ l) :~: (m * Succ l)) -> n :~: m

succPred :: Sing n -> ((n :~: Zero nat) -> Void) -> Succ (Pred n) :~: n

multEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> ((Succ n * m) :~: (Succ n * l)) -> m :~: l

sPred' :: proxy n -> Sing (Succ n) -> Sing (n :: nat)

toNatural :: Sing (n :: nat) -> Natural

fromNatural :: Natural -> SomeSing nat

inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m + 1)) -> Sing n -> p n

Induction scheme for built-in Nat.

QuasiQuotes

snat :: QuasiQuoter

Quotesi-quoter for singleton types for Nat. This can be used for an expression.

For example: [snat|12|] %+ [snat| 5 |].

Re-exports

module Data.Singletons.Prelude.Eq

module Data.Singletons.Prelude.Num

module Data.Singletons.Prelude.Ord

type (<) a b = (:<) a b infix 4

type (<@#@$) = (:<$)

type (<@#@$$) = (:<$$)

type (<@#@$$$) a b = (:<$$$) a b

(%<) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((<) a b) infix 4

type (>) a b = (:>) a b infix 4

type (>@#@$) = (:>$)

type (>@#@$$) = (:>$$)

type (>@#@$$$) a b = (:>$$$) a b

(%>) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((>) a b) infix 4

type (<=) a b = (:<=) a b infix 4

type (<=@#@$) = (:<=$)

type (<=@#@$$) = (:<=$$)

type (<=@#@$$$) a b = (:<=$$$) a b

(%<=) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((<=) a b) infix 4

type (>=) a b = (:>=) a b infix 4

type (>=@#@$) = (:>=$)

type (>=@#@$$) = (:>=$$)

type (>=@#@$$$) a b = (:>=$$$) a b

(%>=) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((>=) a b) infix 4

type (/=) a b = (:/=) a b infix 4

type (/=@#@$) = (:/=$)

type (/=@#@$$) = (:/=$$)

type (/=@#@$$$) a b = (:/=$$$) a b

(%/=) :: forall nat (a :: nat) (b :: nat). SEq nat => Sing a -> Sing b -> Sing ((/=) a b) infix 4

type (==) a b = (:==) a b infix 4

type (==@#@$) = (:==$)

type (==@#@$$) = (:==$$)

type (==@#@$$$) a b = (:==$$$) a b

(%==) :: forall nat (a :: nat) (b :: nat). SEq nat => Sing a -> Sing b -> Sing ((==) a b) infix 4

type (+) a b = (:+) a b infixl 6

type (+@#@$) = (:+$)

type (+@#@$$) = (:+$$)

type (+@#@$$$) a b = (:+$$$) a b

(%+) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing ((+) a b) infixl 6

type (-) a b = (:-) a b infixl 6

type (-@#@$) = (:-$)

type (-@#@$$) = (:-$$)

type (-@#@$$$) a b = (:-$$$) a b

(%-) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing ((-) a b) infixl 6

type * a b = (:*) a b infixl 7

type (*@#@$) = (:*$)

type (*@#@$$) = (:*$$)

type (*@#@$$$) a b = (:*$$$) a b

(%*) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing (* a b) infixl 7

Orphan instances

IsPeano Nat

Methods

succOneCong :: (Nat :~: Succ Nat (Zero Nat)) (One Nat)

succInj :: (Nat :~: Succ Nat n) (Succ Nat m) -> (Nat :~: n) m

succInj' :: proxy n -> proxy' m -> (Nat :~: Succ Nat n) (Succ Nat m) -> (Nat :~: n) m

succNonCyclic :: Sing Nat n -> (Nat :~: Succ Nat n) (Zero Nat) -> Void

induction :: p (Zero Nat) -> (forall (n :: Nat). Sing Nat n -> p n -> p (S Nat n)) -> Sing Nat k -> p k

plusMinus :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat - (Nat + n) m) m) n

plusMinus' :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat - (Nat + n) m) n) m

plusZeroL :: Sing Nat n -> (Nat :~: (Nat + Zero Nat) n) n

plusSuccL :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat + S Nat n) m) (S Nat ((Nat + n) m))

plusZeroR :: Sing Nat n -> (Nat :~: (Nat + n) (Zero Nat)) n

plusSuccR :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat + n) (S Nat m)) (S Nat ((Nat + n) m))

plusComm :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat + n) m) ((Nat + m) n)

plusAssoc :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat + (Nat + n) m) l) ((Nat + n) ((Nat + m) l))

multZeroL :: Sing Nat n -> (Nat :~: (Nat * Zero Nat) n) (Zero Nat)

multSuccL :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat * S Nat n) m) ((Nat + (Nat * n) m) m)

multZeroR :: Sing Nat n -> (Nat :~: (Nat * n) (Zero Nat)) (Zero Nat)

multSuccR :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat * n) (S Nat m)) ((Nat + (Nat * n) m) n)

multComm :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat * n) m) ((Nat * m) n)

multOneR :: Sing Nat n -> (Nat :~: (Nat * n) (One Nat)) n

multOneL :: Sing Nat n -> (Nat :~: (Nat * One Nat) n) n

plusMultDistrib :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat * (Nat + n) m) l) ((Nat + (Nat * n) l) ((Nat * m) l))

multPlusDistrib :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat * n) ((Nat + m) l)) ((Nat + (Nat * n) m) ((Nat * n) l))

minusNilpotent :: Sing Nat n -> (Nat :~: (Nat - n) n) (Zero Nat)

multAssoc :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat * (Nat * n) m) l) ((Nat * n) ((Nat * m) l))

plusEqCancelL :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat + n) m) ((Nat + n) l) -> (Nat :~: m) l

plusEqCancelR :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat + n) l) ((Nat + m) l) -> (Nat :~: n) m

succAndPlusOneL :: Sing Nat n -> (Nat :~: Succ Nat n) ((Nat + One Nat) n)

succAndPlusOneR :: Sing Nat n -> (Nat :~: Succ Nat n) ((Nat + n) (One Nat))

predSucc :: Sing Nat n -> (Nat :~: Pred Nat (Succ Nat n)) n

zeroOrSucc :: Sing Nat n -> ZeroOrSucc Nat n

plusEqZeroL :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat + n) m) (Zero Nat) -> (Nat :~: n) (Zero Nat)

plusEqZeroR :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat + n) m) (Zero Nat) -> (Nat :~: m) (Zero Nat)

predUnique :: Sing Nat n -> Sing Nat m -> (Nat :~: Succ Nat n) m -> (Nat :~: n) (Pred Nat m)

multEqSuccElimL :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat * n) m) (Succ Nat l) -> (Nat :~: n) (Succ Nat (Pred Nat n))

multEqSuccElimR :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat * n) m) (Succ Nat l) -> (Nat :~: m) (Succ Nat (Pred Nat m))

minusZero :: Sing Nat n -> (Nat :~: (Nat - n) (Zero Nat)) n

multEqCancelR :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat * n) (Succ Nat l)) ((Nat * m) (Succ Nat l)) -> (Nat :~: n) m

succPred :: Sing Nat n -> ((Nat :~: n) (Zero Nat) -> Void) -> (Nat :~: Succ Nat (Pred Nat n)) n

multEqCancelL :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat * Succ Nat n) m) ((Nat * Succ Nat n) l) -> (Nat :~: m) l

sPred' :: proxy n -> Sing Nat (Succ Nat n) -> Sing Nat n

toNatural :: Sing Nat n -> Natural

fromNatural :: Natural -> SomeSing Nat

PeanoOrder Nat

Methods

leqToCmp :: Sing Nat a -> Sing Nat b -> IsTrue ((Nat <= a) b) -> Either ((Nat :~: a) b) ((Ordering :~: Compare Nat a b) LT)

eqlCmpEQ :: Sing Nat a -> Sing Nat b -> (Nat :~: a) b -> (Ordering :~: Compare Nat a b) EQ

eqToRefl :: Sing Nat a -> Sing Nat b -> (Ordering :~: Compare Nat a b) EQ -> (Nat :~: a) b

flipCompare :: Sing Nat a -> Sing Nat b -> (Ordering :~: FlipOrdering (Compare Nat a b)) (Compare Nat b a)

ltToNeq :: Sing Nat a -> Sing Nat b -> (Ordering :~: Compare Nat a b) LT -> (Nat :~: a) b -> Void

leqNeqToLT :: Sing Nat a -> Sing Nat b -> IsTrue ((Nat <= a) b) -> ((Nat :~: a) b -> Void) -> (Ordering :~: Compare Nat a b) LT

succLeqToLT :: Sing Nat a -> Sing Nat b -> IsTrue ((Nat <= S Nat a) b) -> (Ordering :~: Compare Nat a b) LT

ltToLeq :: Sing Nat a -> Sing Nat b -> (Ordering :~: Compare Nat a b) LT -> IsTrue ((Nat <= a) b)

gtToLeq :: Sing Nat a -> Sing Nat b -> (Ordering :~: Compare Nat a b) GT -> IsTrue ((Nat <= b) a)

ltToSuccLeq :: Sing Nat a -> Sing Nat b -> (Ordering :~: Compare Nat a b) LT -> IsTrue ((Nat <= Succ Nat a) b)

cmpZero :: Sing Nat a -> (Ordering :~: Compare Nat (Zero Nat) (Succ Nat a)) LT

leqToGT :: Sing Nat a -> Sing Nat b -> IsTrue ((Nat <= Succ Nat b) a) -> (Ordering :~: Compare Nat a b) GT

cmpZero' :: Sing Nat a -> Either ((Ordering :~: Compare Nat (Zero Nat) a) EQ) ((Ordering :~: Compare Nat (Zero Nat) a) LT)

zeroNoLT :: Sing Nat a -> (Ordering :~: Compare Nat a (Zero Nat)) LT -> Void

ltRightPredSucc :: Sing Nat a -> Sing Nat b -> (Ordering :~: Compare Nat a b) LT -> (Nat :~: b) (Succ Nat (Pred Nat b))

cmpSucc :: Sing Nat n -> Sing Nat m -> (Ordering :~: Compare Nat n m) (Compare Nat (Succ Nat n) (Succ Nat m))

ltSucc :: Sing Nat a -> (Ordering :~: Compare Nat a (Succ Nat a)) LT

cmpSuccStepR :: Sing Nat n -> Sing Nat m -> (Ordering :~: Compare Nat n m) LT -> (Ordering :~: Compare Nat n (Succ Nat m)) LT

ltSuccLToLT :: Sing Nat n -> Sing Nat m -> (Ordering :~: Compare Nat (Succ Nat n) m) LT -> (Ordering :~: Compare Nat n m) LT

leqToLT :: Sing Nat a -> Sing Nat b -> IsTrue ((Nat <= Succ Nat a) b) -> (Ordering :~: Compare Nat a b) LT

leqZero :: Sing Nat n -> IsTrue ((Nat <= Zero Nat) n)

leqSucc :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= n) m) -> IsTrue ((Nat <= Succ Nat n) (Succ Nat m))

fromLeqView :: LeqView Nat n m -> IsTrue ((Nat <= n) m)

leqViewRefl :: Sing Nat n -> LeqView Nat n n

viewLeq :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= n) m) -> LeqView Nat n m

leqWitness :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= n) m) -> DiffNat Nat n m

leqStep :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat + n) l) m -> IsTrue ((Nat <= n) m)

leqNeqToSuccLeq :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= n) m) -> ((Nat :~: n) m -> Void) -> IsTrue ((Nat <= Succ Nat n) m)

leqRefl :: Sing Nat n -> IsTrue ((Nat <= n) n)

leqSuccStepR :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= n) m) -> IsTrue ((Nat <= n) (Succ Nat m))

leqSuccStepL :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= Succ Nat n) m) -> IsTrue ((Nat <= n) m)

leqReflexive :: Sing Nat n -> Sing Nat m -> (Nat :~: n) m -> IsTrue ((Nat <= n) m)

leqTrans :: Sing Nat n -> Sing Nat m -> Sing Nat l -> IsTrue ((Nat <= n) m) -> IsTrue ((Nat <= m) l) -> IsTrue ((Nat <= n) l)

leqAntisymm :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= n) m) -> IsTrue ((Nat <= m) n) -> (Nat :~: n) m

plusMonotone :: Sing Nat n -> Sing Nat m -> Sing Nat l -> Sing Nat k -> IsTrue ((Nat <= n) m) -> IsTrue ((Nat <= l) k) -> IsTrue ((Nat <= (Nat + n) l) ((Nat + m) k))

leqZeroElim :: Sing Nat n -> IsTrue ((Nat <= n) (Zero Nat)) -> (Nat :~: n) (Zero Nat)

plusMonotoneL :: Sing Nat n -> Sing Nat m -> Sing Nat l -> IsTrue ((Nat <= n) m) -> IsTrue ((Nat <= (Nat + n) l) ((Nat + m) l))

plusMonotoneR :: Sing Nat n -> Sing Nat m -> Sing Nat l -> IsTrue ((Nat <= m) l) -> IsTrue ((Nat <= (Nat + n) m) ((Nat + n) l))

plusLeqL :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= n) ((Nat + n) m))

plusLeqR :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= m) ((Nat + n) m))

plusCancelLeqR :: Sing Nat n -> Sing Nat m -> Sing Nat l -> IsTrue ((Nat <= (Nat + n) l) ((Nat + m) l)) -> IsTrue ((Nat <= n) m)

plusCancelLeqL :: Sing Nat n -> Sing Nat m -> Sing Nat l -> IsTrue ((Nat <= (Nat + n) m) ((Nat + n) l)) -> IsTrue ((Nat <= m) l)

succLeqZeroAbsurd :: Sing Nat n -> IsTrue ((Nat <= S Nat n) (Zero Nat)) -> Void

succLeqZeroAbsurd' :: Sing Nat n -> (Bool :~: (Nat <= S Nat n) (Zero Nat)) False

succLeqAbsurd :: Sing Nat n -> IsTrue ((Nat <= S Nat n) n) -> Void

succLeqAbsurd' :: Sing Nat n -> (Bool :~: (Nat <= S Nat n) n) False

notLeqToLeq :: (Bool ~ (Nat <= n) m) False => Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= m) n)

leqSucc' :: Sing Nat n -> Sing Nat m -> (Bool :~: (Nat <= n) m) ((Nat <= Succ Nat n) (Succ Nat m))

leqToMin :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= n) m) -> (Nat :~: Min Nat n m) n

geqToMin :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= m) n) -> (Nat :~: Min Nat n m) m

minComm :: Sing Nat n -> Sing Nat m -> (Nat :~: Min Nat n m) (Min Nat m n)

minLeqL :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= Min Nat n m) n)

minLeqR :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= Min Nat n m) m)

minLargest :: Sing Nat l -> Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= l) n) -> IsTrue ((Nat <= l) m) -> IsTrue ((Nat <= l) (Min Nat n m))

leqToMax :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= n) m) -> (Nat :~: Max Nat n m) m

geqToMax :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= m) n) -> (Nat :~: Max Nat n m) n

maxComm :: Sing Nat n -> Sing Nat m -> (Nat :~: Max Nat n m) (Max Nat m n)

maxLeqR :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= m) (Max Nat n m))

maxLeqL :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= n) (Max Nat n m))

maxLeast :: Sing Nat l -> Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= n) l) -> IsTrue ((Nat <= m) l) -> IsTrue ((Nat <= Max Nat n m) l)

leqReversed :: Sing Nat n -> Sing Nat m -> (Bool :~: (Nat <= n) m) ((Nat >= m) n)

lneqSuccLeq :: Sing Nat n -> Sing Nat m -> (Bool :~: (Nat < n) m) ((Nat <= Succ Nat n) m)

lneqReversed :: Sing Nat n -> Sing Nat m -> (Bool :~: (Nat < n) m) ((Nat > m) n)

lneqToLT :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat < n) m) -> (Ordering :~: Compare Nat n m) LT

ltToLneq :: Sing Nat n -> Sing Nat m -> (Ordering :~: Compare Nat n m) LT -> IsTrue ((Nat < n) m)

lneqZero :: Sing Nat a -> IsTrue ((Nat < Zero Nat) (Succ Nat a))

lneqSucc :: Sing Nat n -> IsTrue ((Nat < n) (Succ Nat n))

succLneqSucc :: Sing Nat n -> Sing Nat m -> (Bool :~: (Nat < n) m) ((Nat < Succ Nat n) (Succ Nat m))

lneqRightPredSucc :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat < n) m) -> (Nat :~: m) (Succ Nat (Pred Nat m))

lneqSuccStepL :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat < Succ Nat n) m) -> IsTrue ((Nat < n) m)

lneqSuccStepR :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat < n) m) -> IsTrue ((Nat < n) (Succ Nat m))

plusStrictMonotone :: Sing Nat n -> Sing Nat m -> Sing Nat l -> Sing Nat k -> IsTrue ((Nat < n) m) -> IsTrue ((Nat < l) k) -> IsTrue ((Nat < (Nat + n) l) ((Nat + m) k))

maxZeroL :: Sing Nat n -> (Nat :~: Max Nat (Zero Nat) n) n

maxZeroR :: Sing Nat n -> (Nat :~: Max Nat n (Zero Nat)) n

minZeroL :: Sing Nat n -> (Nat :~: Min Nat (Zero Nat) n) (Zero Nat)

minZeroR :: Sing Nat n -> (Nat :~: Min Nat n (Zero Nat)) (Zero Nat)

minusSucc :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= m) n) -> (Nat :~: (Nat - Succ Nat n) m) (Succ Nat ((Nat - n) m))

lneqZeroAbsurd :: Sing Nat n -> IsTrue ((Nat < n) (Zero Nat)) -> Void

minusPlus :: PeanoOrder Nat => Sing Nat n -> Sing Nat m -> IsTrue ((Nat <= m) n) -> (Nat :~: (Nat + (Nat - n) m) m) n