{-# LANGUAGE DataKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}

module Data.Type.Natural.Lemma.Order
  ( DiffNat (..),
    LeqView (..),
    type (<),
    type (<?),
    (%<?),
    type (>),
    type (>?),
    (%>?),
    type (>=),
    type (>=?),
    (%>=?),
    FlipOrdering,
    Min,
    sMin,
    Max,
    sMax,
    OrdCond,
    sOrdCond,

    -- * Lemmas
    ordCondDistrib,
    leqOrdCond,
    sFlipOrdering,
    coerceLeqL,
    coerceLeqR,
    sLeqCongL,
    sLeqCongR,
    sLeqCong,
    succDiffNat,
    compareCongR,
    leqToCmp,
    eqlCmpEQ,
    eqToRefl,
    flipCmpNat,
    ltToNeq,
    leqNeqToLT,
    succLeqToLT,
    ltToLeq,
    gtToLeq,
    congFlipOrdering,
    ltToSuccLeq,
    cmpZero,
    cmpSuccZeroGT,
    leqToGT,
    cmpZero',
    zeroNoLT,
    ltRightPredSucc,
    cmpSucc,
    ltSucc,
    cmpSuccStepR,
    ltSuccLToLT,
    leqToLT,
    leqZero,
    leqSucc,
    fromLeqView,
    leqViewRefl,
    viewLeq,
    leqWitness,
    leqStep,
    leqNeqToSuccLeq,
    leqRefl,
    leqSuccStepR,
    leqSuccStepL,
    leqReflexive,
    leqTrans,
    leqAntisymm,
    plusMonotone,
    leqZeroElim,
    plusMonotoneL,
    plusMonotoneR,
    plusLeqL,
    plusLeqR,
    plusCancelLeqR,
    plusCancelLeqL,
    succLeqZeroAbsurd,
    succLeqZeroAbsurd',
    succLeqAbsurd,
    succLeqAbsurd',
    notLeqToLeq,
    leqSucc',
    leqToMin,
    geqToMin,
    minComm,
    minLeqL,
    minLeqR,
    minLargest,
    leqToMax,
    geqToMax,
    maxComm,
    maxLeqR,
    maxLeqL,
    maxLeast,
    lneqSuccLeq,
    lneqReversed,
    lneqToLT,
    ltToLneq,
    lneqZero,
    lneqSucc,
    succLneqSucc,
    lneqRightPredSucc,
    lneqSuccStepL,
    lneqSuccStepR,
    plusStrictMonotone,
    minCase,
    maxCase,
    maxZeroL,
    maxZeroR,
    minZeroL,
    minZeroR,
    minusSucc,
    lneqZeroAbsurd,
    minusPlus,
    minPlusTruncMinus,
    truncMinusLeq,
    type (-.),
    (%-.),

    -- * Various witnesses for orderings
    LeqWitness,
    (:<:),
    Leq (..),
    leqRhs,
    leqLhs,

    -- ** conversions between lax orders
    propToBoolLeq,
    boolToPropLeq,

    -- ** conversions between strict orders
    propToBoolLt,
    boolToPropLt,
  )
where

import Data.Type.Equality (gcastWith, (:~:) (..))
import Data.Type.Natural.Core
import Data.Type.Natural.Lemma.Arithmetic
import Data.Void (Void, absurd)
import Proof.Equational
  ( because,
    start,
    sym,
    trans,
    (===),
    (=~=),
  )
import Proof.Propositional (IsTrue (..), eliminate, withWitness)
#if MIN_VERSION_ghc(9,2,1)
import qualified Data.Type.Ord as DTO
import Data.Type.Ord (OrdCond)
#endif


--------------------------------------------------

-- ** Type-level predicate & judgements.

--------------------------------------------------

#if !MIN_VERSION_ghc(9,2,1)
type family OrdCond (o :: Ordering) (lt :: k) (eq :: k) (gt :: k) where
  OrdCond 'LT lt eq gt = lt
  OrdCond 'EQ lt eq gt = eq
  OrdCond 'GT lt eq gt = gt
#endif

sOrdCond :: SOrdering o -> f lt -> f eq -> f gt -> f (OrdCond o lt eq gt)
sOrdCond :: forall {k} (o :: Ordering) (f :: k -> Type) (lt :: k) (eq :: k)
       (gt :: k).
SOrdering o -> f lt -> f eq -> f gt -> f (OrdCond o lt eq gt)
sOrdCond SOrdering o
SLT f lt
lt f eq
_ f gt
_ = f lt
f (OrdCond o lt eq gt)
lt
sOrdCond SOrdering o
SEQ f lt
_ f eq
eq f gt
_ = f eq
f (OrdCond o lt eq gt)
eq
sOrdCond SOrdering o
SGT f lt
_ f eq
_ f gt
gt = f gt
f (OrdCond o lt eq gt)
gt

minCase :: SNat n -> SNat m -> Either (Min n m :~: n) (Min n m :~: m)
minCase :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> Either (Min n m :~: n) (Min n m :~: m)
minCase SNat n
n SNat m
m =
  case SNat n -> SNat m -> SOrdering (CmpNat n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n SNat m
m of
    SOrdering (CmpNat n m)
SLT -> (n :~: n) -> Either (n :~: n) (n :~: m)
forall a b. a -> Either a b
Left n :~: n
forall {k} (a :: k). a :~: a
Refl
    SOrdering (CmpNat n m)
SEQ -> (n :~: n) -> Either (n :~: n) (n :~: m)
forall a b. a -> Either a b
Left n :~: n
forall {k} (a :: k). a :~: a
Refl
    SOrdering (CmpNat n m)
SGT -> (m :~: m) -> Either (m :~: n) (m :~: m)
forall a b. b -> Either a b
Right m :~: m
forall {k} (a :: k). a :~: a
Refl

maxCase :: SNat n -> SNat m -> Either (Max n m :~: m) (Max n m :~: n)
maxCase :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> Either (Max n m :~: m) (Max n m :~: n)
maxCase SNat n
n SNat m
m =
  case SNat n -> SNat m -> SOrdering (CmpNat n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n SNat m
m of
    SOrdering (CmpNat n m)
SLT -> (m :~: m) -> Either (m :~: m) (m :~: n)
forall a b. a -> Either a b
Left m :~: m
forall {k} (a :: k). a :~: a
Refl
    SOrdering (CmpNat n m)
SEQ -> (m :~: m) -> Either (m :~: m) (m :~: n)
forall a b. a -> Either a b
Left m :~: m
forall {k} (a :: k). a :~: a
Refl
    SOrdering (CmpNat n m)
SGT -> (n :~: n) -> Either (n :~: m) (n :~: n)
forall a b. b -> Either a b
Right n :~: n
forall {k} (a :: k). a :~: a
Refl

-- | Comparison via GADTs.
data Leq n m where
  ZeroLeq :: SNat m -> Leq 0 m
  SuccLeqSucc :: Leq n m -> Leq (n + 1) (m + 1)

type LeqWitness n m = IsTrue (n <=? m)

-- | Since 1.2.0 (argument changed)
data a :<: b where
  ZeroLtSucc :: SNat m -> 0 :<: (m + 1)
  SuccLtSucc :: SNat n -> SNat m -> n :<: m -> (n + 1) :<: (m + 1)

deriving instance Show (a :<: b)

--------------------------------------------------

-- * Total orderings on natural numbers.

--------------------------------------------------
propToBoolLeq :: forall n m. Leq n m -> LeqWitness n m
propToBoolLeq :: forall (n :: Natural) (m :: Natural). Leq n m -> LeqWitness n m
propToBoolLeq (ZeroLeq SNat m
_) = IsTrue 'True
IsTrue (OrdCond (Compare n m) 'True 'True 'False)
Witness
propToBoolLeq (SuccLeqSucc Leq n m
leq) = IsTrue (OrdCond (CmpNat n m) 'True 'True 'False)
-> ((OrdCond (CmpNat n m) 'True 'True 'False ~ 'True) =>
    IsTrue (OrdCond (CmpNat n m) 'True 'True 'False))
-> IsTrue (OrdCond (CmpNat n m) 'True 'True 'False)
forall (b :: Bool) r. IsTrue b -> ((b ~ 'True) => r) -> r
withWitness (Leq n m -> LeqWitness n m
forall (n :: Natural) (m :: Natural). Leq n m -> LeqWitness n m
propToBoolLeq Leq n m
leq) IsTrue 'True
IsTrue (OrdCond (CmpNat n m) 'True 'True 'False)
(OrdCond (CmpNat n m) 'True 'True 'False ~ 'True) =>
IsTrue (OrdCond (CmpNat n m) 'True 'True 'False)
Witness
{-# INLINE propToBoolLeq #-}

boolToPropLeq :: (n <= m) => SNat n -> SNat m -> Leq n m
boolToPropLeq :: forall (n :: Natural) (m :: Natural).
(n <= m) =>
SNat n -> SNat m -> Leq n m
boolToPropLeq SNat n
Zero SNat m
m = SNat m -> Leq 0 m
forall (m :: Natural). SNat m -> Leq 0 m
ZeroLeq SNat m
m
boolToPropLeq (Succ SNat n1
n) (Succ SNat n1
m) = Leq n1 n1 -> Leq (Succ n1) (Succ n1)
forall (n :: Natural) (m :: Natural).
Leq n m -> Leq (n + 1) (m + 1)
SuccLeqSucc (Leq n1 n1 -> Leq (Succ n1) (Succ n1))
-> Leq n1 n1 -> Leq (Succ n1) (Succ n1)
forall a b. (a -> b) -> a -> b
$ SNat n1 -> SNat n1 -> Leq n1 n1
forall (n :: Natural) (m :: Natural).
(n <= m) =>
SNat n -> SNat m -> Leq n m
boolToPropLeq SNat n1
n SNat n1
m
boolToPropLeq (Succ SNat n1
n) SNat m
Zero = Void -> Leq n m
forall a. Void -> a
absurd (Void -> Leq n m) -> Void -> Leq n m
forall a b. (a -> b) -> a -> b
$ SNat n1 -> IsTrue (Succ n1 <=? 0) -> Void
forall (n :: Natural). SNat n -> IsTrue (S n <=? 0) -> Void
succLeqZeroAbsurd SNat n1
n IsTrue 'True
IsTrue (Succ n1 <=? 0)
Witness

leqRhs :: Leq n m -> SNat m
leqRhs :: forall (n :: Natural) (m :: Natural). Leq n m -> SNat m
leqRhs (ZeroLeq SNat m
m) = SNat m
m
leqRhs (SuccLeqSucc Leq n m
leq) = SNat m -> SNat (m + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc (SNat m -> SNat (m + 1)) -> SNat m -> SNat (m + 1)
forall a b. (a -> b) -> a -> b
$ Leq n m -> SNat m
forall (n :: Natural) (m :: Natural). Leq n m -> SNat m
leqRhs Leq n m
leq

leqLhs :: Leq n m -> SNat n
leqLhs :: forall (n :: Natural) (m :: Natural). Leq n m -> SNat n
leqLhs (ZeroLeq SNat m
_) = SNat n
forall (n :: Natural). (n ~ 0) => SNat n
Zero
leqLhs (SuccLeqSucc Leq n m
leq) = SNat n -> SNat (n + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc (SNat n -> SNat (n + 1)) -> SNat n -> SNat (n + 1)
forall a b. (a -> b) -> a -> b
$ Leq n m -> SNat n
forall (n :: Natural) (m :: Natural). Leq n m -> SNat n
leqLhs Leq n m
leq

propToBoolLt :: n :<: m -> IsTrue (n <? m)
propToBoolLt :: forall (n :: Natural) (m :: Natural). (n :<: m) -> IsTrue (n <? m)
propToBoolLt (ZeroLtSucc (SNat m
sm :: SNat m)) = 
  (CmpNat 0 m :~: 'LT)
-> ((CmpNat 0 m ~ 'LT) =>
    IsTrue (OrdCond (CmpNat 0 m) 'True 'False 'False))
-> IsTrue (OrdCond (CmpNat 0 m) 'True 'False 'False)
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat m -> CmpNat 0 (m + 1) :~: 'LT
forall (a :: Natural). SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero SNat m
sm) IsTrue 'True
IsTrue (OrdCond (CmpNat 0 m) 'True 'False 'False)
(CmpNat 0 m ~ 'LT) =>
IsTrue (OrdCond (CmpNat 0 m) 'True 'False 'False)
Witness
propToBoolLt (SuccLtSucc SNat n
sn SNat m
sm n :<: m
lt) =
  (CmpNat n m :~: CmpNat n m)
-> ((CmpNat n m ~ CmpNat n m) =>
    IsTrue (OrdCond (Compare n m) 'True 'False 'False))
-> IsTrue (OrdCond (Compare n m) 'True 'False 'False)
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n -> SNat m -> CmpNat n m :~: CmpNat (n + 1) (m + 1)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat n
sn SNat m
sm) (((CmpNat n m ~ CmpNat n m) =>
  IsTrue (OrdCond (Compare n m) 'True 'False 'False))
 -> IsTrue (OrdCond (Compare n m) 'True 'False 'False))
-> ((CmpNat n m ~ CmpNat n m) =>
    IsTrue (OrdCond (Compare n m) 'True 'False 'False))
-> IsTrue (OrdCond (Compare n m) 'True 'False 'False)
forall a b. (a -> b) -> a -> b
$
  IsTrue (OrdCond (CmpNat n m) 'True 'False 'False)
-> ((OrdCond (CmpNat n m) 'True 'False 'False ~ 'True) =>
    IsTrue (OrdCond (CmpNat n m) 'True 'False 'False))
-> IsTrue (OrdCond (CmpNat n m) 'True 'False 'False)
forall (b :: Bool) r. IsTrue b -> ((b ~ 'True) => r) -> r
withWitness ((n :<: m) -> IsTrue (n <? m)
forall (n :: Natural) (m :: Natural). (n :<: m) -> IsTrue (n <? m)
propToBoolLt n :<: m
lt) IsTrue 'True
IsTrue (OrdCond (CmpNat n m) 'True 'False 'False)
(OrdCond (CmpNat n m) 'True 'False 'False ~ 'True) =>
IsTrue (OrdCond (CmpNat n m) 'True 'False 'False)
Witness

boolToPropLt :: n < m => SNat n -> SNat m -> n :<: m
boolToPropLt :: forall (n :: Natural) (m :: Natural).
(n < m) =>
SNat n -> SNat m -> n :<: m
boolToPropLt SNat n
Zero (Succ SNat n1
sn) = SNat n1 -> 0 :<: Succ n1
forall (n :: Natural). SNat n -> 0 :<: (n + 1)
ZeroLtSucc SNat n1
sn
boolToPropLt (Succ SNat n1
n) SNat m
Zero = ('True :~: 'False) -> n :<: m
forall x. ('True :~: 'False) -> x
forall a x. Empty a => a -> x
eliminate (('True :~: 'False) -> n :<: m) -> ('True :~: 'False) -> n :<: m
forall a b. (a -> b) -> a -> b
$
  SBool 'True -> 'True :~: 'True
forall {k} (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start SBool 'True
STrue
  ('True :~: 'True) -> SBool 'True -> 'True :~: 'True
forall {k1} {k2} (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= (SNat n1 -> SNat n
forall (n :: Natural) (n1 :: Natural).
(n ~ Succ n1) =>
SNat n1 -> SNat n
Succ SNat n1
n SNat n -> SNat 0 -> SBool (n <? 0)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SBool (n <? m)
%<? SNat 0
forall (n :: Natural). (n ~ 0) => SNat n
Zero)
  ('True :~: 'True) -> SBool 'True -> 'True :~: 'True
forall {k1} {k2} (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SOrdering (CmpNat n 0)
-> SBool 'True
-> SBool 'False
-> SBool 'False
-> SBool (OrdCond (CmpNat n 0) 'True 'False 'False)
forall {k} (o :: Ordering) (f :: k -> Type) (lt :: k) (eq :: k)
       (gt :: k).
SOrdering o -> f lt -> f eq -> f gt -> f (OrdCond o lt eq gt)
sOrdCond (SNat n -> SNat 0 -> SOrdering (CmpNat n 0)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat (SNat n1 -> SNat n
forall (n :: Natural) (n1 :: Natural).
(n ~ Succ n1) =>
SNat n1 -> SNat n
Succ SNat n1
n) SNat 0
forall (n :: Natural). (n ~ 0) => SNat n
Zero) SBool 'True
STrue SBool 'False
SFalse SBool 'False
SFalse
  ('True :~: 'True) -> Reason (:~:) 'True 'False -> 'True :~: 'False
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering 'GT
-> SBool 'True
-> SBool 'False
-> SBool 'False
-> SBool (OrdCond 'GT 'True 'False 'False)
forall {k} (o :: Ordering) (f :: k -> Type) (lt :: k) (eq :: k)
       (gt :: k).
SOrdering o -> f lt -> f eq -> f gt -> f (OrdCond o lt eq gt)
sOrdCond SOrdering 'GT
SGT SBool 'True
STrue SBool 'False
SFalse SBool 'False
SFalse
    SBool 'False -> ('True :~: 'False) -> Reason (:~:) 'True 'False
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (CmpNat n 0 :~: 'GT)
-> SBool 'True
-> SBool 'False
-> SBool 'False
-> OrdCond (CmpNat n 0) 'True 'False 'False
   :~: OrdCond 'GT 'True 'False 'False
forall {k} (o :: Ordering) (o' :: Ordering) (proxy :: k -> Type)
       (a :: k) (proxy' :: k -> Type) (b :: k) (c :: k).
(o :~: o')
-> proxy a
-> proxy' b
-> proxy' c
-> OrdCond o a b c :~: OrdCond o' a b c
sOrdCondCong1 (SNat n1 -> CmpNat (Succ n1) 0 :~: 'GT
forall (a :: Natural). SNat a -> CmpNat (Succ a) 0 :~: 'GT
cmpSuccZeroGT SNat n1
n) SBool 'True
STrue SBool 'False
SFalse SBool 'False
SFalse
  ('True :~: 'False) -> SBool 'False -> 'True :~: 'False
forall {k1} {k2} (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SBool 'False
SFalse
boolToPropLt (Succ SNat n1
n) (Succ SNat n1
m) = 
  (CmpNat n1 n1 :~: CmpNat n m)
-> ((CmpNat n1 n1 ~ CmpNat n m) => n :<: m) -> n :<: m
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n1 -> SNat n1 -> CmpNat n1 n1 :~: CmpNat (Succ n1) (Succ n1)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat n1
n SNat n1
m) (((CmpNat n1 n1 ~ CmpNat n m) => n :<: m) -> n :<: m)
-> ((CmpNat n1 n1 ~ CmpNat n m) => n :<: m) -> n :<: m
forall a b. (a -> b) -> a -> b
$
  SNat n1 -> SNat n1 -> (n1 :<: n1) -> Succ n1 :<: Succ n1
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n :<: m) -> (n + 1) :<: (m + 1)
SuccLtSucc SNat n1
n SNat n1
m (SNat n1 -> SNat n1 -> n1 :<: n1
forall (n :: Natural) (m :: Natural).
(n < m) =>
SNat n -> SNat m -> n :<: m
boolToPropLt SNat n1
n SNat n1
m)

#if MIN_VERSION_ghc(9,2,1)
type Min m n = DTO.Min @Nat m n
#else
type Min m n = OrdCond (CmpNat m n) m m n
#endif

sMin :: SNat n -> SNat m -> SNat (Min n m)
{-# INLINE sMin #-}
sMin :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin = (Natural -> Natural -> Natural)
-> SNat n -> SNat m -> SNat (OrdCond (CmpNat n m) n n m)
forall (n :: Natural) (m :: Natural) (k :: Natural).
(Natural -> Natural -> Natural) -> SNat n -> SNat m -> SNat k
unsafeLiftSBin Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
min

sMax :: SNat n -> SNat m -> SNat (Max n m)
{-# INLINE sMax #-}
sMax :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Max n m)
sMax = (Natural -> Natural -> Natural)
-> SNat n -> SNat m -> SNat (OrdCond (CmpNat n m) m m n)
forall (n :: Natural) (m :: Natural) (k :: Natural).
(Natural -> Natural -> Natural) -> SNat n -> SNat m -> SNat k
unsafeLiftSBin Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
max

#if MIN_VERSION_ghc(9,2,1)
type Max m n = DTO.Max @Nat m n
#else
type Max m n = OrdCond (CmpNat m n) n n m
#endif

infix 4 <?, <, >=?, >=, >, >?

#if MIN_VERSION_ghc(9,2,1)
type (n :: Nat) <? m = n DTO.<? m
#else
type n <? m = OrdCond (CmpNat n m) 'True 'False 'False
#endif

(%<?) :: SNat n -> SNat m -> SBool (n <? m)
SNat n
n %<? :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SBool (n <? m)
%<? SNat m
m = SOrdering (CmpNat n m)
-> SBool 'True
-> SBool 'False
-> SBool 'False
-> SBool (OrdCond (CmpNat n m) 'True 'False 'False)
forall {k} (o :: Ordering) (f :: k -> Type) (lt :: k) (eq :: k)
       (gt :: k).
SOrdering o -> f lt -> f eq -> f gt -> f (OrdCond o lt eq gt)
sOrdCond (SNat n -> SNat m -> SOrdering (CmpNat n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n SNat m
m) SBool 'True
STrue SBool 'False
SFalse SBool 'False
SFalse

#if MIN_VERSION_ghc(9,2,2)
type (n :: Nat) < m = n DTO.< m
#else
type n < m = (n <? m) ~ 'True
#endif

#if MIN_VERSION_ghc(9,2,1)
type n >=? m = (DTO.>=?) @Nat n m
#else
type n >=? m = OrdCond (CmpNat n m) 'False 'True 'True
#endif

(%>=?) :: SNat n -> SNat m -> SBool (n >=? m)
SNat n
n %>=? :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SBool (n >=? m)
%>=? SNat m
m = SOrdering (CmpNat n m)
-> SBool 'False
-> SBool 'True
-> SBool 'True
-> SBool (OrdCond (CmpNat n m) 'False 'True 'True)
forall {k} (o :: Ordering) (f :: k -> Type) (lt :: k) (eq :: k)
       (gt :: k).
SOrdering o -> f lt -> f eq -> f gt -> f (OrdCond o lt eq gt)
sOrdCond (SNat n -> SNat m -> SOrdering (CmpNat n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n SNat m
m) SBool 'False
SFalse SBool 'True
STrue SBool 'True
STrue

#if MIN_VERSION_ghc(9,2,1)
type (n :: Nat) >= m = n DTO.>= m
#else
type n >= m = (n >=? m) ~ 'True
#endif

#if MIN_VERSION_ghc(9,2,1)
type (n :: Nat) >? m = n DTO.>? m
#else
type n >? m = OrdCond (CmpNat n m) 'False 'False 'True
#endif

(%>?) :: SNat n -> SNat m -> SBool (n >? m)
SNat n
n %>? :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SBool (n >? m)
%>? SNat m
m = SOrdering (CmpNat n m)
-> SBool 'False
-> SBool 'False
-> SBool 'True
-> SBool (OrdCond (CmpNat n m) 'False 'False 'True)
forall {k} (o :: Ordering) (f :: k -> Type) (lt :: k) (eq :: k)
       (gt :: k).
SOrdering o -> f lt -> f eq -> f gt -> f (OrdCond o lt eq gt)
sOrdCond (SNat n -> SNat m -> SOrdering (CmpNat n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n SNat m
m) SBool 'False
SFalse SBool 'False
SFalse SBool 'True
STrue

#if MIN_VERSION_ghc(9,2,1)
type (n :: Nat) > m = n DTO.> m
#else
type n > m = (n >? m) ~ 'True
#endif

infix 4 %>?, %<?, %>=?

ordCondDistrib :: proxy f -> SOrdering o -> p l -> p' e -> p'' g ->
  OrdCond o (f l) (f e) (f g) :~: f (OrdCond o l e g)
ordCondDistrib :: forall {k} {k} (proxy :: (k -> k) -> Type) (f :: k -> k)
       (o :: Ordering) (p :: k -> Type) (l :: k) (p' :: k -> Type)
       (e :: k) (p'' :: k -> Type) (g :: k).
proxy f
-> SOrdering o
-> p l
-> p' e
-> p'' g
-> OrdCond o (f l) (f e) (f g) :~: f (OrdCond o l e g)
ordCondDistrib proxy f
_ SOrdering o
SLT p l
_ p' e
_ p'' g
_ = f l :~: f l
OrdCond o (f l) (f e) (f g) :~: f (OrdCond o l e g)
forall {k} (a :: k). a :~: a
Refl
ordCondDistrib proxy f
_ SOrdering o
SEQ p l
_ p' e
_ p'' g
_ = f e :~: f e
OrdCond o (f l) (f e) (f g) :~: f (OrdCond o l e g)
forall {k} (a :: k). a :~: a
Refl
ordCondDistrib proxy f
_ SOrdering o
SGT p l
_ p' e
_ p'' g
_ = f g :~: f g
OrdCond o (f l) (f e) (f g) :~: f (OrdCond o l e g)
forall {k} (a :: k). a :~: a
Refl

leqOrdCond
  :: SNat n -> SNat m -> (n <=? m) :~: OrdCond (CmpNat n m) 'True 'True 'False
#if MIN_VERSION_ghc(9,2,1)
leqOrdCond :: forall (n :: Natural) (m :: Natural).
SNat n
-> SNat m -> (n <=? m) :~: OrdCond (CmpNat n m) 'True 'True 'False
leqOrdCond SNat n
_ SNat m
_ = OrdCond (CmpNat n m) 'True 'True 'False
:~: OrdCond (CmpNat n m) 'True 'True 'False
OrdCond (Compare n m) 'True 'True 'False
:~: OrdCond (CmpNat n m) 'True 'True 'False
forall {k} (a :: k). a :~: a
Refl
#else
leqOrdCond Zero n =
  case cmpZero' n of
    Left Refl -> Refl
    Right Refl -> Refl
leqOrdCond (Succ m) Zero = 
  gcastWith (succLeqZeroAbsurd' m) $
  gcastWith (cmpSuccZeroGT m) $
  Refl
leqOrdCond (Succ m) (Succ n) =
  gcastWith (cmpSucc m n) $
  start (Succ m %<=? Succ n)
  === (m %<=? n) `because` sym (leqSucc' m n)
  === sOrdCond (sCmpNat m n) STrue STrue SFalse `because` leqOrdCond m n
#endif

data LeqView n m where
  LeqZero :: SNat n -> LeqView 0 n
  LeqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView (Succ n) (Succ m)

data DiffNat n m where
  DiffNat :: SNat n -> SNat m -> DiffNat n (n + m)

newtype LeqWitPf n = LeqWitPf {forall (n :: Natural).
LeqWitPf n
-> forall (m :: Natural). SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitPf :: forall m. SNat m -> IsTrue (n <=? m) -> DiffNat n m}

succDiffNat :: SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m)
succDiffNat :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m)
succDiffNat SNat n
_ SNat m
_ (DiffNat SNat n
n SNat m
m) = (((n + 1) + m) :~: (m + 1))
-> ((((n + 1) + m) ~ (m + 1)) => DiffNat (n + 1) (m + 1))
-> DiffNat (n + 1) (m + 1)
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n -> SNat m -> ((n + 1) + m) :~: S (n + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat n
n SNat m
m) (((((n + 1) + m) ~ (m + 1)) => DiffNat (n + 1) (m + 1))
 -> DiffNat (n + 1) (m + 1))
-> ((((n + 1) + m) ~ (m + 1)) => DiffNat (n + 1) (m + 1))
-> DiffNat (n + 1) (m + 1)
forall a b. (a -> b) -> a -> b
$ SNat (n + 1) -> SNat m -> DiffNat (n + 1) ((n + 1) + m)
forall (n :: Natural) (n :: Natural).
SNat n -> SNat n -> DiffNat n (n + n)
DiffNat (SNat n -> SNat (n + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m

-- | Since 1.0.0.0 (type changed)
coerceLeqL ::
  forall n m l.
  n :~: m ->
  SNat l ->
  IsTrue (n <=? l) ->
  IsTrue (m <=? l)
coerceLeqL :: forall (n :: Natural) (m :: Natural) (l :: Natural).
(n :~: m) -> SNat l -> IsTrue (n <=? l) -> IsTrue (m <=? l)
coerceLeqL n :~: m
Refl SNat l
_ IsTrue (n <=? l)
Witness = IsTrue 'True
IsTrue (OrdCond (Compare m l) 'True 'True 'False)
Witness

-- | Since 1.0.0.0 (type changed)
coerceLeqR ::
  forall n m l.
  SNat l ->
  n :~: m ->
  IsTrue (l <=? n) ->
  IsTrue (l <=? m)
coerceLeqR :: forall (n :: Natural) (m :: Natural) (l :: Natural).
SNat l -> (n :~: m) -> IsTrue (l <=? n) -> IsTrue (l <=? m)
coerceLeqR SNat l
_ n :~: m
Refl IsTrue (l <=? n)
Witness = IsTrue 'True
IsTrue (OrdCond (Compare l m) 'True 'True 'False)
Witness

compareCongR :: SNat a -> b :~: c -> CmpNat a b :~: CmpNat a c
compareCongR :: forall (a :: Natural) (b :: Natural) (c :: Natural).
SNat a -> (b :~: c) -> CmpNat a b :~: CmpNat a c
compareCongR SNat a
_ b :~: c
Refl = CmpNat a b :~: CmpNat a b
CmpNat a b :~: CmpNat a c
forall {k} (a :: k). a :~: a
Refl

sLeqCong :: a :~: b -> c :~: d -> (a <= c) :~: (b <= d)
sLeqCong :: forall {t} (a :: t) (b :: t) (c :: t) (d :: t).
(a :~: b) -> (c :~: d) -> (a <= c) :~: (b <= d)
sLeqCong a :~: b
Refl c :~: d
Refl = Assert (OrdCond (Compare a c) 'True 'True 'False) (TypeError ...)
:~: Assert
      (OrdCond (Compare a c) 'True 'True 'False) (TypeError ...)
Assert (OrdCond (Compare a c) 'True 'True 'False) (TypeError ...)
:~: Assert
      (OrdCond (Compare b d) 'True 'True 'False) (TypeError ...)
forall {k} (a :: k). a :~: a
Refl

sLeqCongL :: a :~: b -> SNat c -> (a <= c) :~: (b <= c)
sLeqCongL :: forall (a :: Natural) (b :: Natural) (c :: Natural).
(a :~: b) -> SNat c -> (a <= c) :~: (b <= c)
sLeqCongL a :~: b
Refl SNat c
_ = Assert (OrdCond (CmpNat a c) 'True 'True 'False) (TypeError ...)
:~: Assert
      (OrdCond (CmpNat a c) 'True 'True 'False) (TypeError ...)
Assert (OrdCond (Compare a c) 'True 'True 'False) (TypeError ...)
:~: Assert
      (OrdCond (Compare b c) 'True 'True 'False) (TypeError ...)
forall {k} (a :: k). a :~: a
Refl

sLeqCongR :: SNat a -> b :~: c -> (a <= b) :~: (a <= c)
sLeqCongR :: forall (a :: Natural) (b :: Natural) (c :: Natural).
SNat a -> (b :~: c) -> (a <= b) :~: (a <= c)
sLeqCongR SNat a
_ b :~: c
Refl = Assert (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...)
:~: Assert
      (OrdCond (CmpNat a b) 'True 'True 'False) (TypeError ...)
Assert (OrdCond (Compare a b) 'True 'True 'False) (TypeError ...)
:~: Assert
      (OrdCond (Compare a c) 'True 'True 'False) (TypeError ...)
forall {k} (a :: k). a :~: a
Refl

newtype LeqViewRefl n = LeqViewRefl {forall (n :: Natural). LeqViewRefl n -> LeqView n n
proofLeqViewRefl :: LeqView n n}

leqToCmp ::
  SNat a ->
  SNat b ->
  IsTrue (a <=? b) ->
  Either (a :~: b) (CmpNat a b :~: 'LT)
leqToCmp :: forall (a :: Natural) (b :: Natural).
SNat a
-> SNat b
-> IsTrue (a <=? b)
-> Either (a :~: b) (CmpNat a b :~: 'LT)
leqToCmp SNat a
n SNat b
m IsTrue (a <=? b)
Witness =
  case SNat a
n SNat a -> SNat b -> Equality a b
forall (l :: Natural) (r :: Natural).
SNat l -> SNat r -> Equality l r
%~ SNat b
m of
    Equality a b
Equal -> (a :~: b) -> Either (a :~: b) ('EQ :~: 'LT)
forall a b. a -> Either a b
Left a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    Equality a b
NonEqual -> (CmpNat a b :~: CmpNat a b)
-> Either (a :~: b) (CmpNat a b :~: CmpNat a b)
forall a b. b -> Either a b
Right CmpNat a b :~: CmpNat a b
forall {k} (a :: k). a :~: a
Refl

eqlCmpEQ :: SNat a -> SNat b -> a :~: b -> CmpNat a b :~: 'EQ
eqlCmpEQ :: forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ
eqlCmpEQ SNat a
_ SNat b
_ a :~: b
Refl = CmpNat a b :~: 'EQ
'EQ :~: 'EQ
forall {k} (a :: k). a :~: a
Refl

eqToRefl :: SNat a -> SNat b -> CmpNat a b :~: 'EQ -> a :~: b
eqToRefl :: forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> (CmpNat a b :~: 'EQ) -> a :~: b
eqToRefl SNat a
_ SNat b
_ CmpNat a b :~: 'EQ
Refl = a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl

flipCmpNat ::
  SNat a ->
  SNat b ->
  FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat :: forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat SNat a
n SNat b
m = case SNat a -> SNat b -> SOrdering (CmpNat a b)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
n SNat b
m of
  SOrdering (CmpNat a b)
SGT -> 'LT :~: 'LT
FlipOrdering (CmpNat a b) :~: CmpNat b a
forall {k} (a :: k). a :~: a
Refl
  SOrdering (CmpNat a b)
SLT -> 'GT :~: 'GT
FlipOrdering (CmpNat a b) :~: CmpNat b a
forall {k} (a :: k). a :~: a
Refl
  SOrdering (CmpNat a b)
SEQ -> 'EQ :~: 'EQ
FlipOrdering (CmpNat a b) :~: CmpNat b a
forall {k} (a :: k). a :~: a
Refl

ltToNeq ::
  SNat a ->
  SNat b ->
  CmpNat a b :~: 'LT ->
  a :~: b ->
  Void
ltToNeq :: forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> (a :~: b) -> Void
ltToNeq SNat a
a SNat b
b CmpNat a b :~: 'LT
aLTb a :~: b
aEQb =
  ('LT :~: 'EQ) -> Void
forall x. ('LT :~: 'EQ) -> x
forall a x. Empty a => a -> x
eliminate (('LT :~: 'EQ) -> Void) -> ('LT :~: 'EQ) -> Void
forall a b. (a -> b) -> a -> b
$
    SOrdering 'LT -> 'LT :~: 'LT
forall {k} (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start SOrdering 'LT
SLT
      ('LT :~: 'LT)
-> Reason (:~:) 'LT (CmpNat a b) -> 'LT :~: CmpNat a b
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat a -> SNat b -> SOrdering (CmpNat a b)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
a SNat b
b SOrdering (CmpNat a b)
-> ('LT :~: CmpNat a b) -> Reason (:~:) 'LT (CmpNat a b)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (CmpNat a b :~: 'LT) -> 'LT :~: CmpNat a b
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym CmpNat a b :~: 'LT
aLTb
      ('LT :~: CmpNat a b)
-> Reason (:~:) (CmpNat a b) 'EQ -> 'LT :~: 'EQ
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering 'EQ
SEQ SOrdering 'EQ
-> (CmpNat a b :~: 'EQ) -> Reason (:~:) (CmpNat a b) 'EQ
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ
forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ
eqlCmpEQ SNat a
a SNat b
b a :~: b
aEQb

leqNeqToLT :: SNat a -> SNat b -> IsTrue (a <=? b) -> (a :~: b -> Void) -> CmpNat a b :~: 'LT
leqNeqToLT :: forall (a :: Natural) (b :: Natural).
SNat a
-> SNat b
-> IsTrue (a <=? b)
-> ((a :~: b) -> Void)
-> CmpNat a b :~: 'LT
leqNeqToLT SNat a
a SNat b
b IsTrue (a <=? b)
aLEQb (a :~: b) -> Void
aNEQb = ((a :~: b) -> CmpNat a b :~: 'LT)
-> ((CmpNat a b :~: 'LT) -> CmpNat a b :~: 'LT)
-> Either (a :~: b) (CmpNat a b :~: 'LT)
-> CmpNat a b :~: 'LT
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Void -> CmpNat a b :~: 'LT
forall a. Void -> a
absurd (Void -> CmpNat a b :~: 'LT)
-> ((a :~: b) -> Void) -> (a :~: b) -> CmpNat a b :~: 'LT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a :~: b) -> Void
aNEQb) (CmpNat a b :~: 'LT) -> CmpNat a b :~: 'LT
forall a. a -> a
id (Either (a :~: b) (CmpNat a b :~: 'LT) -> CmpNat a b :~: 'LT)
-> Either (a :~: b) (CmpNat a b :~: 'LT) -> CmpNat a b :~: 'LT
forall a b. (a -> b) -> a -> b
$ SNat a
-> SNat b
-> IsTrue (a <=? b)
-> Either (a :~: b) (CmpNat a b :~: 'LT)
forall (a :: Natural) (b :: Natural).
SNat a
-> SNat b
-> IsTrue (a <=? b)
-> Either (a :~: b) (CmpNat a b :~: 'LT)
leqToCmp SNat a
a SNat b
b IsTrue (a <=? b)
aLEQb

succLeqToLT :: SNat a -> SNat b -> IsTrue (S a <=? b) -> CmpNat a b :~: 'LT
succLeqToLT :: forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> IsTrue (S a <=? b) -> CmpNat a b :~: 'LT
succLeqToLT SNat a
_ SNat b
_ IsTrue (S a <=? b)
Witness = CmpNat a b :~: 'LT
'LT :~: 'LT
forall {k} (a :: k). a :~: a
Refl

ltToLeq ::
  SNat a ->
  SNat b ->
  CmpNat a b :~: 'LT ->
  IsTrue (a <=? b)
ltToLeq :: forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)
ltToLeq SNat a
_ SNat b
_ CmpNat a b :~: 'LT
Refl = IsTrue 'True
IsTrue (OrdCond (Compare a b) 'True 'True 'False)
Witness

gtToLeq ::
  SNat a ->
  SNat b ->
  CmpNat a b :~: 'GT ->
  IsTrue (b <=? a)
gtToLeq :: forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> (CmpNat a b :~: 'GT) -> IsTrue (b <=? a)
gtToLeq SNat a
_ SNat b
_ CmpNat a b :~: 'GT
Refl = IsTrue 'True
IsTrue (OrdCond (Compare b a) 'True 'True 'False)
Witness

congFlipOrdering ::
  a :~: b -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering :: forall (a :: Ordering) (b :: Ordering).
(a :~: b) -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering a :~: b
Refl = FlipOrdering a :~: FlipOrdering a
FlipOrdering a :~: FlipOrdering b
forall {k} (a :: k). a :~: a
Refl

ltToSuccLeq ::
  SNat a ->
  SNat b ->
  CmpNat a b :~: 'LT ->
  IsTrue (Succ a <=? b)
ltToSuccLeq :: forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)
ltToSuccLeq SNat a
_ SNat b
_ CmpNat a b :~: 'LT
Refl = IsTrue 'True
IsTrue (OrdCond (Compare (a + 1) b) 'True 'True 'False)
Witness

cmpZero :: SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero :: forall (a :: Natural). SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero SNat a
_ = CmpNat 0 (a + 1) :~: 'LT
'LT :~: 'LT
forall {k} (a :: k). a :~: a
Refl

cmpSuccZeroGT :: SNat a -> CmpNat (Succ a) 0 :~: 'GT
cmpSuccZeroGT :: forall (a :: Natural). SNat a -> CmpNat (Succ a) 0 :~: 'GT
cmpSuccZeroGT SNat a
_ = CmpNat (a + 1) 0 :~: 'GT
'GT :~: 'GT
forall {k} (a :: k). a :~: a
Refl

leqToGT ::
  SNat a ->
  SNat b ->
  IsTrue (Succ b <=? a) ->
  CmpNat a b :~: 'GT
leqToGT :: forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> IsTrue (Succ b <=? a) -> CmpNat a b :~: 'GT
leqToGT SNat a
_ SNat b
_ IsTrue (Succ b <=? a)
Witness = CmpNat a b :~: 'GT
'GT :~: 'GT
forall {k} (a :: k). a :~: a
Refl

cmpZero' :: SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
cmpZero' :: forall (a :: Natural).
SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
cmpZero' SNat a
n =
  case SNat a -> ZeroOrSucc a
forall (n :: Natural). SNat n -> ZeroOrSucc n
zeroOrSucc SNat a
n of
    ZeroOrSucc a
IsZero -> (CmpNat 0 a :~: 'EQ)
-> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
forall a b. a -> Either a b
Left ((CmpNat 0 a :~: 'EQ)
 -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT))
-> (CmpNat 0 a :~: 'EQ)
-> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
forall a b. (a -> b) -> a -> b
$ SNat 0 -> SNat a -> (0 :~: a) -> CmpNat 0 a :~: 'EQ
forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ
eqlCmpEQ SNat 0
sZero SNat a
n 0 :~: a
0 :~: 0
forall {k} (a :: k). a :~: a
Refl
    IsSucc SNat n1
n' -> (CmpNat 0 a :~: 'LT)
-> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
forall a b. b -> Either a b
Right ((CmpNat 0 a :~: 'LT)
 -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT))
-> (CmpNat 0 a :~: 'LT)
-> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
forall a b. (a -> b) -> a -> b
$ SNat n1 -> CmpNat 0 (n1 + 1) :~: 'LT
forall (a :: Natural). SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero SNat n1
n'

zeroNoLT :: SNat a -> CmpNat a 0 :~: 'LT -> Void
zeroNoLT :: forall (a :: Natural). SNat a -> (CmpNat a 0 :~: 'LT) -> Void
zeroNoLT SNat a
n CmpNat a 0 :~: 'LT
eql =
  case SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
forall (a :: Natural).
SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
cmpZero' SNat a
n of
    Left CmpNat 0 a :~: 'EQ
cmp0nEQ ->
      ('GT :~: 'EQ) -> Void
forall x. ('GT :~: 'EQ) -> x
forall a x. Empty a => a -> x
eliminate (('GT :~: 'EQ) -> Void) -> ('GT :~: 'EQ) -> Void
forall a b. (a -> b) -> a -> b
$
        SOrdering 'GT -> 'GT :~: 'GT
forall {k} (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start SOrdering 'GT
SGT
          ('GT :~: 'GT) -> SOrdering 'GT -> 'GT :~: 'GT
forall {k1} {k2} (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SOrdering 'LT -> SOrdering (FlipOrdering 'LT)
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering SOrdering 'LT
SLT
          ('GT :~: 'GT)
-> Reason (:~:) 'GT (FlipOrdering (CmpNat a 0))
-> 'GT :~: FlipOrdering (CmpNat a 0)
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering (CmpNat a 0) -> SOrdering (FlipOrdering (CmpNat a 0))
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering (SNat a -> SNat 0 -> SOrdering (CmpNat a 0)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
n SNat 0
sZero) SOrdering (FlipOrdering (CmpNat a 0))
-> ('GT :~: FlipOrdering (CmpNat a 0))
-> Reason (:~:) 'GT (FlipOrdering (CmpNat a 0))
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` ('LT :~: CmpNat a 0)
-> FlipOrdering 'LT :~: FlipOrdering (CmpNat a 0)
forall (a :: Ordering) (b :: Ordering).
(a :~: b) -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering ((CmpNat a 0 :~: 'LT) -> 'LT :~: CmpNat a 0
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym CmpNat a 0 :~: 'LT
eql)
          ('GT :~: FlipOrdering (CmpNat a 0))
-> Reason (:~:) (FlipOrdering (CmpNat a 0)) (CmpNat 0 a)
-> 'GT :~: CmpNat 0 a
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat 0 -> SNat a -> SOrdering (CmpNat 0 a)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat 0
sZero SNat a
n SOrdering (CmpNat 0 a)
-> (FlipOrdering (CmpNat a 0) :~: CmpNat 0 a)
-> Reason (:~:) (FlipOrdering (CmpNat a 0)) (CmpNat 0 a)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat a -> SNat 0 -> FlipOrdering (CmpNat a 0) :~: CmpNat 0 a
forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat SNat a
n SNat 0
sZero
          ('GT :~: CmpNat 0 a)
-> Reason (:~:) (CmpNat 0 a) 'EQ -> 'GT :~: 'EQ
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering 'EQ
SEQ SOrdering 'EQ
-> (CmpNat 0 a :~: 'EQ) -> Reason (:~:) (CmpNat 0 a) 'EQ
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` CmpNat 0 a :~: 'EQ
cmp0nEQ
    Right CmpNat 0 a :~: 'LT
cmp0nLT ->
      ('GT :~: 'LT) -> Void
forall x. ('GT :~: 'LT) -> x
forall a x. Empty a => a -> x
eliminate (('GT :~: 'LT) -> Void) -> ('GT :~: 'LT) -> Void
forall a b. (a -> b) -> a -> b
$
        SOrdering 'GT -> 'GT :~: 'GT
forall {k} (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start SOrdering 'GT
SGT
          ('GT :~: 'GT) -> SOrdering 'GT -> 'GT :~: 'GT
forall {k1} {k2} (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SOrdering 'LT -> SOrdering (FlipOrdering 'LT)
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering SOrdering 'LT
SLT
          ('GT :~: 'GT)
-> Reason (:~:) 'GT (FlipOrdering (CmpNat a 0))
-> 'GT :~: FlipOrdering (CmpNat a 0)
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering (CmpNat a 0) -> SOrdering (FlipOrdering (CmpNat a 0))
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering (SNat a -> SNat 0 -> SOrdering (CmpNat a 0)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
n SNat 0
sZero) SOrdering (FlipOrdering (CmpNat a 0))
-> ('GT :~: FlipOrdering (CmpNat a 0))
-> Reason (:~:) 'GT (FlipOrdering (CmpNat a 0))
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` ('LT :~: CmpNat a 0)
-> FlipOrdering 'LT :~: FlipOrdering (CmpNat a 0)
forall (a :: Ordering) (b :: Ordering).
(a :~: b) -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering ((CmpNat a 0 :~: 'LT) -> 'LT :~: CmpNat a 0
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym CmpNat a 0 :~: 'LT
eql)
          ('GT :~: FlipOrdering (CmpNat a 0))
-> Reason (:~:) (FlipOrdering (CmpNat a 0)) (CmpNat 0 a)
-> 'GT :~: CmpNat 0 a
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat 0 -> SNat a -> SOrdering (CmpNat 0 a)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat 0
sZero SNat a
n SOrdering (CmpNat 0 a)
-> (FlipOrdering (CmpNat a 0) :~: CmpNat 0 a)
-> Reason (:~:) (FlipOrdering (CmpNat a 0)) (CmpNat 0 a)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat a -> SNat 0 -> FlipOrdering (CmpNat a 0) :~: CmpNat 0 a
forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat SNat a
n SNat 0
sZero
          ('GT :~: CmpNat 0 a)
-> Reason (:~:) (CmpNat 0 a) 'LT -> 'GT :~: 'LT
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering 'LT
SLT SOrdering 'LT
-> (CmpNat 0 a :~: 'LT) -> Reason (:~:) (CmpNat 0 a) 'LT
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` CmpNat 0 a :~: 'LT
cmp0nLT

ltRightPredSucc :: SNat a -> SNat b -> CmpNat a b :~: 'LT -> b :~: Succ (Pred b)
ltRightPredSucc :: forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> b :~: Succ (Pred b)
ltRightPredSucc SNat a
_ SNat b
_ CmpNat a b :~: 'LT
Refl = b :~: b
b :~: ((b - 1) + 1)
forall {k} (a :: k). a :~: a
Refl

cmpSucc :: SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat n
_ SNat m
_ = CmpNat n m :~: CmpNat n m
CmpNat n m :~: CmpNat (n + 1) (m + 1)
forall {k} (a :: k). a :~: a
Refl

ltSucc :: SNat a -> CmpNat a (Succ a) :~: 'LT
ltSucc :: forall (a :: Natural). SNat a -> CmpNat a (Succ a) :~: 'LT
ltSucc SNat a
_ = CmpNat a (a + 1) :~: 'LT
'LT :~: 'LT
forall {k} (a :: k). a :~: a
Refl

cmpSuccStepR ::
  forall n m.
  SNat n ->
  SNat m ->
  CmpNat n m :~: 'LT ->
  CmpNat n (Succ m) :~: 'LT
cmpSuccStepR :: forall (n :: Natural) (m :: Natural).
SNat n
-> SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
cmpSuccStepR SNat n
_ SNat m
_ CmpNat n m :~: 'LT
Refl = CmpNat n (m + 1) :~: 'LT
'LT :~: 'LT
forall {k} (a :: k). a :~: a
Refl

ltSuccLToLT ::
  SNat n ->
  SNat m ->
  CmpNat (Succ n) m :~: 'LT ->
  CmpNat n m :~: 'LT
ltSuccLToLT :: forall (n :: Natural) (m :: Natural).
SNat n
-> SNat m -> (CmpNat (Succ n) m :~: 'LT) -> CmpNat n m :~: 'LT
ltSuccLToLT SNat n
n SNat m
m CmpNat (Succ n) m :~: 'LT
snLTm =
  case SNat m -> ZeroOrSucc m
forall (n :: Natural). SNat n -> ZeroOrSucc n
zeroOrSucc SNat m
m of
    ZeroOrSucc m
IsZero -> Void -> CmpNat n m :~: 'LT
forall a. Void -> a
absurd (Void -> CmpNat n m :~: 'LT) -> Void -> CmpNat n m :~: 'LT
forall a b. (a -> b) -> a -> b
$ SNat (Succ n) -> (CmpNat (Succ n) 0 :~: 'LT) -> Void
forall (a :: Natural). SNat a -> (CmpNat a 0 :~: 'LT) -> Void
zeroNoLT (SNat n -> SNat (Succ n)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat n
n) CmpNat (Succ n) m :~: 'LT
CmpNat (Succ n) 0 :~: 'LT
snLTm
    IsSucc SNat n1
m' ->
      let nLTm :: CmpNat n n1 :~: 'LT
nLTm = SNat n -> SNat n1 -> CmpNat n n1 :~: CmpNat (Succ n) (n1 + 1)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat n
n SNat n1
m' (CmpNat n n1 :~: CmpNat (Succ n) m)
-> (CmpNat (Succ n) m :~: 'LT) -> CmpNat n n1 :~: 'LT
forall {k} (a :: k) (b :: k) (c :: k).
(a :~: b) -> (b :~: c) -> a :~: c
`trans` CmpNat (Succ n) m :~: 'LT
snLTm
       in SOrdering (CmpNat n m) -> CmpNat n m :~: CmpNat n m
forall {k} (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat m -> SOrdering (CmpNat n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n (SNat n1 -> SNat (n1 + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat n1
m'))
            (CmpNat n m :~: CmpNat n m)
-> Reason (:~:) (CmpNat n m) 'LT -> CmpNat n m :~: 'LT
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering 'LT
SLT SOrdering 'LT
-> (CmpNat n m :~: 'LT) -> Reason (:~:) (CmpNat n m) 'LT
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n
-> SNat n1 -> (CmpNat n n1 :~: 'LT) -> CmpNat n (n1 + 1) :~: 'LT
forall (n :: Natural) (m :: Natural).
SNat n
-> SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
cmpSuccStepR SNat n
n SNat n1
m' CmpNat n n1 :~: 'LT
nLTm

leqToLT ::
  SNat a ->
  SNat b ->
  IsTrue (Succ a <=? b) ->
  CmpNat a b :~: 'LT
leqToLT :: forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> IsTrue (S a <=? b) -> CmpNat a b :~: 'LT
leqToLT SNat a
_ SNat b
_ IsTrue (Succ a <=? b)
Witness = CmpNat a b :~: 'LT
'LT :~: 'LT
forall {k} (a :: k). a :~: a
Refl

leqZero :: SNat n -> IsTrue (0 <=? n)
leqZero :: forall (n :: Natural). SNat n -> IsTrue (0 <=? n)
leqZero SNat n
_ = IsTrue 'True
IsTrue (OrdCond (Compare 0 n) 'True 'True 'False)
Witness

leqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m)
leqSucc :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m)
leqSucc SNat n
_ SNat m
_ IsTrue (n <=? m)
Witness = IsTrue 'True
IsTrue (OrdCond (Compare (n + 1) (m + 1)) 'True 'True 'False)
Witness

fromLeqView :: LeqView n m -> IsTrue (n <=? m)
fromLeqView :: forall (n :: Natural) (m :: Natural).
LeqView n m -> IsTrue (n <=? m)
fromLeqView (LeqZero SNat m
n) = SNat m -> IsTrue (0 <=? m)
forall (n :: Natural). SNat n -> IsTrue (0 <=? n)
leqZero SNat m
n
fromLeqView (LeqSucc SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm) = SNat n
-> SNat m -> IsTrue (n <=? m) -> IsTrue ((n + 1) <=? (m + 1))
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m)
leqSucc SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm

leqViewRefl :: SNat n -> LeqView n n
leqViewRefl :: forall (n :: Natural). SNat n -> LeqView n n
leqViewRefl = LeqViewRefl n -> LeqView n n
forall (n :: Natural). LeqViewRefl n -> LeqView n n
proofLeqViewRefl (LeqViewRefl n -> LeqView n n)
-> (SNat n -> LeqViewRefl n) -> SNat n -> LeqView n n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LeqViewRefl 0
-> (forall (n :: Natural).
    SNat n -> LeqViewRefl n -> LeqViewRefl (S n))
-> SNat n
-> LeqViewRefl n
forall (p :: Natural -> Type) (k :: Natural).
p 0
-> (forall (n :: Natural). SNat n -> p n -> p (S n))
-> SNat k
-> p k
induction LeqViewRefl 0
base SNat n -> LeqViewRefl n -> LeqViewRefl (Succ n)
forall (n :: Natural). SNat n -> LeqViewRefl n -> LeqViewRefl (S n)
step
  where
    base :: LeqViewRefl 0
    base :: LeqViewRefl 0
base = LeqView 0 0 -> LeqViewRefl 0
forall (n :: Natural). LeqView n n -> LeqViewRefl n
LeqViewRefl (LeqView 0 0 -> LeqViewRefl 0) -> LeqView 0 0 -> LeqViewRefl 0
forall a b. (a -> b) -> a -> b
$ SNat 0 -> LeqView 0 0
forall (n :: Natural). SNat n -> LeqView 0 n
LeqZero SNat 0
sZero
    step :: SNat n -> LeqViewRefl n -> LeqViewRefl (Succ n)
    step :: forall (n :: Natural). SNat n -> LeqViewRefl n -> LeqViewRefl (S n)
step SNat n
n (LeqViewRefl LeqView n n
nLEQn) =
      LeqView (Succ n) (Succ n) -> LeqViewRefl (Succ n)
forall (n :: Natural). LeqView n n -> LeqViewRefl n
LeqViewRefl (LeqView (Succ n) (Succ n) -> LeqViewRefl (Succ n))
-> LeqView (Succ n) (Succ n) -> LeqViewRefl (Succ n)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat n -> IsTrue (n <=? n) -> LeqView (Succ n) (Succ n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView (n + 1) (m + 1)
LeqSucc SNat n
n SNat n
n (LeqView n n -> IsTrue (n <=? n)
forall (n :: Natural) (m :: Natural).
LeqView n m -> IsTrue (n <=? m)
fromLeqView LeqView n n
nLEQn)

viewLeq :: forall n m. SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView n m
viewLeq :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView n m
viewLeq SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm =
  case (SNat n -> ZeroOrSucc n
forall (n :: Natural). SNat n -> ZeroOrSucc n
zeroOrSucc SNat n
n, SNat n
-> SNat m
-> IsTrue (n <=? m)
-> Either (n :~: m) (CmpNat n m :~: 'LT)
forall (a :: Natural) (b :: Natural).
SNat a
-> SNat b
-> IsTrue (a <=? b)
-> Either (a :~: b) (CmpNat a b :~: 'LT)
leqToCmp SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm) of
    (ZeroOrSucc n
IsZero, Either (n :~: m) (CmpNat n m :~: 'LT)
_) -> SNat m -> LeqView 0 m
forall (n :: Natural). SNat n -> LeqView 0 n
LeqZero SNat m
m
    (ZeroOrSucc n
_, Left n :~: m
Refl) -> SNat n -> LeqView n n
forall (n :: Natural). SNat n -> LeqView n n
leqViewRefl SNat n
n
    (IsSucc SNat n1
n', Right CmpNat n m :~: 'LT
nLTm) ->
      let sm'EQm :: m :~: Succ (Pred m)
sm'EQm = SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> m :~: Succ (Pred m)
forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> b :~: Succ (Pred b)
ltRightPredSucc SNat n
n SNat m
m CmpNat n m :~: 'LT
nLTm
          m' :: SNat (Pred m)
m' = SNat m -> SNat (Pred m)
forall (n :: Natural). SNat n -> SNat (Pred n)
sPred SNat m
m
          n'LTm' :: CmpNat n1 (Pred m) :~: 'LT
n'LTm' = SNat n1
-> SNat (Pred m)
-> CmpNat n1 (Pred m) :~: CmpNat (n1 + 1) (Succ (Pred m))
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat n1
n' SNat (Pred m)
m' (CmpNat n1 (Pred m) :~: CmpNat n (Succ (Pred m)))
-> (CmpNat n (Succ (Pred m)) :~: CmpNat n m)
-> CmpNat n1 (Pred m) :~: CmpNat n m
forall {k} (a :: k) (b :: k) (c :: k).
(a :~: b) -> (b :~: c) -> a :~: c
`trans` SNat n
-> (Succ (Pred m) :~: m) -> CmpNat n (Succ (Pred m)) :~: CmpNat n m
forall (a :: Natural) (b :: Natural) (c :: Natural).
SNat a -> (b :~: c) -> CmpNat a b :~: CmpNat a c
compareCongR SNat n
n ((m :~: Succ (Pred m)) -> Succ (Pred m) :~: m
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym m :~: Succ (Pred m)
sm'EQm) (CmpNat n1 (Pred m) :~: CmpNat n m)
-> (CmpNat n m :~: 'LT) -> CmpNat n1 (Pred m) :~: 'LT
forall {k} (a :: k) (b :: k) (c :: k).
(a :~: b) -> (b :~: c) -> a :~: c
`trans` CmpNat n m :~: 'LT
nLTm
       in (Succ (Pred m) :~: m)
-> ((Succ (Pred m) ~ m) => LeqView n m) -> LeqView n m
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith ((m :~: Succ (Pred m)) -> Succ (Pred m) :~: m
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym m :~: Succ (Pred m)
sm'EQm) (((Succ (Pred m) ~ m) => LeqView n m) -> LeqView n m)
-> ((Succ (Pred m) ~ m) => LeqView n m) -> LeqView n m
forall a b. (a -> b) -> a -> b
$ SNat n1
-> SNat (Pred m)
-> IsTrue (n1 <=? Pred m)
-> LeqView (n1 + 1) (Succ (Pred m))
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView (n + 1) (m + 1)
LeqSucc SNat n1
n' SNat (Pred m)
m' (IsTrue (n1 <=? Pred m) -> LeqView (n1 + 1) (Succ (Pred m)))
-> IsTrue (n1 <=? Pred m) -> LeqView (n1 + 1) (Succ (Pred m))
forall a b. (a -> b) -> a -> b
$ SNat n1
-> SNat (Pred m)
-> (CmpNat n1 (Pred m) :~: 'LT)
-> IsTrue (n1 <=? Pred m)
forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)
ltToLeq SNat n1
n' SNat (Pred m)
m' CmpNat n1 (Pred m) :~: 'LT
n'LTm'

leqWitness :: forall n m. SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness = \SNat n
sn -> LeqWitPf n
-> forall (m :: Natural). SNat m -> IsTrue (n <=? m) -> DiffNat n m
forall (n :: Natural).
LeqWitPf n
-> forall (m :: Natural). SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitPf (LeqWitPf 0
-> (forall (n :: Natural). SNat n -> LeqWitPf n -> LeqWitPf (S n))
-> SNat n
-> LeqWitPf n
forall (p :: Natural -> Type) (k :: Natural).
p 0
-> (forall (n :: Natural). SNat n -> p n -> p (S n))
-> SNat k
-> p k
induction LeqWitPf 0
base SNat n -> LeqWitPf n -> LeqWitPf (Succ n)
forall (n :: Natural). SNat n -> LeqWitPf n -> LeqWitPf (S n)
step SNat n
sn) @m
  where
    base :: LeqWitPf 0
    base :: LeqWitPf 0
base = (forall (m :: Natural). SNat m -> IsTrue (0 <=? m) -> DiffNat 0 m)
-> LeqWitPf 0
forall (n :: Natural).
(forall (m :: Natural). SNat m -> IsTrue (n <=? m) -> DiffNat n m)
-> LeqWitPf n
LeqWitPf ((forall (m :: Natural). SNat m -> IsTrue (0 <=? m) -> DiffNat 0 m)
 -> LeqWitPf 0)
-> (forall (m :: Natural).
    SNat m -> IsTrue (0 <=? m) -> DiffNat 0 m)
-> LeqWitPf 0
forall a b. (a -> b) -> a -> b
$ \SNat m
sm IsTrue (0 <=? m)
_ -> (m :~: m) -> ((m ~ m) => DiffNat 0 m) -> DiffNat 0 m
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat m -> (0 + m) :~: m
forall (n :: Natural). SNat n -> (0 + n) :~: n
plusZeroL SNat m
sm) (((m ~ m) => DiffNat 0 m) -> DiffNat 0 m)
-> ((m ~ m) => DiffNat 0 m) -> DiffNat 0 m
forall a b. (a -> b) -> a -> b
$ SNat 0 -> SNat m -> DiffNat 0 (0 + m)
forall (n :: Natural) (n :: Natural).
SNat n -> SNat n -> DiffNat n (n + n)
DiffNat SNat 0
sZero SNat m
sm

    step :: SNat x -> LeqWitPf x -> LeqWitPf (Succ x)
    step :: forall (n :: Natural). SNat n -> LeqWitPf n -> LeqWitPf (S n)
step (SNat x
n :: SNat x) (LeqWitPf forall (m :: Natural). SNat m -> IsTrue (x <=? m) -> DiffNat x m
ih) = (forall (m :: Natural).
 SNat m -> IsTrue (Succ x <=? m) -> DiffNat (Succ x) m)
-> LeqWitPf (Succ x)
forall (n :: Natural).
(forall (m :: Natural). SNat m -> IsTrue (n <=? m) -> DiffNat n m)
-> LeqWitPf n
LeqWitPf ((forall (m :: Natural).
  SNat m -> IsTrue (Succ x <=? m) -> DiffNat (Succ x) m)
 -> LeqWitPf (Succ x))
-> (forall (m :: Natural).
    SNat m -> IsTrue (Succ x <=? m) -> DiffNat (Succ x) m)
-> LeqWitPf (Succ x)
forall a b. (a -> b) -> a -> b
$ \SNat m
m IsTrue (Succ x <=? m)
snLEQm ->
      case SNat (Succ x)
-> SNat m -> IsTrue (Succ x <=? m) -> LeqView (Succ x) m
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView n m
viewLeq (SNat x -> SNat (Succ x)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat x
n) SNat m
m IsTrue (Succ x <=? m)
snLEQm of
#if !MIN_VERSION_ghc(9,2,0) || MIN_VERSION_ghc(9,4,0)
        LeqZero SNat m
_ -> Void -> DiffNat (Succ x) m
forall a. Void -> a
absurd (Void -> DiffNat (Succ x) m) -> Void -> DiffNat (Succ x) m
forall a b. (a -> b) -> a -> b
$ SNat x -> (Succ x :~: 0) -> Void
forall (n :: Natural). SNat n -> (Succ n :~: 0) -> Void
succNonCyclic SNat x
n 0 :~: 0
Succ x :~: 0
forall {k} (a :: k). a :~: a
Refl
#endif
        LeqSucc (SNat n
_ :: SNat n') SNat m
pm IsTrue (n <=? m)
nLEQpm ->
          SNat x -> SNat m -> DiffNat x m -> DiffNat (Succ x) (m + 1)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m)
succDiffNat SNat x
n SNat m
pm (DiffNat x m -> DiffNat (Succ x) (m + 1))
-> DiffNat x m -> DiffNat (Succ x) (m + 1)
forall a b. (a -> b) -> a -> b
$ SNat m
-> IsTrue (OrdCond (Compare x m) 'True 'True 'False) -> DiffNat x m
forall (m :: Natural). SNat m -> IsTrue (x <=? m) -> DiffNat x m
ih SNat m
pm (IsTrue (OrdCond (Compare x m) 'True 'True 'False) -> DiffNat x m)
-> IsTrue (OrdCond (Compare x m) 'True 'True 'False) -> DiffNat x m
forall a b. (a -> b) -> a -> b
$ (n :~: x)
-> SNat m
-> IsTrue (n <=? m)
-> IsTrue (OrdCond (Compare x m) 'True 'True 'False)
forall (n :: Natural) (m :: Natural) (l :: Natural).
(n :~: m) -> SNat l -> IsTrue (n <=? l) -> IsTrue (m <=? l)
coerceLeqL (((n + 1) :~: Succ x) -> n :~: x
forall (n :: Natural) (m :: Natural).
(Succ n :~: Succ m) -> n :~: m
succInj (n + 1) :~: Succ x
(n + 1) :~: (n + 1)
forall {k} (a :: k). a :~: a
Refl :: n' :~: x) SNat m
pm IsTrue (n <=? m)
nLEQpm

leqStep :: forall n m l. SNat n -> SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m)
leqStep :: forall (n :: Natural) (m :: Natural) (l :: Natural).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep SNat n
_ SNat m
_ SNat l
_ (n + l) :~: m
Refl = IsTrue 'True
IsTrue (OrdCond (Compare n m) 'True 'True 'False)
Witness

leqNeqToSuccLeq :: SNat n -> SNat m -> IsTrue (n <=? m) -> (n :~: m -> Void) -> IsTrue (Succ n <=? m)
leqNeqToSuccLeq :: forall (n :: Natural) (m :: Natural).
SNat n
-> SNat m
-> IsTrue (n <=? m)
-> ((n :~: m) -> Void)
-> IsTrue (Succ n <=? m)
leqNeqToSuccLeq SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm (n :~: m) -> Void
nNEQm =
  case SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm of
    DiffNat SNat n
_ SNat m
k ->
      case SNat m -> ZeroOrSucc m
forall (n :: Natural). SNat n -> ZeroOrSucc n
zeroOrSucc SNat m
k of
        ZeroOrSucc m
IsZero -> Void -> IsTrue (Succ n <=? m)
forall a. Void -> a
absurd (Void -> IsTrue (Succ n <=? m)) -> Void -> IsTrue (Succ n <=? m)
forall a b. (a -> b) -> a -> b
$ (n :~: m) -> Void
nNEQm ((n :~: m) -> Void) -> (n :~: m) -> Void
forall a b. (a -> b) -> a -> b
$ (m :~: n) -> n :~: m
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((m :~: n) -> n :~: m) -> (m :~: n) -> n :~: m
forall a b. (a -> b) -> a -> b
$ SNat n -> (n + 0) :~: n
forall (n :: Natural). SNat n -> (n + 0) :~: n
plusZeroR SNat n
n
        IsSucc SNat n1
k' ->
          SNat (Succ n)
-> SNat m
-> SNat n1
-> ((Succ n + n1) :~: m)
-> IsTrue (Succ n <=? m)
forall (n :: Natural) (m :: Natural) (l :: Natural).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep (SNat n -> SNat (Succ n)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m SNat n1
k' (((Succ n + n1) :~: m) -> IsTrue (Succ n <=? m))
-> ((Succ n + n1) :~: m) -> IsTrue (Succ n <=? m)
forall a b. (a -> b) -> a -> b
$
            SNat (Succ n + n1) -> (Succ n + n1) :~: (Succ n + n1)
forall {k} (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat (Succ n)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat n
n SNat (Succ n) -> SNat n1 -> SNat (Succ n + n1)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat n1
k')
              ((Succ n + n1) :~: (Succ n + n1))
-> Reason (:~:) (Succ n + n1) ((n + n1) + 1)
-> (Succ n + n1) :~: ((n + n1) + 1)
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat (n + n1) -> SNat ((n + n1) + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc (SNat n
n SNat n -> SNat n1 -> SNat (n + n1)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat n1
k') SNat ((n + n1) + 1)
-> ((Succ n + n1) :~: ((n + n1) + 1))
-> Reason (:~:) (Succ n + n1) ((n + n1) + 1)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat n1 -> (Succ n + n1) :~: ((n + n1) + 1)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat n
n SNat n1
k'
              ((Succ n + n1) :~: ((n + n1) + 1))
-> Reason (:~:) ((n + n1) + 1) m -> (Succ n + n1) :~: m
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat n1 -> SNat (n1 + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat n1
k' SNat m -> (((n + n1) + 1) :~: m) -> Reason (:~:) ((n + n1) + 1) m
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (m :~: ((n + n1) + 1)) -> ((n + n1) + 1) :~: m
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat n -> SNat n1 -> (n + (n1 + 1)) :~: ((n + n1) + 1)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n + S m) :~: S (n + m)
plusSuccR SNat n
n SNat n1
k')
              ((Succ n + n1) :~: m) -> SNat m -> (Succ n + n1) :~: m
forall {k1} {k2} (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat m
m

leqRefl :: SNat n -> IsTrue (n <=? n)
leqRefl :: forall (n :: Natural). SNat n -> IsTrue (n <=? n)
leqRefl SNat n
_ = IsTrue 'True
IsTrue (OrdCond (Compare n n) 'True 'True 'False)
Witness

leqSuccStepR :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)
leqSuccStepR :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)
leqSuccStepR SNat n
_ SNat m
_ IsTrue (n <=? m)
Witness = IsTrue 'True
IsTrue (OrdCond (Compare n (m + 1)) 'True 'True 'False)
Witness

leqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m)
leqSuccStepL :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m)
leqSuccStepL SNat n
_ SNat m
_ IsTrue (Succ n <=? m)
Witness = IsTrue 'True
IsTrue (OrdCond (Compare n m) 'True 'True 'False)
Witness

leqReflexive :: SNat n -> SNat m -> n :~: m -> IsTrue (n <=? m)
leqReflexive :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive SNat n
_ SNat m
_ n :~: m
Refl = IsTrue 'True
IsTrue (OrdCond (Compare n m) 'True 'True 'False)
Witness

leqTrans :: SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue (m <=? l) -> IsTrue (n <=? l)
leqTrans :: forall (n :: Natural) (m :: Natural) (l :: Natural).
SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (m <=? l)
-> IsTrue (n <=? l)
leqTrans SNat n
_ SNat m
_ SNat l
_ IsTrue (n <=? m)
Witness IsTrue (m <=? l)
Witness = IsTrue 'True
IsTrue (OrdCond (Compare n l) 'True 'True 'False)
Witness

leqAntisymm :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m
leqAntisymm :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m
leqAntisymm SNat n
_ SNat m
_ IsTrue (n <=? m)
Witness IsTrue (m <=? n)
Witness = n :~: n
n :~: m
forall {k} (a :: k). a :~: a
Refl

plusMonotone ::
  SNat n ->
  SNat m ->
  SNat l ->
  SNat k ->
  IsTrue (n <=? m) ->
  IsTrue (l <=? k) ->
  IsTrue ((n + l) <=? (m + k))
plusMonotone :: forall (n :: Natural) (m :: Natural) (l :: Natural) (k :: Natural).
SNat n
-> SNat m
-> SNat l
-> SNat k
-> IsTrue (n <=? m)
-> IsTrue (l <=? k)
-> IsTrue ((n + l) <=? (m + k))
plusMonotone SNat n
_ SNat m
_ SNat l
_ SNat k
_ IsTrue (n <=? m)
Witness IsTrue (l <=? k)
Witness = IsTrue 'True
IsTrue (OrdCond (Compare (n + l) (m + k)) 'True 'True 'False)
Witness

leqZeroElim :: SNat n -> IsTrue (n <=? 0) -> n :~: 0
leqZeroElim :: forall (n :: Natural). SNat n -> IsTrue (n <=? 0) -> n :~: 0
leqZeroElim SNat n
_ IsTrue (n <=? 0)
Witness = n :~: n
n :~: 0
forall {k} (a :: k). a :~: a
Refl

plusMonotoneL ::
  SNat n ->
  SNat m ->
  SNat l ->
  IsTrue (n <=? m) ->
  IsTrue ((n + l) <=? (m + l))
plusMonotoneL :: forall (n :: Natural) (m :: Natural) (l :: Natural).
SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue ((n + l) <=? (m + l))
plusMonotoneL SNat n
_ SNat m
_ SNat l
_ IsTrue (n <=? m)
Witness = IsTrue 'True
IsTrue (OrdCond (Compare (n + l) (m + l)) 'True 'True 'False)
Witness

plusMonotoneR ::
  SNat n ->
  SNat m ->
  SNat l ->
  IsTrue (m <=? l) ->
  IsTrue ((n + m) <=? (n + l))
plusMonotoneR :: forall (n :: Natural) (m :: Natural) (l :: Natural).
SNat n
-> SNat m
-> SNat l
-> IsTrue (m <=? l)
-> IsTrue ((n + m) <=? (n + l))
plusMonotoneR SNat n
_ SNat m
_ SNat l
_ IsTrue (m <=? l)
Witness = IsTrue 'True
IsTrue (OrdCond (Compare (n + m) (n + l)) 'True 'True 'False)
Witness

plusLeqL :: SNat n -> SNat m -> IsTrue (n <=? (n + m))
plusLeqL :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? (n + m))
plusLeqL SNat n
_ SNat m
_  = IsTrue 'True
IsTrue (OrdCond (Compare n (n + m)) 'True 'True 'False)
Witness

plusLeqR :: SNat n -> SNat m -> IsTrue (m <=? (n + m))
plusLeqR :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? (n + m))
plusLeqR SNat n
_ SNat m
_ = IsTrue 'True
IsTrue (OrdCond (Compare m (n + m)) 'True 'True 'False)
Witness

plusCancelLeqR ::
  SNat n ->
  SNat m ->
  SNat l ->
  IsTrue ((n + l) <=? (m + l)) ->
  IsTrue (n <=? m)
plusCancelLeqR :: forall (n :: Natural) (m :: Natural) (l :: Natural).
SNat n
-> SNat m
-> SNat l
-> IsTrue ((n + l) <=? (m + l))
-> IsTrue (n <=? m)
plusCancelLeqR SNat n
_ SNat m
_ SNat l
_ IsTrue ((n + l) <=? (m + l))
Witness = IsTrue 'True
IsTrue (OrdCond (Compare n m) 'True 'True 'False)
Witness

plusCancelLeqL ::
  SNat n ->
  SNat m ->
  SNat l ->
  IsTrue ((n + m) <=? (n + l)) ->
  IsTrue (m <=? l)
plusCancelLeqL :: forall (n :: Natural) (m :: Natural) (l :: Natural).
SNat n
-> SNat m
-> SNat l
-> IsTrue ((n + m) <=? (n + l))
-> IsTrue (m <=? l)
plusCancelLeqL SNat n
_ SNat m
_ SNat l
_ IsTrue ((n + m) <=? (n + l))
Witness = IsTrue 'True
IsTrue (OrdCond (Compare m l) 'True 'True 'False)
Witness

succLeqZeroAbsurd :: SNat n -> IsTrue (S n <=? 0) -> Void
succLeqZeroAbsurd :: forall (n :: Natural). SNat n -> IsTrue (S n <=? 0) -> Void
succLeqZeroAbsurd SNat n
n IsTrue (S n <=? 0)
leq =
  SNat n -> (S n :~: 0) -> Void
forall (n :: Natural). SNat n -> (Succ n :~: 0) -> Void
succNonCyclic SNat n
n (SNat (S n) -> IsTrue (S n <=? 0) -> S n :~: 0
forall (n :: Natural). SNat n -> IsTrue (n <=? 0) -> n :~: 0
leqZeroElim (SNat n -> SNat (S n)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat n
n) IsTrue (S n <=? 0)
leq)

succLeqZeroAbsurd' :: SNat n -> (S n <=? 0) :~: 'False
succLeqZeroAbsurd' :: forall (n :: Natural). SNat n -> (S n <=? 0) :~: 'False
succLeqZeroAbsurd' SNat n
_ = 'False :~: 'False
OrdCond (Compare (n + 1) 0) 'True 'True 'False :~: 'False
forall {k} (a :: k). a :~: a
Refl

succLeqAbsurd :: SNat n -> IsTrue (S n <=? n) -> Void
succLeqAbsurd :: forall (n :: Natural). SNat n -> IsTrue (S n <=? n) -> Void
succLeqAbsurd SNat n
n IsTrue (S n <=? n)
snLEQn =
  ('LT :~: 'EQ) -> Void
forall x. ('LT :~: 'EQ) -> x
forall a x. Empty a => a -> x
eliminate (('LT :~: 'EQ) -> Void) -> ('LT :~: 'EQ) -> Void
forall a b. (a -> b) -> a -> b
$
    SOrdering 'LT -> 'LT :~: 'LT
forall {k} (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start SOrdering 'LT
SLT
      ('LT :~: 'LT) -> Reason (:~:) 'LT 'EQ -> 'LT :~: 'EQ
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n -> SNat n -> SOrdering (CmpNat n n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n SNat n
n SOrdering 'EQ -> ('LT :~: 'EQ) -> Reason (:~:) 'LT 'EQ
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` ('EQ :~: 'LT) -> 'LT :~: 'EQ
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat n -> SNat n -> IsTrue (S n <=? n) -> CmpNat n n :~: 'LT
forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> IsTrue (S a <=? b) -> CmpNat a b :~: 'LT
succLeqToLT SNat n
n SNat n
n IsTrue (S n <=? n)
snLEQn)
      ('LT :~: 'EQ) -> Reason (:~:) 'EQ 'EQ -> 'LT :~: 'EQ
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering 'EQ
SEQ SOrdering 'EQ -> ('EQ :~: 'EQ) -> Reason (:~:) 'EQ 'EQ
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat n -> (n :~: n) -> CmpNat n n :~: 'EQ
forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ
eqlCmpEQ SNat n
n SNat n
n n :~: n
forall {k} (a :: k). a :~: a
Refl

succLeqAbsurd' :: SNat n -> (S n <=? n) :~: 'False
succLeqAbsurd' :: forall (n :: Natural). SNat n -> (S n <=? n) :~: 'False
succLeqAbsurd' SNat n
_ = 'False :~: 'False
OrdCond (Compare (n + 1) n) 'True 'True 'False :~: 'False
forall {k} (a :: k). a :~: a
Refl

notLeqToLeq :: forall n m. ((n <=? m) ~ 'False) => SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq :: forall (n :: Natural) (m :: Natural).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
_ SNat m
_ = IsTrue 'True
IsTrue (OrdCond (Compare m n) 'True 'True 'False)
Witness

leqSucc' :: SNat n -> SNat m -> (n <=? m) :~: (Succ n <=? Succ m)
leqSucc' :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n <=? m) :~: (Succ n <=? Succ m)
leqSucc' SNat n
_ SNat m
_ = OrdCond (CmpNat n m) 'True 'True 'False
:~: OrdCond (CmpNat n m) 'True 'True 'False
OrdCond (Compare n m) 'True 'True 'False
:~: OrdCond (Compare (n + 1) (m + 1)) 'True 'True 'False
forall {k} (a :: k). a :~: a
Refl

leqToMin :: SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin SNat n
n SNat m
m IsTrue (n <=? m)
Witness =
  case SNat n
-> SNat m
-> IsTrue (n <=? m)
-> Either (n :~: m) (CmpNat n m :~: 'LT)
forall (a :: Natural) (b :: Natural).
SNat a
-> SNat b
-> IsTrue (a <=? b)
-> Either (a :~: b) (CmpNat a b :~: 'LT)
leqToCmp SNat n
n SNat m
m IsTrue 'True
IsTrue (n <=? m)
Witness of
    Left n :~: m
Refl -> n :~: n
Min n m :~: n
forall {k} (a :: k). a :~: a
Refl
    Right CmpNat n m :~: 'LT
Refl -> n :~: n
Min n m :~: n
forall {k} (a :: k). a :~: a
Refl

geqToMin :: SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin SNat n
n SNat m
m IsTrue (m <=? n)
Witness =
  case SNat m
-> SNat n
-> IsTrue (m <=? n)
-> Either (m :~: n) (CmpNat m n :~: 'LT)
forall (a :: Natural) (b :: Natural).
SNat a
-> SNat b
-> IsTrue (a <=? b)
-> Either (a :~: b) (CmpNat a b :~: 'LT)
leqToCmp SNat m
m SNat n
n IsTrue 'True
IsTrue (m <=? n)
Witness of
    Left m :~: n
Refl -> m :~: m
Min n m :~: m
forall {k} (a :: k). a :~: a
Refl
    Right CmpNat m n :~: 'LT
Refl -> 
      ('GT :~: CmpNat n m)
-> (('GT ~ CmpNat n m) => OrdCond (CmpNat n m) n n m :~: m)
-> OrdCond (CmpNat n m) n n m :~: m
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat m -> SNat n -> FlipOrdering (CmpNat m n) :~: CmpNat n m
forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat SNat m
m SNat n
n) m :~: m
OrdCond (CmpNat n m) n n m :~: m
('GT ~ CmpNat n m) => OrdCond (CmpNat n m) n n m :~: m
forall {k} (a :: k). a :~: a
Refl

minComm :: SNat n -> SNat m -> Min n m :~: Min m n
minComm :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> Min n m :~: Min m n
minComm SNat n
n SNat m
m =
  case SNat n
n SNat n -> SNat m -> SBool (n <=? m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
    SBool (n <=? m)
STrue ->
      SNat (OrdCond (CmpNat n m) n n m)
-> OrdCond (CmpNat n m) n n m :~: OrdCond (CmpNat n m) n n m
forall {k} (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m) (OrdCond (CmpNat n m) n n m :~: OrdCond (CmpNat n m) n n m)
-> Reason (:~:) (OrdCond (CmpNat n m) n n m) n
-> OrdCond (CmpNat n m) n n m :~: n
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n
-> (OrdCond (CmpNat n m) n n m :~: n)
-> Reason (:~:) (OrdCond (CmpNat n m) n n m) n
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin SNat n
n SNat m
m IsTrue 'True
IsTrue (n <=? m)
Witness
        (OrdCond (CmpNat n m) n n m :~: n)
-> Reason (:~:) n (OrdCond (CmpNat m n) m m n)
-> OrdCond (CmpNat n m) n n m :~: OrdCond (CmpNat m n) m m n
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m -> SNat n -> SNat (Min m n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin SNat m
m SNat n
n SNat (OrdCond (CmpNat m n) m m n)
-> (n :~: OrdCond (CmpNat m n) m m n)
-> Reason (:~:) n (OrdCond (CmpNat m n) m m n)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (OrdCond (CmpNat m n) m m n :~: n)
-> n :~: OrdCond (CmpNat m n) m m n
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat m -> SNat n -> IsTrue (n <=? m) -> Min m n :~: n
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin SNat m
m SNat n
n IsTrue 'True
IsTrue (n <=? m)
Witness)
    SBool (n <=? m)
SFalse ->
      SNat (OrdCond (CmpNat n m) n n m)
-> OrdCond (CmpNat n m) n n m :~: OrdCond (CmpNat n m) n n m
forall {k} (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m) (OrdCond (CmpNat n m) n n m :~: OrdCond (CmpNat n m) n n m)
-> Reason (:~:) (OrdCond (CmpNat n m) n n m) m
-> OrdCond (CmpNat n m) n n m :~: m
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m
m SNat m
-> (OrdCond (CmpNat n m) n n m :~: m)
-> Reason (:~:) (OrdCond (CmpNat n m) n n m) m
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin SNat n
n SNat m
m (SNat n -> SNat m -> IsTrue (m <=? n)
forall (n :: Natural) (m :: Natural).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m)
        (OrdCond (CmpNat n m) n n m :~: m)
-> Reason (:~:) m (OrdCond (CmpNat m n) m m n)
-> OrdCond (CmpNat n m) n n m :~: OrdCond (CmpNat m n) m m n
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m -> SNat n -> SNat (Min m n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin SNat m
m SNat n
n SNat (OrdCond (CmpNat m n) m m n)
-> (m :~: OrdCond (CmpNat m n) m m n)
-> Reason (:~:) m (OrdCond (CmpNat m n) m m n)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (OrdCond (CmpNat m n) m m n :~: m)
-> m :~: OrdCond (CmpNat m n) m m n
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat m -> SNat n -> IsTrue (m <=? n) -> Min m n :~: m
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin SNat m
m SNat n
n (IsTrue (m <=? n) -> Min m n :~: m)
-> IsTrue (m <=? n) -> Min m n :~: m
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (m <=? n)
forall (n :: Natural) (m :: Natural).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m)

minLeqL :: SNat n -> SNat m -> IsTrue (Min n m <=? n)
minLeqL :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (Min n m <=? n)
minLeqL SNat n
n SNat m
m =
  case SNat n
n SNat n -> SNat m -> SBool (n <=? m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
    SBool (n <=? m)
STrue -> SNat (OrdCond (CmpNat n m) n n m)
-> SNat n
-> (OrdCond (CmpNat n m) n n m :~: n)
-> IsTrue (OrdCond (CmpNat n m) n n m <=? n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m) SNat n
n ((OrdCond (CmpNat n m) n n m :~: n)
 -> IsTrue (OrdCond (CmpNat n m) n n m <=? n))
-> (OrdCond (CmpNat n m) n n m :~: n)
-> IsTrue (OrdCond (CmpNat n m) n n m <=? n)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin SNat n
n SNat m
m IsTrue 'True
IsTrue (n <=? m)
Witness
    SBool (n <=? m)
SFalse ->
      let mLEQn :: IsTrue (m <=? n)
mLEQn = SNat n -> SNat m -> IsTrue (m <=? n)
forall (n :: Natural) (m :: Natural).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m
       in SNat (OrdCond (CmpNat n m) n n m)
-> SNat m
-> SNat n
-> IsTrue (OrdCond (CmpNat n m) n n m <=? m)
-> IsTrue (m <=? n)
-> IsTrue (OrdCond (CmpNat n m) n n m <=? n)
forall (n :: Natural) (m :: Natural) (l :: Natural).
SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (m <=? l)
-> IsTrue (n <=? l)
leqTrans
            (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m)
            SNat m
m
            SNat n
n
            (SNat (OrdCond (CmpNat n m) n n m)
-> SNat m
-> (OrdCond (CmpNat n m) n n m :~: m)
-> IsTrue (OrdCond (CmpNat n m) n n m <=? m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m) SNat m
m (SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin SNat n
n SNat m
m IsTrue (m <=? n)
mLEQn))
            (IsTrue (m <=? n) -> IsTrue (OrdCond (CmpNat n m) n n m <=? n))
-> IsTrue (m <=? n) -> IsTrue (OrdCond (CmpNat n m) n n m <=? n)
forall a b. (a -> b) -> a -> b
$ IsTrue (m <=? n)
mLEQn

minLeqR :: SNat n -> SNat m -> IsTrue (Min n m <=? m)
minLeqR :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (Min n m <=? m)
minLeqR SNat n
n SNat m
m =
  SNat (OrdCond (CmpNat n m) n n m)
-> SNat (OrdCond (CmpNat m n) m m n)
-> SNat m
-> IsTrue
     (OrdCond (CmpNat n m) n n m <=? OrdCond (CmpNat m n) m m n)
-> IsTrue (OrdCond (CmpNat m n) m m n <=? m)
-> IsTrue (OrdCond (CmpNat n m) n n m <=? m)
forall (n :: Natural) (m :: Natural) (l :: Natural).
SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (m <=? l)
-> IsTrue (n <=? l)
leqTrans
    (SNat n -> SNat m -> SNat (OrdCond (Compare n m) n n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m)
    (SNat m -> SNat n -> SNat (Min m n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin SNat m
m SNat n
n)
    SNat m
m
    (SNat (OrdCond (CmpNat n m) n n m)
-> SNat (OrdCond (CmpNat m n) m m n)
-> (OrdCond (CmpNat n m) n n m :~: OrdCond (CmpNat m n) m m n)
-> IsTrue
     (OrdCond (CmpNat n m) n n m <=? OrdCond (CmpNat m n) m m n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive (SNat n -> SNat m -> SNat (OrdCond (Compare n m) n n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m) (SNat m -> SNat n -> SNat (Min m n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin SNat m
m SNat n
n) ((OrdCond (CmpNat n m) n n m :~: OrdCond (CmpNat m n) m m n)
 -> IsTrue
      (OrdCond (CmpNat n m) n n m <=? OrdCond (CmpNat m n) m m n))
-> (OrdCond (CmpNat n m) n n m :~: OrdCond (CmpNat m n) m m n)
-> IsTrue
     (OrdCond (CmpNat n m) n n m <=? OrdCond (CmpNat m n) m m n)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> OrdCond (Compare n m) n n m :~: Min m n
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> Min n m :~: Min m n
minComm SNat n
n SNat m
m)
    (SNat m -> SNat n -> IsTrue (Min m n <=? m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (Min n m <=? n)
minLeqL SNat m
m SNat n
n)

minLargest ::
  SNat l ->
  SNat n ->
  SNat m ->
  IsTrue (l <=? n) ->
  IsTrue (l <=? m) ->
  IsTrue (l <=? Min n m)
minLargest :: forall (l :: Natural) (n :: Natural) (m :: Natural).
SNat l
-> SNat n
-> SNat m
-> IsTrue (l <=? n)
-> IsTrue (l <=? m)
-> IsTrue (l <=? Min n m)
minLargest SNat l
_ SNat n
n SNat m
m IsTrue (l <=? n)
lLEQn IsTrue (l <=? m)
lLEQm =
  case SNat n -> SNat m -> Either (Min n m :~: n) (Min n m :~: m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> Either (Min n m :~: n) (Min n m :~: m)
minCase SNat n
n SNat m
m of
    Left Min n m :~: n
Refl -> IsTrue (l <=? n)
IsTrue (l <=? Min n m)
lLEQn
    Right Min n m :~: m
Refl -> IsTrue (l <=? m)
IsTrue (l <=? Min n m)
lLEQm

leqToMax :: SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax SNat n
n SNat m
m IsTrue (n <=? m)
lLeqm =
  case SNat n
-> SNat m
-> IsTrue (n <=? m)
-> Either (n :~: m) (CmpNat n m :~: 'LT)
forall (a :: Natural) (b :: Natural).
SNat a
-> SNat b
-> IsTrue (a <=? b)
-> Either (a :~: b) (CmpNat a b :~: 'LT)
leqToCmp SNat n
n SNat m
m IsTrue (n <=? m)
lLeqm of
    Left n :~: m
Refl -> m :~: m
Max n m :~: m
forall {k} (a :: k). a :~: a
Refl
    Right CmpNat n m :~: 'LT
Refl -> m :~: m
Max n m :~: m
forall {k} (a :: k). a :~: a
Refl

geqToMax :: SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax SNat n
n SNat m
m IsTrue (m <=? n)
Witness =
  case SNat n -> SNat m -> SOrdering (CmpNat n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n SNat m
m of
    SOrdering (CmpNat n m)
SLT -> n :~: n
Max n m :~: n
forall {k} (a :: k). a :~: a
Refl
    SOrdering (CmpNat n m)
SEQ -> n :~: n
Max n m :~: n
forall {k} (a :: k). a :~: a
Refl
    SOrdering (CmpNat n m)
SGT -> n :~: n
Max n m :~: n
forall {k} (a :: k). a :~: a
Refl

maxComm :: SNat n -> SNat m -> Max n m :~: Max m n
maxComm :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> Max n m :~: Max m n
maxComm SNat n
n SNat m
m =
  case SNat n
n SNat n -> SNat m -> SBool (n <=? m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
    SBool (n <=? m)
STrue ->
      SNat (OrdCond (CmpNat n m) m m n)
-> OrdCond (CmpNat n m) m m n :~: OrdCond (CmpNat n m) m m n
forall {k} (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) (OrdCond (CmpNat n m) m m n :~: OrdCond (CmpNat n m) m m n)
-> Reason (:~:) (OrdCond (CmpNat n m) m m n) m
-> OrdCond (CmpNat n m) m m n :~: m
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m
m SNat m
-> (OrdCond (CmpNat n m) m m n :~: m)
-> Reason (:~:) (OrdCond (CmpNat n m) m m n) m
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax SNat n
n SNat m
m IsTrue 'True
IsTrue (n <=? m)
Witness
        (OrdCond (CmpNat n m) m m n :~: m)
-> Reason (:~:) m (OrdCond (CmpNat m n) n n m)
-> OrdCond (CmpNat n m) m m n :~: OrdCond (CmpNat m n) n n m
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m -> SNat n -> SNat (Max m n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Max n m)
sMax SNat m
m SNat n
n SNat (OrdCond (CmpNat m n) n n m)
-> (m :~: OrdCond (CmpNat m n) n n m)
-> Reason (:~:) m (OrdCond (CmpNat m n) n n m)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (OrdCond (CmpNat m n) n n m :~: m)
-> m :~: OrdCond (CmpNat m n) n n m
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat m -> SNat n -> IsTrue (n <=? m) -> Max m n :~: m
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax SNat m
m SNat n
n IsTrue 'True
IsTrue (n <=? m)
Witness)
    SBool (n <=? m)
SFalse ->
      SNat (OrdCond (CmpNat n m) m m n)
-> OrdCond (CmpNat n m) m m n :~: OrdCond (CmpNat n m) m m n
forall {k} (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) (OrdCond (CmpNat n m) m m n :~: OrdCond (CmpNat n m) m m n)
-> Reason (:~:) (OrdCond (CmpNat n m) m m n) n
-> OrdCond (CmpNat n m) m m n :~: n
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n
-> (OrdCond (CmpNat n m) m m n :~: n)
-> Reason (:~:) (OrdCond (CmpNat n m) m m n) n
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax SNat n
n SNat m
m (SNat n -> SNat m -> IsTrue (m <=? n)
forall (n :: Natural) (m :: Natural).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m)
        (OrdCond (CmpNat n m) m m n :~: n)
-> Reason (:~:) n (OrdCond (CmpNat m n) n n m)
-> OrdCond (CmpNat n m) m m n :~: OrdCond (CmpNat m n) n n m
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m -> SNat n -> SNat (Max m n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Max n m)
sMax SNat m
m SNat n
n SNat (OrdCond (CmpNat m n) n n m)
-> (n :~: OrdCond (CmpNat m n) n n m)
-> Reason (:~:) n (OrdCond (CmpNat m n) n n m)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (OrdCond (CmpNat m n) n n m :~: n)
-> n :~: OrdCond (CmpNat m n) n n m
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat m -> SNat n -> IsTrue (m <=? n) -> Max m n :~: n
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax SNat m
m SNat n
n (IsTrue (m <=? n) -> Max m n :~: n)
-> IsTrue (m <=? n) -> Max m n :~: n
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (m <=? n)
forall (n :: Natural) (m :: Natural).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m)

maxLeqR :: SNat n -> SNat m -> IsTrue (m <=? Max n m)
maxLeqR :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? Max n m)
maxLeqR SNat n
n SNat m
m =
  case SNat n
n SNat n -> SNat m -> SBool (n <=? m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
    SBool (n <=? m)
STrue -> SNat m
-> SNat (OrdCond (CmpNat n m) m m n)
-> (m :~: OrdCond (CmpNat n m) m m n)
-> IsTrue (m <=? OrdCond (CmpNat n m) m m n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive SNat m
m (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) ((m :~: OrdCond (CmpNat n m) m m n)
 -> IsTrue (m <=? OrdCond (CmpNat n m) m m n))
-> (m :~: OrdCond (CmpNat n m) m m n)
-> IsTrue (m <=? OrdCond (CmpNat n m) m m n)
forall a b. (a -> b) -> a -> b
$ (OrdCond (CmpNat n m) m m n :~: m)
-> m :~: OrdCond (CmpNat n m) m m n
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((OrdCond (CmpNat n m) m m n :~: m)
 -> m :~: OrdCond (CmpNat n m) m m n)
-> (OrdCond (CmpNat n m) m m n :~: m)
-> m :~: OrdCond (CmpNat n m) m m n
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax SNat n
n SNat m
m IsTrue 'True
IsTrue (n <=? m)
Witness
    SBool (n <=? m)
SFalse ->
      let mLEQn :: IsTrue (m <=? n)
mLEQn = SNat n -> SNat m -> IsTrue (m <=? n)
forall (n :: Natural) (m :: Natural).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m
       in SNat m
-> SNat n
-> SNat (OrdCond (CmpNat n m) m m n)
-> IsTrue (m <=? n)
-> IsTrue (n <=? OrdCond (CmpNat n m) m m n)
-> IsTrue (m <=? OrdCond (CmpNat n m) m m n)
forall (n :: Natural) (m :: Natural) (l :: Natural).
SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (m <=? l)
-> IsTrue (n <=? l)
leqTrans
            SNat m
m
            SNat n
n
            (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m)
            IsTrue (m <=? n)
mLEQn
            (SNat n
-> SNat (OrdCond (CmpNat n m) m m n)
-> (n :~: OrdCond (CmpNat n m) m m n)
-> IsTrue (n <=? OrdCond (CmpNat n m) m m n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive SNat n
n (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) ((OrdCond (CmpNat n m) m m n :~: n)
-> n :~: OrdCond (CmpNat n m) m m n
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((OrdCond (CmpNat n m) m m n :~: n)
 -> n :~: OrdCond (CmpNat n m) m m n)
-> (OrdCond (CmpNat n m) m m n :~: n)
-> n :~: OrdCond (CmpNat n m) m m n
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax SNat n
n SNat m
m IsTrue (m <=? n)
mLEQn))

maxLeqL :: SNat n -> SNat m -> IsTrue (n <=? Max n m)
maxLeqL :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? Max n m)
maxLeqL SNat n
n SNat m
m =
  SNat n
-> SNat (OrdCond (CmpNat m n) n n m)
-> SNat (OrdCond (CmpNat n m) m m n)
-> IsTrue (n <=? OrdCond (CmpNat m n) n n m)
-> IsTrue
     (OrdCond (CmpNat m n) n n m <=? OrdCond (CmpNat n m) m m n)
-> IsTrue (n <=? OrdCond (CmpNat n m) m m n)
forall (n :: Natural) (m :: Natural) (l :: Natural).
SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (m <=? l)
-> IsTrue (n <=? l)
leqTrans
    SNat n
n
    (SNat m -> SNat n -> SNat (Max m n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Max n m)
sMax SNat m
m SNat n
n)
    (SNat n -> SNat m -> SNat (OrdCond (Compare n m) m m n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m)
    (SNat m -> SNat n -> IsTrue (n <=? Max m n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? Max n m)
maxLeqR SNat m
m SNat n
n)
    (SNat (OrdCond (CmpNat m n) n n m)
-> SNat (OrdCond (CmpNat n m) m m n)
-> (OrdCond (CmpNat m n) n n m :~: OrdCond (CmpNat n m) m m n)
-> IsTrue
     (OrdCond (CmpNat m n) n n m <=? OrdCond (CmpNat n m) m m n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive (SNat m -> SNat n -> SNat (Max m n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Max n m)
sMax SNat m
m SNat n
n) (SNat n -> SNat m -> SNat (OrdCond (Compare n m) m m n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) ((OrdCond (CmpNat m n) n n m :~: OrdCond (CmpNat n m) m m n)
 -> IsTrue
      (OrdCond (CmpNat m n) n n m <=? OrdCond (CmpNat n m) m m n))
-> (OrdCond (CmpNat m n) n n m :~: OrdCond (CmpNat n m) m m n)
-> IsTrue
     (OrdCond (CmpNat m n) n n m <=? OrdCond (CmpNat n m) m m n)
forall a b. (a -> b) -> a -> b
$ SNat m -> SNat n -> Max m n :~: OrdCond (Compare n m) m m n
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> Max n m :~: Max m n
maxComm SNat m
m SNat n
n)

maxLeast ::
  SNat l ->
  SNat n ->
  SNat m ->
  IsTrue (n <=? l) ->
  IsTrue (m <=? l) ->
  IsTrue (Max n m <=? l)
maxLeast :: forall (l :: Natural) (n :: Natural) (m :: Natural).
SNat l
-> SNat n
-> SNat m
-> IsTrue (n <=? l)
-> IsTrue (m <=? l)
-> IsTrue (Max n m <=? l)
maxLeast SNat l
_ SNat n
n SNat m
m IsTrue (n <=? l)
nLEQl IsTrue (m <=? l)
mLEQl =
  case SNat n -> SNat m -> Either (Max n m :~: m) (Max n m :~: n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> Either (Max n m :~: m) (Max n m :~: n)
maxCase SNat n
n SNat m
m of
    Left Max n m :~: m
Refl -> IsTrue (m <=? l)
IsTrue (Max n m <=? l)
mLEQl
    Right Max n m :~: n
Refl -> IsTrue (n <=? l)
IsTrue (Max n m <=? l)
nLEQl


-- | Since 1.2.0.0 (type changed)
lneqSuccLeq :: SNat n -> SNat m -> (n <? m) :~: (Succ n <=? m)
#if MIN_VERSION_ghc(9,2,1)
lneqSuccLeq :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n <? m) :~: (Succ n <=? m)
lneqSuccLeq SNat n
_ SNat m
_ = OrdCond (CmpNat n m) 'True 'False 'False
:~: OrdCond (CmpNat n m) 'True 'False 'False
OrdCond (Compare n m) 'True 'False 'False
:~: OrdCond (Compare (n + 1) m) 'True 'True 'False
forall {k} (a :: k). a :~: a
Refl
#else
lneqSuccLeq n m = isTrueRefl (n %<? m) (Succ n %<=? m)
  (ltToSuccLeq n m . lneqToLT n m)
  (ltToLneq n m . succLeqToLT n m)

isTrueRefl :: SBool a -> SBool b 
  -> (IsTrue a -> IsTrue b)
  -> (IsTrue b -> IsTrue a)
  -> a :~: b
isTrueRefl SFalse SFalse _ _ = Refl
isTrueRefl STrue _ f _ = withWitness (f Witness) Refl
isTrueRefl _ STrue _ g = withWitness (g Witness) Refl
#endif

-- | Since 1.2.0.0 (type changed)
lneqReversed :: SNat n -> SNat m -> (n <? m) :~: (m >? n)
#if MIN_VERSION_ghc(9,2,1)
lneqReversed :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n <? m) :~: (m >? n)
lneqReversed SNat n
_ SNat m
_ = OrdCond (CmpNat n m) 'True 'False 'False
:~: OrdCond (CmpNat n m) 'True 'False 'False
OrdCond (Compare n m) 'True 'False 'False
:~: OrdCond (Compare m n) 'False 'False 'True
forall {k} (a :: k). a :~: a
Refl
#else
lneqReversed n m = 
  case sCmpNat n m of
    SLT -> gcastWith (flipCmpNat n m) Refl
    SEQ -> gcastWith (flipCmpNat n m) Refl
    SGT -> gcastWith (flipCmpNat n m) Refl
#endif

lneqToLT ::
  SNat n ->
  SNat m ->
  IsTrue (n <? m) ->
  CmpNat n m :~: 'LT
lneqToLT :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <? m) -> CmpNat n m :~: 'LT
lneqToLT SNat n
n SNat m
m IsTrue (n <? m)
Witness =
  case SNat n -> SNat m -> SOrdering (CmpNat n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n SNat m
m of
    SOrdering (CmpNat n m)
SLT -> CmpNat n m :~: 'LT
'LT :~: 'LT
forall {k} (a :: k). a :~: a
Refl

ltToLneq ::
  SNat n ->
  SNat m ->
  CmpNat n m :~: 'LT ->
  IsTrue (n <? m)
ltToLneq :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> IsTrue (n <? m)
ltToLneq SNat n
_ SNat m
_ CmpNat n m :~: 'LT
Refl = IsTrue 'True
IsTrue (OrdCond (Compare n m) 'True 'False 'False)
Witness

lneqZero :: SNat a -> IsTrue (0 <? Succ a)
lneqZero :: forall (a :: Natural). SNat a -> IsTrue (0 <? Succ a)
lneqZero SNat a
n = SNat 0
-> SNat (a + 1)
-> (CmpNat 0 (a + 1) :~: 'LT)
-> IsTrue (OrdCond (Compare 0 (a + 1)) 'True 'False 'False)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> IsTrue (n <? m)
ltToLneq SNat 0
sZero (SNat a -> SNat (a + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat a
n) ((CmpNat 0 (a + 1) :~: 'LT)
 -> IsTrue (OrdCond (Compare 0 (a + 1)) 'True 'False 'False))
-> (CmpNat 0 (a + 1) :~: 'LT)
-> IsTrue (OrdCond (Compare 0 (a + 1)) 'True 'False 'False)
forall a b. (a -> b) -> a -> b
$ SNat a -> CmpNat 0 (a + 1) :~: 'LT
forall (a :: Natural). SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero SNat a
n

lneqSucc :: SNat n -> IsTrue (n <? Succ n)
lneqSucc :: forall (n :: Natural). SNat n -> IsTrue (n <? Succ n)
lneqSucc SNat n
n = SNat n
-> SNat (n + 1)
-> (CmpNat n (n + 1) :~: 'LT)
-> IsTrue (OrdCond (Compare n (n + 1)) 'True 'False 'False)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> IsTrue (n <? m)
ltToLneq SNat n
n (SNat n -> SNat (n + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat n
n) ((CmpNat n (n + 1) :~: 'LT)
 -> IsTrue (OrdCond (Compare n (n + 1)) 'True 'False 'False))
-> (CmpNat n (n + 1) :~: 'LT)
-> IsTrue (OrdCond (Compare n (n + 1)) 'True 'False 'False)
forall a b. (a -> b) -> a -> b
$ SNat n -> CmpNat n (n + 1) :~: 'LT
forall (a :: Natural). SNat a -> CmpNat a (Succ a) :~: 'LT
ltSucc SNat n
n

succLneqSucc ::
  SNat n ->
  SNat m ->
  (n <? m) :~: (Succ n <? Succ m)
succLneqSucc :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n <? m) :~: (Succ n <? Succ m)
succLneqSucc SNat n
n SNat m
m = 
  SBool (OrdCond (CmpNat n m) 'True 'False 'False)
-> OrdCond (CmpNat n m) 'True 'False 'False
   :~: OrdCond (CmpNat n m) 'True 'False 'False
forall {k} (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n
n SNat n
-> SNat m -> SBool (OrdCond (Compare n m) 'True 'False 'False)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SBool (n <? m)
%<? SNat m
m)
  (OrdCond (CmpNat n m) 'True 'False 'False
 :~: OrdCond (CmpNat n m) 'True 'False 'False)
-> SBool (OrdCond (CmpNat n m) 'True 'False 'False)
-> OrdCond (CmpNat n m) 'True 'False 'False
   :~: OrdCond (CmpNat n m) 'True 'False 'False
forall {k1} {k2} (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~=
  SOrdering (CmpNat n m)
-> SBool 'True
-> SBool 'False
-> SBool 'False
-> SBool (OrdCond (CmpNat n m) 'True 'False 'False)
forall {k} (o :: Ordering) (f :: k -> Type) (lt :: k) (eq :: k)
       (gt :: k).
SOrdering o -> f lt -> f eq -> f gt -> f (OrdCond o lt eq gt)
sOrdCond (SNat n -> SNat m -> SOrdering (CmpNat n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n SNat m
m)  SBool 'True
STrue SBool 'False
SFalse SBool 'False
SFalse
  (OrdCond (CmpNat n m) 'True 'False 'False
 :~: OrdCond (CmpNat n m) 'True 'False 'False)
-> Reason
     (:~:)
     (OrdCond (CmpNat n m) 'True 'False 'False)
     (OrdCond (CmpNat (n + 1) (m + 1)) 'True 'False 'False)
-> OrdCond (CmpNat n m) 'True 'False 'False
   :~: OrdCond (CmpNat (n + 1) (m + 1)) 'True 'False 'False
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SOrdering (CmpNat (n + 1) (m + 1))
-> SBool 'True
-> SBool 'False
-> SBool 'False
-> SBool (OrdCond (CmpNat (n + 1) (m + 1)) 'True 'False 'False)
forall {k} (o :: Ordering) (f :: k -> Type) (lt :: k) (eq :: k)
       (gt :: k).
SOrdering o -> f lt -> f eq -> f gt -> f (OrdCond o lt eq gt)
sOrdCond (SNat (n + 1) -> SNat (m + 1) -> SOrdering (CmpNat (n + 1) (m + 1))
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat (SNat n -> SNat (n + 1)
forall (n :: Natural) (n1 :: Natural).
(n ~ Succ n1) =>
SNat n1 -> SNat n
Succ SNat n
n) (SNat m -> SNat (m + 1)
forall (n :: Natural) (n1 :: Natural).
(n ~ Succ n1) =>
SNat n1 -> SNat n
Succ SNat m
m)) SBool 'True
STrue SBool 'False
SFalse SBool 'False
SFalse 
    SBool (OrdCond (CmpNat (n + 1) (m + 1)) 'True 'False 'False)
-> (OrdCond (CmpNat n m) 'True 'False 'False
    :~: OrdCond (CmpNat (n + 1) (m + 1)) 'True 'False 'False)
-> Reason
     (:~:)
     (OrdCond (CmpNat n m) 'True 'False 'False)
     (OrdCond (CmpNat (n + 1) (m + 1)) 'True 'False 'False)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (CmpNat n m :~: CmpNat (n + 1) (m + 1))
-> SBool 'True
-> SBool 'False
-> SBool 'False
-> OrdCond (CmpNat n m) 'True 'False 'False
   :~: OrdCond (CmpNat (n + 1) (m + 1)) 'True 'False 'False
forall {k} (o :: Ordering) (o' :: Ordering) (proxy :: k -> Type)
       (a :: k) (proxy' :: k -> Type) (b :: k) (c :: k).
(o :~: o')
-> proxy a
-> proxy' b
-> proxy' c
-> OrdCond o a b c :~: OrdCond o' a b c
sOrdCondCong1 (SNat n -> SNat m -> CmpNat n m :~: CmpNat (n + 1) (m + 1)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat n
n SNat m
m) SBool 'True
STrue SBool 'False
SFalse SBool 'False
SFalse
  (OrdCond (CmpNat n m) 'True 'False 'False
 :~: OrdCond (CmpNat (n + 1) (m + 1)) 'True 'False 'False)
-> SBool (OrdCond (CmpNat (n + 1) (m + 1)) 'True 'False 'False)
-> OrdCond (CmpNat n m) 'True 'False 'False
   :~: OrdCond (CmpNat (n + 1) (m + 1)) 'True 'False 'False
forall {k1} {k2} (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= (SNat n -> SNat (n + 1)
forall (n :: Natural) (n1 :: Natural).
(n ~ Succ n1) =>
SNat n1 -> SNat n
Succ SNat n
n SNat (n + 1)
-> SNat (m + 1)
-> SBool (OrdCond (Compare (n + 1) (m + 1)) 'True 'False 'False)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SBool (n <? m)
%<? SNat m -> SNat (m + 1)
forall (n :: Natural) (n1 :: Natural).
(n ~ Succ n1) =>
SNat n1 -> SNat n
Succ SNat m
m)

sOrdCondCong1 :: o :~: o' -> proxy a -> proxy' b -> proxy' c 
  -> OrdCond o a b c :~: OrdCond o' a b c
sOrdCondCong1 :: forall {k} (o :: Ordering) (o' :: Ordering) (proxy :: k -> Type)
       (a :: k) (proxy' :: k -> Type) (b :: k) (c :: k).
(o :~: o')
-> proxy a
-> proxy' b
-> proxy' c
-> OrdCond o a b c :~: OrdCond o' a b c
sOrdCondCong1 o :~: o'
Refl proxy a
_ proxy' b
_ proxy' c
_ = OrdCond o a b c :~: OrdCond o a b c
OrdCond o a b c :~: OrdCond o' a b c
forall {k} (a :: k). a :~: a
Refl

lneqRightPredSucc ::
  SNat n ->
  SNat m ->
  IsTrue (n <? m) ->
  m :~: Succ (Pred m)
lneqRightPredSucc :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <? m) -> m :~: Succ (Pred m)
lneqRightPredSucc SNat n
n SNat m
m IsTrue (n <? m)
nLNEQm = SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> m :~: (Pred m + 1)
forall (a :: Natural) (b :: Natural).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> b :~: Succ (Pred b)
ltRightPredSucc SNat n
n SNat m
m ((CmpNat n m :~: 'LT) -> m :~: (Pred m + 1))
-> (CmpNat n m :~: 'LT) -> m :~: (Pred m + 1)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (n <? m) -> CmpNat n m :~: 'LT
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <? m) -> CmpNat n m :~: 'LT
lneqToLT SNat n
n SNat m
m IsTrue (n <? m)
nLNEQm

lneqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <? m) -> IsTrue (n <? m)
lneqSuccStepL :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (Succ n <? m) -> IsTrue (n <? m)
lneqSuccStepL SNat n
n SNat m
m IsTrue (Succ n <? m)
snLNEQm =
  (OrdCond (CmpNat (Succ n) m) 'True 'True 'False
 :~: OrdCond (CmpNat n m) 'True 'False 'False)
-> ((OrdCond (CmpNat (Succ n) m) 'True 'True 'False
     ~ OrdCond (CmpNat n m) 'True 'False 'False) =>
    IsTrue (n <? m))
-> IsTrue (n <? m)
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith ((OrdCond (CmpNat n m) 'True 'False 'False
 :~: OrdCond (CmpNat (Succ n) m) 'True 'True 'False)
-> OrdCond (CmpNat (Succ n) m) 'True 'True 'False
   :~: OrdCond (CmpNat n m) 'True 'False 'False
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((OrdCond (CmpNat n m) 'True 'False 'False
  :~: OrdCond (CmpNat (Succ n) m) 'True 'True 'False)
 -> OrdCond (CmpNat (Succ n) m) 'True 'True 'False
    :~: OrdCond (CmpNat n m) 'True 'False 'False)
-> (OrdCond (CmpNat n m) 'True 'False 'False
    :~: OrdCond (CmpNat (Succ n) m) 'True 'True 'False)
-> OrdCond (CmpNat (Succ n) m) 'True 'True 'False
   :~: OrdCond (CmpNat n m) 'True 'False 'False
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> (n <? m) :~: (Succ n <=? m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n <? m) :~: (Succ n <=? m)
lneqSuccLeq SNat n
n SNat m
m) (((OrdCond (CmpNat (Succ n) m) 'True 'True 'False
   ~ OrdCond (CmpNat n m) 'True 'False 'False) =>
  IsTrue (n <? m))
 -> IsTrue (n <? m))
-> ((OrdCond (CmpNat (Succ n) m) 'True 'True 'False
     ~ OrdCond (CmpNat n m) 'True 'False 'False) =>
    IsTrue (n <? m))
-> IsTrue (n <? m)
forall a b. (a -> b) -> a -> b
$
    SNat (Succ n)
-> SNat m -> IsTrue (Succ (Succ n) <=? m) -> IsTrue (Succ n <=? m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m)
leqSuccStepL (SNat n -> SNat (Succ n)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m (IsTrue (Succ (Succ n) <=? m) -> IsTrue (Succ n <=? m))
-> IsTrue (Succ (Succ n) <=? m) -> IsTrue (Succ n <=? m)
forall a b. (a -> b) -> a -> b
$
      (OrdCond (CmpNat (Succ n) m) 'True 'False 'False
 :~: OrdCond (CmpNat (Succ (Succ n)) m) 'True 'True 'False)
-> ((OrdCond (CmpNat (Succ n) m) 'True 'False 'False
     ~ OrdCond (CmpNat (Succ (Succ n)) m) 'True 'True 'False) =>
    IsTrue (OrdCond (CmpNat (Succ (Succ n)) m) 'True 'True 'False))
-> IsTrue (OrdCond (CmpNat (Succ (Succ n)) m) 'True 'True 'False)
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat (Succ n) -> SNat m -> (Succ n <? m) :~: (Succ (Succ n) <=? m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n <? m) :~: (Succ n <=? m)
lneqSuccLeq (SNat n -> SNat (Succ n)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m) IsTrue (OrdCond (CmpNat (Succ (Succ n)) m) 'True 'True 'False)
IsTrue (Succ n <? m)
(OrdCond (CmpNat (Succ n) m) 'True 'False 'False
 ~ OrdCond (CmpNat (Succ (Succ n)) m) 'True 'True 'False) =>
IsTrue (OrdCond (CmpNat (Succ (Succ n)) m) 'True 'True 'False)
snLNEQm

lneqSuccStepR :: SNat n -> SNat m -> IsTrue (n <? m) -> IsTrue (n <? Succ m)
lneqSuccStepR :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <? m) -> IsTrue (n <? Succ m)
lneqSuccStepR SNat n
n SNat m
m IsTrue (n <? m)
nLNEQm =
  (OrdCond (CmpNat (n + 1) (m + 1)) 'True 'True 'False
 :~: OrdCond (CmpNat n (m + 1)) 'True 'False 'False)
-> ((OrdCond (CmpNat (n + 1) (m + 1)) 'True 'True 'False
     ~ OrdCond (CmpNat n (m + 1)) 'True 'False 'False) =>
    IsTrue (n <? (m + 1)))
-> IsTrue (n <? (m + 1))
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith ((OrdCond (CmpNat n (m + 1)) 'True 'False 'False
 :~: OrdCond (CmpNat (n + 1) (m + 1)) 'True 'True 'False)
-> OrdCond (CmpNat (n + 1) (m + 1)) 'True 'True 'False
   :~: OrdCond (CmpNat n (m + 1)) 'True 'False 'False
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((OrdCond (CmpNat n (m + 1)) 'True 'False 'False
  :~: OrdCond (CmpNat (n + 1) (m + 1)) 'True 'True 'False)
 -> OrdCond (CmpNat (n + 1) (m + 1)) 'True 'True 'False
    :~: OrdCond (CmpNat n (m + 1)) 'True 'False 'False)
-> (OrdCond (CmpNat n (m + 1)) 'True 'False 'False
    :~: OrdCond (CmpNat (n + 1) (m + 1)) 'True 'True 'False)
-> OrdCond (CmpNat (n + 1) (m + 1)) 'True 'True 'False
   :~: OrdCond (CmpNat n (m + 1)) 'True 'False 'False
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat (m + 1) -> (n <? (m + 1)) :~: ((n + 1) <=? (m + 1))
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n <? m) :~: (Succ n <=? m)
lneqSuccLeq SNat n
n (SNat m -> SNat (m + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat m
m)) (((OrdCond (CmpNat (n + 1) (m + 1)) 'True 'True 'False
   ~ OrdCond (CmpNat n (m + 1)) 'True 'False 'False) =>
  IsTrue (n <? (m + 1)))
 -> IsTrue (n <? (m + 1)))
-> ((OrdCond (CmpNat (n + 1) (m + 1)) 'True 'True 'False
     ~ OrdCond (CmpNat n (m + 1)) 'True 'False 'False) =>
    IsTrue (n <? (m + 1)))
-> IsTrue (n <? (m + 1))
forall a b. (a -> b) -> a -> b
$
    SNat (n + 1)
-> SNat m -> IsTrue ((n + 1) <=? m) -> IsTrue ((n + 1) <=? (m + 1))
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)
leqSuccStepR (SNat n -> SNat (n + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m (IsTrue ((n + 1) <=? m) -> IsTrue ((n + 1) <=? (m + 1)))
-> IsTrue ((n + 1) <=? m) -> IsTrue ((n + 1) <=? (m + 1))
forall a b. (a -> b) -> a -> b
$
      (OrdCond (CmpNat n m) 'True 'False 'False
 :~: OrdCond (CmpNat (n + 1) m) 'True 'True 'False)
-> ((OrdCond (CmpNat n m) 'True 'False 'False
     ~ OrdCond (CmpNat (n + 1) m) 'True 'True 'False) =>
    IsTrue (OrdCond (CmpNat (n + 1) m) 'True 'True 'False))
-> IsTrue (OrdCond (CmpNat (n + 1) m) 'True 'True 'False)
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n -> SNat m -> (n <? m) :~: ((n + 1) <=? m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n <? m) :~: (Succ n <=? m)
lneqSuccLeq SNat n
n SNat m
m) IsTrue (OrdCond (CmpNat (n + 1) m) 'True 'True 'False)
IsTrue (n <? m)
(OrdCond (CmpNat n m) 'True 'False 'False
 ~ OrdCond (CmpNat (n + 1) m) 'True 'True 'False) =>
IsTrue (OrdCond (CmpNat (n + 1) m) 'True 'True 'False)
nLNEQm

plusStrictMonotone ::
  SNat n ->
  SNat m ->
  SNat l ->
  SNat k ->
  IsTrue (n <? m) ->
  IsTrue (l <? k) ->
  IsTrue ((n + l) <? (m + k))
plusStrictMonotone :: forall (n :: Natural) (m :: Natural) (l :: Natural) (k :: Natural).
SNat n
-> SNat m
-> SNat l
-> SNat k
-> IsTrue (n <? m)
-> IsTrue (l <? k)
-> IsTrue ((n + l) <? (m + k))
plusStrictMonotone SNat n
n SNat m
m SNat l
l SNat k
k IsTrue (n <? m)
nLNm IsTrue (l <? k)
lLNk =
  (OrdCond (CmpNat ((n + l) + 1) (m + k)) 'True 'True 'False
 :~: OrdCond (CmpNat (n + l) (m + k)) 'True 'False 'False)
-> ((OrdCond (CmpNat ((n + l) + 1) (m + k)) 'True 'True 'False
     ~ OrdCond (CmpNat (n + l) (m + k)) 'True 'False 'False) =>
    IsTrue ((n + l) <? (m + k)))
-> IsTrue ((n + l) <? (m + k))
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith ((OrdCond (CmpNat (n + l) (m + k)) 'True 'False 'False
 :~: OrdCond (CmpNat ((n + l) + 1) (m + k)) 'True 'True 'False)
-> OrdCond (CmpNat ((n + l) + 1) (m + k)) 'True 'True 'False
   :~: OrdCond (CmpNat (n + l) (m + k)) 'True 'False 'False
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((OrdCond (CmpNat (n + l) (m + k)) 'True 'False 'False
  :~: OrdCond (CmpNat ((n + l) + 1) (m + k)) 'True 'True 'False)
 -> OrdCond (CmpNat ((n + l) + 1) (m + k)) 'True 'True 'False
    :~: OrdCond (CmpNat (n + l) (m + k)) 'True 'False 'False)
-> (OrdCond (CmpNat (n + l) (m + k)) 'True 'False 'False
    :~: OrdCond (CmpNat ((n + l) + 1) (m + k)) 'True 'True 'False)
-> OrdCond (CmpNat ((n + l) + 1) (m + k)) 'True 'True 'False
   :~: OrdCond (CmpNat (n + l) (m + k)) 'True 'False 'False
forall a b. (a -> b) -> a -> b
$ SNat (n + l)
-> SNat (m + k)
-> ((n + l) <? (m + k)) :~: (((n + l) + 1) <=? (m + k))
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n <? m) :~: (Succ n <=? m)
lneqSuccLeq (SNat n
n SNat n -> SNat l -> SNat (n + l)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l) (SNat m
m SNat m -> SNat k -> SNat (m + k)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat k
k)) (((OrdCond (CmpNat ((n + l) + 1) (m + k)) 'True 'True 'False
   ~ OrdCond (CmpNat (n + l) (m + k)) 'True 'False 'False) =>
  IsTrue ((n + l) <? (m + k)))
 -> IsTrue ((n + l) <? (m + k)))
-> ((OrdCond (CmpNat ((n + l) + 1) (m + k)) 'True 'True 'False
     ~ OrdCond (CmpNat (n + l) (m + k)) 'True 'False 'False) =>
    IsTrue ((n + l) <? (m + k)))
-> IsTrue ((n + l) <? (m + k))
forall a b. (a -> b) -> a -> b
$
    ((((n + 1) + l) :~: ((n + l) + 1))
 -> SNat (m + k)
 -> IsTrue
      (OrdCond (CmpNat ((n + 1) + l) (m + k)) 'True 'True 'False)
 -> IsTrue ((n + l) <? (m + k)))
-> SNat (m + k)
-> (((n + 1) + l) :~: ((n + l) + 1))
-> IsTrue
     (OrdCond (CmpNat ((n + 1) + l) (m + k)) 'True 'True 'False)
-> IsTrue ((n + l) <? (m + k))
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((n + 1) + l) :~: ((n + l) + 1))
-> SNat (m + k)
-> IsTrue
     (OrdCond (CmpNat ((n + 1) + l) (m + k)) 'True 'True 'False)
-> IsTrue ((n + l) <? (m + k))
(((n + 1) + l) :~: ((n + l) + 1))
-> SNat (m + k)
-> IsTrue (((n + 1) + l) <=? (m + k))
-> IsTrue (((n + l) + 1) <=? (m + k))
forall (n :: Natural) (m :: Natural) (l :: Natural).
(n :~: m) -> SNat l -> IsTrue (n <=? l) -> IsTrue (m <=? l)
coerceLeqL (SNat m
m SNat m -> SNat k -> SNat (m + k)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat k
k) (SNat n -> SNat l -> ((n + 1) + l) :~: ((n + l) + 1)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat n
n SNat l
l) (IsTrue (OrdCond (CmpNat ((n + 1) + l) (m + k)) 'True 'True 'False)
 -> IsTrue ((n + l) <? (m + k)))
-> IsTrue
     (OrdCond (CmpNat ((n + 1) + l) (m + k)) 'True 'True 'False)
-> IsTrue ((n + l) <? (m + k))
forall a b. (a -> b) -> a -> b
$
      SNat (n + 1)
-> SNat m
-> SNat l
-> SNat k
-> IsTrue ((n + 1) <=? m)
-> IsTrue (l <=? k)
-> IsTrue (((n + 1) + l) <=? (m + k))
forall (n :: Natural) (m :: Natural) (l :: Natural) (k :: Natural).
SNat n
-> SNat m
-> SNat l
-> SNat k
-> IsTrue (n <=? m)
-> IsTrue (l <=? k)
-> IsTrue ((n + l) <=? (m + k))
plusMonotone
        (SNat n -> SNat (n + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat n
n)
        SNat m
m
        SNat l
l
        SNat k
k
        ((OrdCond (CmpNat n m) 'True 'False 'False
 :~: OrdCond (CmpNat (n + 1) m) 'True 'True 'False)
-> ((OrdCond (CmpNat n m) 'True 'False 'False
     ~ OrdCond (CmpNat (n + 1) m) 'True 'True 'False) =>
    IsTrue (OrdCond (CmpNat (n + 1) m) 'True 'True 'False))
-> IsTrue (OrdCond (CmpNat (n + 1) m) 'True 'True 'False)
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n -> SNat m -> (n <? m) :~: ((n + 1) <=? m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n <? m) :~: (Succ n <=? m)
lneqSuccLeq SNat n
n SNat m
m) IsTrue (OrdCond (CmpNat (n + 1) m) 'True 'True 'False)
IsTrue (n <? m)
(OrdCond (CmpNat n m) 'True 'False 'False
 ~ OrdCond (CmpNat (n + 1) m) 'True 'True 'False) =>
IsTrue (OrdCond (CmpNat (n + 1) m) 'True 'True 'False)
nLNm)
        ( SNat l
-> SNat (l + 1)
-> SNat k
-> IsTrue (l <=? (l + 1))
-> IsTrue ((l + 1) <=? k)
-> IsTrue (l <=? k)
forall (n :: Natural) (m :: Natural) (l :: Natural).
SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (m <=? l)
-> IsTrue (n <=? l)
leqTrans SNat l
l (SNat l -> SNat (l + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat l
l) SNat k
k (SNat l -> SNat l -> IsTrue (l <=? l) -> IsTrue (l <=? (l + 1))
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)
leqSuccStepR SNat l
l SNat l
l (SNat l -> IsTrue (l <=? l)
forall (n :: Natural). SNat n -> IsTrue (n <=? n)
leqRefl SNat l
l)) (IsTrue ((l + 1) <=? k) -> IsTrue (l <=? k))
-> IsTrue ((l + 1) <=? k) -> IsTrue (l <=? k)
forall a b. (a -> b) -> a -> b
$
            (OrdCond (CmpNat l k) 'True 'False 'False
 :~: OrdCond (CmpNat (l + 1) k) 'True 'True 'False)
-> ((OrdCond (CmpNat l k) 'True 'False 'False
     ~ OrdCond (CmpNat (l + 1) k) 'True 'True 'False) =>
    IsTrue (OrdCond (CmpNat (l + 1) k) 'True 'True 'False))
-> IsTrue (OrdCond (CmpNat (l + 1) k) 'True 'True 'False)
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat l -> SNat k -> (l <? k) :~: ((l + 1) <=? k)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n <? m) :~: (Succ n <=? m)
lneqSuccLeq SNat l
l SNat k
k) IsTrue (OrdCond (CmpNat (l + 1) k) 'True 'True 'False)
IsTrue (l <? k)
(OrdCond (CmpNat l k) 'True 'False 'False
 ~ OrdCond (CmpNat (l + 1) k) 'True 'True 'False) =>
IsTrue (OrdCond (CmpNat (l + 1) k) 'True 'True 'False)
lLNk
        )

maxZeroL :: SNat n -> Max 0 n :~: n
maxZeroL :: forall (n :: Natural). SNat n -> Max 0 n :~: n
maxZeroL SNat n
n = SNat 0
-> SNat n -> IsTrue (0 <=? n) -> OrdCond (Compare 0 n) n n 0 :~: n
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax SNat 0
sZero SNat n
n (SNat n -> IsTrue (0 <=? n)
forall (n :: Natural). SNat n -> IsTrue (0 <=? n)
leqZero SNat n
n)

maxZeroR :: SNat n -> Max n 0 :~: n
maxZeroR :: forall (n :: Natural). SNat n -> Max n 0 :~: n
maxZeroR SNat n
n = SNat n
-> SNat 0 -> IsTrue (0 <=? n) -> OrdCond (Compare n 0) 0 0 n :~: n
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax SNat n
n SNat 0
sZero (SNat n -> IsTrue (0 <=? n)
forall (n :: Natural). SNat n -> IsTrue (0 <=? n)
leqZero SNat n
n)

minZeroL :: SNat n -> Min 0 n :~: 0
minZeroL :: forall (n :: Natural). SNat n -> Min 0 n :~: 0
minZeroL SNat n
n = SNat 0
-> SNat n -> IsTrue (0 <=? n) -> OrdCond (Compare 0 n) 0 0 n :~: 0
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin SNat 0
sZero SNat n
n (SNat n -> IsTrue (0 <=? n)
forall (n :: Natural). SNat n -> IsTrue (0 <=? n)
leqZero SNat n
n)

minZeroR :: SNat n -> Min n 0 :~: 0
minZeroR :: forall (n :: Natural). SNat n -> Min n 0 :~: 0
minZeroR SNat n
n = SNat n
-> SNat 0 -> IsTrue (0 <=? n) -> OrdCond (Compare n 0) n n 0 :~: 0
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin SNat n
n SNat 0
sZero (SNat n -> IsTrue (0 <=? n)
forall (n :: Natural). SNat n -> IsTrue (0 <=? n)
leqZero SNat n
n)

minusSucc :: SNat n -> SNat m -> IsTrue (m <=? n) -> Succ n - m :~: Succ (n - m)
minusSucc :: forall (n :: Natural) (m :: Natural).
SNat n
-> SNat m -> IsTrue (m <=? n) -> (Succ n - m) :~: Succ (n - m)
minusSucc SNat n
n SNat m
m IsTrue (m <=? n)
mLEQn =
  case SNat m -> SNat n -> IsTrue (m <=? n) -> DiffNat m n
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat m
m SNat n
n IsTrue (m <=? n)
mLEQn of
    DiffNat SNat m
_ SNat m
k ->
      SNat (Succ n - m) -> (Succ n - m) :~: (Succ n - m)
forall {k} (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat (Succ n)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat n
n SNat (Succ n) -> SNat m -> SNat (Succ n - m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n - m)
%- SNat m
m)
        ((Succ n - m) :~: (Succ n - m))
-> SNat (Succ n - m) -> (Succ n - m) :~: (Succ n - m)
forall {k1} {k2} (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat n -> SNat (Succ n)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc (SNat m
m SNat m -> SNat m -> SNat (m + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat (Succ n) -> SNat m -> SNat (Succ n - m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n - m)
%- SNat m
m
        ((Succ n - m) :~: (Succ n - m))
-> Reason (:~:) (Succ n - m) ((m + (m + 1)) - m)
-> (Succ n - m) :~: ((m + (m + 1)) - m)
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== (SNat m
m SNat m -> SNat (m + 1) -> SNat (m + (m + 1))
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat m -> SNat (m + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat m
k) SNat (m + (m + 1)) -> SNat m -> SNat ((m + (m + 1)) - m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n - m)
%- SNat m
m SNat ((m + (m + 1)) - m)
-> ((Succ n - m) :~: ((m + (m + 1)) - m))
-> Reason (:~:) (Succ n - m) ((m + (m + 1)) - m)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (Succ n :~: (m + (m + 1)))
-> SNat m -> (Succ n - m) :~: ((m + (m + 1)) - m)
forall (n :: Natural) (m :: Natural) (k :: Natural).
(n :~: m) -> SNat k -> (n - k) :~: (m - k)
minusCongL (((m + (m + 1)) :~: Succ n) -> Succ n :~: (m + (m + 1))
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (((m + (m + 1)) :~: Succ n) -> Succ n :~: (m + (m + 1)))
-> ((m + (m + 1)) :~: Succ n) -> Succ n :~: (m + (m + 1))
forall a b. (a -> b) -> a -> b
$ SNat m -> SNat m -> (m + (m + 1)) :~: S (m + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n + S m) :~: S (n + m)
plusSuccR SNat m
m SNat m
k) SNat m
m
        ((Succ n - m) :~: ((m + (m + 1)) - m))
-> Reason (:~:) ((m + (m + 1)) - m) (((m + 1) + m) - m)
-> (Succ n - m) :~: (((m + 1) + m) - m)
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== (SNat m -> SNat (m + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat m
k SNat (m + 1) -> SNat m -> SNat ((m + 1) + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m) SNat ((m + 1) + m) -> SNat m -> SNat (((m + 1) + m) - m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n - m)
%- SNat m
m SNat (((m + 1) + m) - m)
-> (((m + (m + 1)) - m) :~: (((m + 1) + m) - m))
-> Reason (:~:) ((m + (m + 1)) - m) (((m + 1) + m) - m)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` ((m + (m + 1)) :~: ((m + 1) + m))
-> SNat m -> ((m + (m + 1)) - m) :~: (((m + 1) + m) - m)
forall (n :: Natural) (m :: Natural) (k :: Natural).
(n :~: m) -> SNat k -> (n - k) :~: (m - k)
minusCongL (SNat m -> SNat (m + 1) -> (m + (m + 1)) :~: ((m + 1) + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
m (SNat m -> SNat (m + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat m
k)) SNat m
m
        ((Succ n - m) :~: (((m + 1) + m) - m))
-> Reason (:~:) (((m + 1) + m) - m) (m + 1)
-> (Succ n - m) :~: (m + 1)
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m -> SNat (m + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat m
k SNat (m + 1)
-> ((((m + 1) + m) - m) :~: (m + 1))
-> Reason (:~:) (((m + 1) + m) - m) (m + 1)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat (m + 1) -> SNat m -> (((m + 1) + m) - m) :~: (m + 1)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> ((n + m) - m) :~: n
plusMinus (SNat m -> SNat (m + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc SNat m
k) SNat m
m
        ((Succ n - m) :~: (m + 1))
-> Reason (:~:) (m + 1) (((m + m) - m) + 1)
-> (Succ n - m) :~: (((m + m) - m) + 1)
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat ((m + m) - m) -> SNat (((m + m) - m) + 1)
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc (SNat m
k SNat m -> SNat m -> SNat (m + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m SNat (m + m) -> SNat m -> SNat ((m + m) - m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n - m)
%- SNat m
m) SNat (((m + m) - m) + 1)
-> ((m + 1) :~: (((m + m) - m) + 1))
-> Reason (:~:) (m + 1) (((m + m) - m) + 1)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (m :~: ((m + m) - m)) -> (m + 1) :~: (((m + m) - m) + 1)
forall (n :: Natural) (m :: Natural). (n :~: m) -> S n :~: S m
succCong ((((m + m) - m) :~: m) -> m :~: ((m + m) - m)
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((((m + m) - m) :~: m) -> m :~: ((m + m) - m))
-> (((m + m) - m) :~: m) -> m :~: ((m + m) - m)
forall a b. (a -> b) -> a -> b
$ SNat m -> SNat m -> ((m + m) - m) :~: m
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> ((n + m) - m) :~: n
plusMinus SNat m
k SNat m
m)
        ((Succ n - m) :~: (((m + m) - m) + 1))
-> Reason (:~:) (((m + m) - m) + 1) (Succ (n - m))
-> (Succ n - m) :~: Succ (n - m)
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat (n - m) -> SNat (Succ (n - m))
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc (SNat m
m SNat m -> SNat m -> SNat (m + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k SNat n -> SNat m -> SNat (n - m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n - m)
%- SNat m
m) SNat (Succ (n - m))
-> ((((m + m) - m) + 1) :~: Succ (n - m))
-> Reason (:~:) (((m + m) - m) + 1) (Succ (n - m))
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (((m + m) - m) :~: (n - m)) -> (((m + m) - m) + 1) :~: Succ (n - m)
forall (n :: Natural) (m :: Natural). (n :~: m) -> S n :~: S m
succCong (((m + m) :~: n) -> SNat m -> ((m + m) - m) :~: (n - m)
forall (n :: Natural) (m :: Natural) (k :: Natural).
(n :~: m) -> SNat k -> (n - k) :~: (m - k)
minusCongL (SNat m -> SNat m -> (m + m) :~: (m + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
k SNat m
m) SNat m
m)
        ((Succ n - m) :~: Succ (n - m))
-> SNat (Succ (n - m)) -> (Succ n - m) :~: Succ (n - m)
forall {k1} {k2} (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat (n - m) -> SNat (Succ (n - m))
forall (n :: Natural). SNat n -> SNat (Succ n)
sSucc (SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n - m)
%- SNat m
m)

lneqZeroAbsurd :: SNat n -> IsTrue (n <? 0) -> Void
lneqZeroAbsurd :: forall (n :: Natural). SNat n -> IsTrue (n <? 0) -> Void
lneqZeroAbsurd SNat n
n IsTrue (n <? 0)
leq =
  SNat n -> IsTrue (S n <=? 0) -> Void
forall (n :: Natural). SNat n -> IsTrue (S n <=? 0) -> Void
succLeqZeroAbsurd SNat n
n ((OrdCond (CmpNat n 0) 'True 'False 'False
 :~: OrdCond (CmpNat (S n) 0) 'True 'True 'False)
-> ((OrdCond (CmpNat n 0) 'True 'False 'False
     ~ OrdCond (CmpNat (S n) 0) 'True 'True 'False) =>
    IsTrue (OrdCond (CmpNat (S n) 0) 'True 'True 'False))
-> IsTrue (OrdCond (CmpNat (S n) 0) 'True 'True 'False)
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n -> SNat 0 -> (n <? 0) :~: (S n <=? 0)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n <? m) :~: (Succ n <=? m)
lneqSuccLeq SNat n
n SNat 0
sZero) IsTrue (OrdCond (CmpNat (S n) 0) 'True 'True 'False)
IsTrue (n <? 0)
(OrdCond (CmpNat n 0) 'True 'False 'False
 ~ OrdCond (CmpNat (S n) 0) 'True 'True 'False) =>
IsTrue (OrdCond (CmpNat (S n) 0) 'True 'True 'False)
leq)

minusPlus ::
  forall n m.
  SNat n ->
  SNat m ->
  IsTrue (m <=? n) ->
  n - m + m :~: n
minusPlus :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
minusPlus SNat n
n SNat m
m IsTrue (m <=? n)
mLEQn =
  case SNat m -> SNat n -> IsTrue (m <=? n) -> DiffNat m n
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat m
m SNat n
n IsTrue (m <=? n)
mLEQn of
    DiffNat SNat m
_ SNat m
k ->
      SNat ((n - m) + m) -> ((n - m) + m) :~: ((n - m) + m)
forall {k} (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n - m)
%- SNat m
m SNat (n - m) -> SNat m -> SNat ((n - m) + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m)
        (((n - m) + m) :~: ((n - m) + m))
-> SNat ((n - m) + m) -> ((n - m) + m) :~: ((n - m) + m)
forall {k1} {k2} (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat m
m SNat m -> SNat m -> SNat (m + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k SNat n -> SNat m -> SNat (n - m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n - m)
%- SNat m
m SNat (n - m) -> SNat m -> SNat ((n - m) + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m
        (((n - m) + m) :~: ((n - m) + m))
-> Reason (:~:) ((n - m) + m) (((m + m) - m) + m)
-> ((n - m) + m) :~: (((m + m) - m) + m)
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m
k SNat m -> SNat m -> SNat (m + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m SNat (m + m) -> SNat m -> SNat ((m + m) - m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n - m)
%- SNat m
m SNat ((m + m) - m) -> SNat m -> SNat (((m + m) - m) + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m SNat (((m + m) - m) + m)
-> (((n - m) + m) :~: (((m + m) - m) + m))
-> Reason (:~:) ((n - m) + m) (((m + m) - m) + m)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` ((n - m) :~: ((m + m) - m))
-> SNat m -> ((n - m) + m) :~: (((m + m) - m) + m)
forall (n :: Natural) (m :: Natural) (k :: Natural).
(n :~: m) -> SNat k -> (n + k) :~: (m + k)
plusCongL ((n :~: (m + m)) -> SNat m -> (n - m) :~: ((m + m) - m)
forall (n :: Natural) (m :: Natural) (k :: Natural).
(n :~: m) -> SNat k -> (n - k) :~: (m - k)
minusCongL (SNat m -> SNat m -> (m + m) :~: (m + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
m SNat m
k) SNat m
m) SNat m
m
        (((n - m) + m) :~: (((m + m) - m) + m))
-> Reason (:~:) (((m + m) - m) + m) (m + m)
-> ((n - m) + m) :~: (m + m)
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m
k SNat m -> SNat m -> SNat (m + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m SNat (m + m)
-> ((((m + m) - m) + m) :~: (m + m))
-> Reason (:~:) (((m + m) - m) + m) (m + m)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (((m + m) - m) :~: m) -> SNat m -> (((m + m) - m) + m) :~: (m + m)
forall (n :: Natural) (m :: Natural) (k :: Natural).
(n :~: m) -> SNat k -> (n + k) :~: (m + k)
plusCongL (SNat m -> SNat m -> ((m + m) - m) :~: m
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> ((n + m) - m) :~: n
plusMinus SNat m
k SNat m
m) SNat m
m
        (((n - m) + m) :~: (m + m))
-> Reason (:~:) (m + m) n -> ((n - m) + m) :~: n
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m
m SNat m -> SNat m -> SNat (m + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k SNat n -> ((m + m) :~: n) -> Reason (:~:) (m + m) n
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat m -> SNat m -> (m + m) :~: (m + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
k SNat m
m
        (((n - m) + m) :~: n) -> SNat n -> ((n - m) + m) :~: n
forall {k1} {k2} (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat n
n

-- | Natural subtraction, truncated to zero if m > n.
type n -. m = Subt n m (m <=? n)

type family Subt n m (b :: Bool) where
  Subt n m 'True = n - m
  Subt n m 'False = 0

infixl 6 -.

(%-.) :: SNat n -> SNat m -> SNat (n -. m)
SNat n
n %-. :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m =
  case SNat m
m SNat m -> SNat n -> SBool (m <=? n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat n
n of
    SBool (m <=? n)
STrue -> SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n - m)
%- SNat m
m
    SBool (m <=? n)
SFalse -> SNat 0
SNat (n -. m)
sZero

minPlusTruncMinus ::
  SNat n ->
  SNat m ->
  Min n m + (n -. m) :~: n
minPlusTruncMinus :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (Min n m + (n -. m)) :~: n
minPlusTruncMinus SNat n
n SNat m
m =
  case SNat m
m SNat m -> SNat n -> SBool (m <=? n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat n
n of
    SBool (m <=? n)
STrue ->
      SNat (OrdCond (CmpNat n m) n n m + (n - m))
-> (OrdCond (CmpNat n m) n n m + (n - m))
   :~: (OrdCond (CmpNat n m) n n m + (n - m))
forall {k} (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m SNat (OrdCond (CmpNat n m) n n m)
-> SNat (n - m) -> SNat (OrdCond (CmpNat n m) n n m + (n - m))
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ (SNat n
n SNat n -> SNat m -> SNat (n -. m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m))
        ((OrdCond (CmpNat n m) n n m + (n - m))
 :~: (OrdCond (CmpNat n m) n n m + (n - m)))
-> Reason
     (:~:) (OrdCond (CmpNat n m) n n m + (n - m)) (m + (n - m))
-> (OrdCond (CmpNat n m) n n m + (n - m)) :~: (m + (n - m))
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m
m SNat m -> SNat (n - m) -> SNat (m + (n - m))
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ (SNat n
n SNat n -> SNat m -> SNat (n -. m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m) SNat (m + (n - m))
-> ((OrdCond (CmpNat n m) n n m + (n - m)) :~: (m + (n - m)))
-> Reason
     (:~:) (OrdCond (CmpNat n m) n n m + (n - m)) (m + (n - m))
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` (OrdCond (CmpNat n m) n n m :~: m)
-> SNat (n - m)
-> (OrdCond (CmpNat n m) n n m + (n - m)) :~: (m + (n - m))
forall (n :: Natural) (m :: Natural) (k :: Natural).
(n :~: m) -> SNat k -> (n + k) :~: (m + k)
plusCongL (SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin SNat n
n SNat m
m IsTrue 'True
IsTrue (m <=? n)
Witness) (SNat n
n SNat n -> SNat m -> SNat (n -. m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m)
        ((OrdCond (CmpNat n m) n n m + (n - m)) :~: (m + (n - m)))
-> SNat (m + (n - m))
-> (OrdCond (CmpNat n m) n n m + (n - m)) :~: (m + (n - m))
forall {k1} {k2} (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat m
m SNat m -> SNat (n - m) -> SNat (m + (n - m))
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ (SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n - m)
%- SNat m
m)
        ((OrdCond (CmpNat n m) n n m + (n - m)) :~: (m + (n - m)))
-> Reason (:~:) (m + (n - m)) ((n - m) + m)
-> (OrdCond (CmpNat n m) n n m + (n - m)) :~: ((n - m) + m)
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== (SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n - m)
%- SNat m
m) SNat (n - m) -> SNat m -> SNat ((n - m) + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m SNat ((n - m) + m)
-> ((m + (n - m)) :~: ((n - m) + m))
-> Reason (:~:) (m + (n - m)) ((n - m) + m)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat m -> SNat (n - m) -> (m + (n - m)) :~: ((n - m) + m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
m (SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n - m)
%- SNat m
m)
        ((OrdCond (CmpNat n m) n n m + (n - m)) :~: ((n - m) + m))
-> Reason (:~:) ((n - m) + m) n
-> (OrdCond (CmpNat n m) n n m + (n - m)) :~: n
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> (((n - m) + m) :~: n) -> Reason (:~:) ((n - m) + m) n
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
minusPlus SNat n
n SNat m
m IsTrue 'True
IsTrue (m <=? n)
Witness
    SBool (m <=? n)
SFalse ->
      SNat (OrdCond (CmpNat n m) n n m)
-> OrdCond (CmpNat n m) n n m :~: OrdCond (CmpNat n m) n n m
forall {k} (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m SNat (OrdCond (CmpNat n m) n n m)
-> SNat 0 -> SNat (OrdCond (CmpNat n m) n n m + 0)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ (SNat n
n SNat n -> SNat m -> SNat (n -. m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m))
        (OrdCond (CmpNat n m) n n m :~: OrdCond (CmpNat n m) n n m)
-> SNat (OrdCond (CmpNat n m) n n m)
-> OrdCond (CmpNat n m) n n m :~: OrdCond (CmpNat n m) n n m
forall {k1} {k2} (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat n -> SNat m -> SNat (Min n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m SNat (OrdCond (CmpNat n m) n n m)
-> SNat 0 -> SNat (OrdCond (CmpNat n m) n n m + 0)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ SNat 0
sZero
        (OrdCond (CmpNat n m) n n m :~: OrdCond (CmpNat n m) n n m)
-> Reason
     (:~:) (OrdCond (CmpNat n m) n n m) (OrdCond (CmpNat n m) n n m)
-> OrdCond (CmpNat n m) n n m :~: OrdCond (CmpNat n m) n n m
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n -> SNat m -> SNat (Min n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m SNat (OrdCond (CmpNat n m) n n m)
-> (OrdCond (CmpNat n m) n n m :~: OrdCond (CmpNat n m) n n m)
-> Reason
     (:~:) (OrdCond (CmpNat n m) n n m) (OrdCond (CmpNat n m) n n m)
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat (OrdCond (CmpNat n m) n n m)
-> (OrdCond (CmpNat n m) n n m + 0) :~: OrdCond (CmpNat n m) n n m
forall (n :: Natural). SNat n -> (n + 0) :~: n
plusZeroR (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m)
        (OrdCond (CmpNat n m) n n m :~: OrdCond (CmpNat n m) n n m)
-> Reason (:~:) (OrdCond (CmpNat n m) n n m) n
-> OrdCond (CmpNat n m) n n m :~: n
forall {k} (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n
-> (OrdCond (CmpNat n m) n n m :~: n)
-> Reason (:~:) (OrdCond (CmpNat n m) n n m) n
forall {k1} {k2} (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin SNat n
n SNat m
m (SNat m -> SNat n -> IsTrue (n <=? m)
forall (n :: Natural) (m :: Natural).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat m
m SNat n
n)

truncMinusLeq :: SNat n -> SNat m -> IsTrue ((n -. m) <=? n)
truncMinusLeq :: forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue ((n -. m) <=? n)
truncMinusLeq SNat n
n SNat m
m =
  case SNat m
m SNat m -> SNat n -> SBool (m <=? n)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat n
n of
    SBool (m <=? n)
STrue -> SNat (n - m)
-> SNat n
-> SNat m
-> (((n - m) + m) :~: n)
-> IsTrue ((n - m) <=? n)
forall (n :: Natural) (m :: Natural) (l :: Natural).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep (SNat n
n SNat n -> SNat m -> SNat (n -. m)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m) SNat n
n SNat m
m ((((n - m) + m) :~: n) -> IsTrue ((n - m) <=? n))
-> (((n - m) + m) :~: n) -> IsTrue ((n - m) <=? n)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
minusPlus SNat n
n SNat m
m IsTrue 'True
IsTrue (m <=? n)
Witness
    SBool (m <=? n)
SFalse -> SNat n -> IsTrue (0 <=? n)
forall (n :: Natural). SNat n -> IsTrue (0 <=? n)
leqZero SNat n
n