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)

leqqAndLeq :: Sing n -> Sing m -> (n <=? m) :~: (n <= m)

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

Instances

IsPeano Nat

Defined in Data.Type.Natural.Builtin

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

multSuccL :: Sing n -> 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)

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

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

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

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

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

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

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

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

plusEqCancelR :: Sing n -> 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

zeroOrSucc :: Sing n -> 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 -> Sing m -> (Succ n :~: m) -> n :~: Pred m

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

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

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

multEqCancelR :: Sing n -> 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 -> Sing m -> Sing l -> ((Succ n * m) :~: (Succ n * l)) -> m :~: l

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

toNatural :: Sing n -> Natural

fromNatural :: Natural -> SomeSing Nat

IsPeano Nat

Since 0.5.0.0

Defined in Data.Type.Natural

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

multSuccL :: Sing n -> 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)

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

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

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

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

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

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

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

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

plusEqCancelR :: Sing n -> 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

zeroOrSucc :: Sing n -> 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 -> Sing m -> (Succ n :~: m) -> n :~: Pred m

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

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

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

multEqCancelR :: Sing n -> 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 -> Sing m -> Sing l -> ((Succ n * m) :~: (Succ n * l)) -> m :~: l

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

toNatural :: Sing n -> 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

Orphan instances

IsPeano Nat

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

multSuccL :: Sing n -> 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)

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

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

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

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

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

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

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

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

plusEqCancelR :: Sing n -> 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

zeroOrSucc :: Sing n -> 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 -> Sing m -> (Succ n :~: m) -> n :~: Pred m

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

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

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

multEqCancelR :: Sing n -> 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 -> Sing m -> Sing l -> ((Succ n * m) :~: (Succ n * l)) -> m :~: l

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

toNatural :: Sing n -> Natural

fromNatural :: Natural -> SomeSing Nat

PeanoOrder Nat

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

leqViewRefl :: Sing n -> LeqView n n

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

minComm :: Sing n -> Sing m -> Min n m :~: Min m n

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

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

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

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

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

maxComm :: Sing n -> Sing m -> Max n m :~: Max m n

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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