{-# LANGUAGE DataKinds #-}
{-# 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,

    -- * Lemmas
    sFlipOrdering,
    coerceLeqL,
    coerceLeqR,
    sLeqCongL,
    sLeqCongR,
    sLeqCong,
    succDiffNat,
    compareCongR,
    leqToCmp,
    eqlCmpEQ,
    eqToRefl,
    flipCmpNat,
    ltToNeq,
    leqNeqToLT,
    succLeqToLT,
    ltToLeq,
    gtToLeq,
    congFlipOrdering,
    ltToSuccLeq,
    cmpZero,
    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,
    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.Coerce (coerce)
import Data.Type.Equality (gcastWith, (:~:) (..))
import Data.Type.Natural.Core
import Data.Type.Natural.Lemma.Arithmetic
import Data.Void (Void, absurd)
import Numeric.Natural (Natural)
import Proof.Equational
  ( because,
    start,
    sym,
    trans,
    withRefl,
    (===),
    (=~=),
  )
import Proof.Propositional (IsTrue (..), eliminate, withWitness)

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

-- ** Type-level predicate & judgements.

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

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

data a :<: b where
  ZeroLtSucc :: 0 :<: (m + 1)
  SuccLtSucc :: 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 :: Leq n m -> LeqWitness n m
propToBoolLeq (ZeroLeq SNat m
_) = LeqWitness n m
IsTrue 'True
Witness
propToBoolLeq (SuccLeqSucc Leq n m
leq) = IsTrue (n <=? m)
-> (((n <=? m) ~ 'True) => LeqWitness n m) -> LeqWitness n m
forall (b :: Bool) r. IsTrue b -> ((b ~ 'True) => r) -> r
withWitness (Leq n m -> IsTrue (n <=? m)
forall (n :: Nat) (m :: Nat). Leq n m -> LeqWitness n m
propToBoolLeq Leq n m
leq) IsTrue 'True
((n <=? m) ~ 'True) => LeqWitness n m
Witness
{-# INLINE propToBoolLeq #-}

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

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

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

propToBoolLt :: n :<: m -> IsTrue (n <? m)
propToBoolLt :: (n :<: m) -> IsTrue (n <? m)
propToBoolLt n :<: m
ZeroLtSucc = IsTrue (n <? m)
IsTrue 'True
Witness
propToBoolLt (SuccLtSucc n :<: m
lt) =
  IsTrue (n <=? m)
-> (((n <=? m) ~ 'True) => IsTrue (n <? m)) -> IsTrue (n <? m)
forall (b :: Bool) r. IsTrue b -> ((b ~ 'True) => r) -> r
withWitness ((n :<: m) -> IsTrue (n <? m)
forall (n :: Nat) (m :: Nat). (n :<: m) -> IsTrue (n <? m)
propToBoolLt n :<: m
lt) IsTrue 'True
((n <=? m) ~ 'True) => IsTrue (n <? m)
Witness

boolToPropLt :: n < m => SNat n -> SNat m -> n :<: m
boolToPropLt :: SNat n -> SNat m -> n :<: m
boolToPropLt SNat n
Zero (Succ SNat n1
_) = n :<: m
forall (m :: Nat). 0 :<: (m + 1)
ZeroLtSucc
boolToPropLt (Succ SNat n1
_) SNat m
Zero = (0 :~: 1) -> n :<: m
forall a x. Empty a => a -> x
eliminate (0 :~: 1
forall k (a :: k). a :~: a
Refl :: 0 :~: 1)
boolToPropLt (Succ SNat n1
n) (Succ SNat n1
m) = (n1 :<: n1) -> (n1 + 1) :<: (n1 + 1)
forall (n :: Nat) (m :: Nat). (n :<: m) -> (n + 1) :<: (m + 1)
SuccLtSucc (SNat n1 -> SNat n1 -> n1 :<: n1
forall (n :: Nat) (m :: Nat).
(n < m) =>
SNat n -> SNat m -> n :<: m
boolToPropLt SNat n1
n SNat n1
m)

type Min n m = MinAux (n <=? m) n m

sMin :: SNat n -> SNat m -> SNat (Min n m)
sMin :: SNat n -> SNat m -> SNat (Min n m)
sMin = (Natural -> Natural -> Natural)
-> SNat n -> SNat m -> SNat (Min n m)
coerce ((Natural -> Natural -> Natural)
 -> SNat n -> SNat m -> SNat (Min n m))
-> (Natural -> Natural -> Natural)
-> SNat n
-> SNat m
-> SNat (Min n m)
forall a b. (a -> b) -> a -> b
$ Ord Natural => Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
min @Natural

sMax :: SNat n -> SNat m -> SNat (Max n m)
sMax :: SNat n -> SNat m -> SNat (Max n m)
sMax = (Natural -> Natural -> Natural)
-> SNat n -> SNat m -> SNat (Max n m)
coerce ((Natural -> Natural -> Natural)
 -> SNat n -> SNat m -> SNat (Max n m))
-> (Natural -> Natural -> Natural)
-> SNat n
-> SNat m
-> SNat (Max n m)
forall a b. (a -> b) -> a -> b
$ Ord Natural => Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
max @Natural

type family MinAux (p :: Bool) (n :: Nat) (m :: Nat) :: Nat where
  MinAux 'True n _ = n
  MinAux 'False _ m = m

type Max n m = MaxAux (n >=? m) n m

type family MaxAux (p :: Bool) (n :: Nat) (m :: Nat) :: Nat where
  MaxAux 'True n _ = n
  MaxAux 'False _ m = m

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

type n <? m = n + 1 <=? m

(%<?) :: SNat n -> SNat m -> SBool (n <? m)
%<? :: SNat n -> SNat m -> SBool (n <? m)
(%<?) = SNat (n + 1) -> SNat m -> SBool (n <? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
(%<=?) (SNat (n + 1) -> SNat m -> SBool (n <? m))
-> (SNat n -> SNat (n + 1)) -> SNat n -> SNat m -> SBool (n <? m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat n -> SNat (n + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc

type n < m = (n <? m) ~ 'True

type n >=? m = m <=? n

(%>=?) :: SNat n -> SNat m -> SBool (n >=? m)
%>=? :: SNat n -> SNat m -> SBool (n >=? m)
(%>=?) = (SNat m -> SNat n -> SBool (n >=? m))
-> SNat n -> SNat m -> SBool (n >=? m)
forall a b c. (a -> b -> c) -> b -> a -> c
flip SNat m -> SNat n -> SBool (n >=? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
(%<=?)

type n >= m = (n >=? m) ~ 'True

type n >? m = m <? n

(%>?) :: SNat n -> SNat m -> SBool (n >? m)
%>? :: SNat n -> SNat m -> SBool (n >? m)
(%>?) = (SNat m -> SNat n -> SBool (n >? m))
-> SNat n -> SNat m -> SBool (n >? m)
forall a b c. (a -> b -> c) -> b -> a -> c
flip SNat m -> SNat n -> SBool (n >? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <? m)
(%<?)

type n > m = (n >? m) ~ 'True

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

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 {LeqWitPf n
-> forall (m :: Nat). SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitPf :: forall m. SNat m -> IsTrue (n <=? m) -> DiffNat n m}

newtype LeqStepPf n = LeqStepPf {LeqStepPf n
-> forall (m :: Nat) (l :: Nat).
   SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStepPf :: forall m l. SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m)}

succDiffNat :: SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m)
succDiffNat :: SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m)
succDiffNat SNat n
_ SNat m
_ (DiffNat SNat n
n SNat m
m) = ((Succ n + m) :~: Succ m)
-> (((Succ n + m) ~ Succ m) => DiffNat (Succ n) (Succ m))
-> DiffNat (Succ n) (Succ m)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n -> SNat m -> (Succ n + m) :~: S (n + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat n
n SNat m
m) ((((Succ n + m) ~ Succ m) => DiffNat (Succ n) (Succ m))
 -> DiffNat (Succ n) (Succ m))
-> (((Succ n + m) ~ Succ m) => DiffNat (Succ n) (Succ m))
-> DiffNat (Succ n) (Succ m)
forall a b. (a -> b) -> a -> b
$ SNat (Succ n) -> SNat m -> DiffNat (Succ n) (Succ n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> DiffNat n (n + m)
DiffNat (SNat n -> SNat (Succ n)
forall (n :: Nat). 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 :: (n :~: m) -> SNat l -> IsTrue (n <=? l) -> IsTrue (m <=? l)
coerceLeqL n :~: m
Refl SNat l
_ IsTrue (n <=? l)
Witness = IsTrue (m <=? l)
IsTrue 'True
Witness

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

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

sLeqCong :: a :~: b -> c :~: d -> (a <= c) :~: (b <= d)
sLeqCong :: (a :~: b) -> (c :~: d) -> (a <= c) :~: (b <= d)
sLeqCong a :~: b
Refl c :~: d
Refl = (a <= c) :~: (b <= d)
forall k (a :: k). a :~: a
Refl

sLeqCongL :: a :~: b -> SNat c -> (a <= c) :~: (b <= c)
sLeqCongL :: (a :~: b) -> SNat c -> (a <= c) :~: (b <= c)
sLeqCongL a :~: b
Refl SNat c
_ = (a <= c) :~: (b <= c)
forall k (a :: k). a :~: a
Refl

sLeqCongR :: SNat a -> b :~: c -> (a <= b) :~: (a <= c)
sLeqCongR :: SNat a -> (b :~: c) -> (a <= b) :~: (a <= c)
sLeqCongR SNat a
_ b :~: c
Refl = (a <= b) :~: (a <= c)
forall k (a :: k). a :~: a
Refl

newtype LTSucc n = LTSucc {LTSucc n -> CmpNat n (Succ n) :~: 'LT
proofLTSucc :: CmpNat n (Succ n) :~: 'LT}

newtype CmpSuccStepR n = CmpSuccStepR
  { CmpSuccStepR n
-> forall (m :: Nat).
   SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
proofCmpSuccStepR ::
      forall m.
      SNat m ->
      CmpNat n m :~: 'LT ->
      CmpNat n (Succ m) :~: 'LT
  }

newtype LeqViewRefl n = LeqViewRefl {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 :: 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 :: Nat) (r :: Nat). SNat l -> SNat r -> Equality l r
%~ SNat b
m of
    Equality a b
Equal -> (a :~: a) -> Either (a :~: a) ('EQ :~: 'LT)
forall a b. a -> Either a b
Left a :~: a
forall k (a :: k). a :~: a
Refl
    Equality a b
NonEqual -> ('LT :~: 'LT) -> Either (a :~: b) ('LT :~: 'LT)
forall a b. b -> Either a b
Right 'LT :~: 'LT
forall k (a :: k). a :~: a
Refl

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

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

flipCmpNat ::
  SNat a ->
  SNat b ->
  FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat :: 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 :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
n SNat b
m of
  SOrdering (CmpNat a b)
SGT -> FlipOrdering (CmpNat a b) :~: CmpNat b a
forall k (a :: k). a :~: a
Refl
  SOrdering (CmpNat a b)
SLT -> FlipOrdering (CmpNat a b) :~: CmpNat b a
forall k (a :: k). a :~: a
Refl
  SOrdering (CmpNat a b)
SEQ -> 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 :: 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 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 :: Nat) (m :: Nat).
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 :: Nat) (b :: Nat).
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 :: 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 :: Nat) (b :: Nat).
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 :: SNat a -> SNat b -> IsTrue (S a <=? b) -> CmpNat a b :~: 'LT
succLeqToLT SNat a
a SNat b
b IsTrue (S a <=? b)
saLEQb =
  case SNat (S a) -> SNat b -> IsTrue (S a <=? b) -> DiffNat (S a) b
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness (SNat a -> SNat (S a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
a) SNat b
b IsTrue (S a <=? b)
saLEQb of
    DiffNat SNat (S a)
_ SNat m
k ->
      let aLEQb :: IsTrue (a <=? b)
aLEQb =
            SNat a
-> SNat b
-> SNat (m + 1)
-> ((a + (m + 1)) :~: b)
-> IsTrue (a <=? b)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep SNat a
a SNat b
b (SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k) (((a + (m + 1)) :~: b) -> IsTrue (a <=? b))
-> ((a + (m + 1)) :~: b) -> IsTrue (a <=? b)
forall a b. (a -> b) -> a -> b
$
              SNat (a + (m + 1)) -> (a + (m + 1)) :~: (a + (m + 1))
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat a
a SNat a -> SNat (m + 1) -> SNat (a + (m + 1))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k)
                ((a + (m + 1)) :~: (a + (m + 1)))
-> Reason (:~:) (a + (m + 1)) ((a + m) + 1)
-> (a + (m + 1)) :~: ((a + 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 (a + m) -> SNat ((a + m) + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat a
a SNat a -> SNat m -> SNat (a + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat ((a + m) + 1)
-> ((a + (m + 1)) :~: ((a + m) + 1))
-> Reason (:~:) (a + (m + 1)) ((a + 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 a -> SNat m -> (a + (m + 1)) :~: ((a + m) + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + S m) :~: S (n + m)
plusSuccR SNat a
a SNat m
k
                ((a + (m + 1)) :~: ((a + m) + 1))
-> Reason (:~:) ((a + m) + 1) b -> (a + (m + 1)) :~: 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 (S a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
a SNat (S a) -> SNat m -> SNat (S a + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k SNat b -> (((a + m) + 1) :~: b) -> Reason (:~:) ((a + m) + 1) 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` (b :~: ((a + m) + 1)) -> ((a + m) + 1) :~: b
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat a -> SNat m -> (S a + m) :~: ((a + m) + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat a
a SNat m
k)
                ((a + (m + 1)) :~: b) -> SNat b -> (a + (m + 1)) :~: b
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat b
b
          aNEQb :: (a :~: b) -> Void
aNEQb a :~: b
aeqb =
            SNat m -> ((m + 1) :~: 0) -> Void
forall (n :: Nat). SNat n -> (Succ n :~: 0) -> Void
succNonCyclic SNat m
k (((m + 1) :~: 0) -> Void) -> ((m + 1) :~: 0) -> Void
forall a b. (a -> b) -> a -> b
$
              SNat a
-> SNat (m + 1)
-> SNat 0
-> ((a + (m + 1)) :~: (a + 0))
-> (m + 1) :~: 0
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) :~: (n + l)) -> m :~: l
plusEqCancelL SNat a
a (SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k) SNat 0
sZero (((a + (m + 1)) :~: (a + 0)) -> (m + 1) :~: 0)
-> ((a + (m + 1)) :~: (a + 0)) -> (m + 1) :~: 0
forall a b. (a -> b) -> a -> b
$
                SNat (a + (m + 1)) -> (a + (m + 1)) :~: (a + (m + 1))
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat a
a SNat a -> SNat (m + 1) -> SNat (a + (m + 1))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k)
                  ((a + (m + 1)) :~: (a + (m + 1)))
-> Reason (:~:) (a + (m + 1)) ((a + m) + 1)
-> (a + (m + 1)) :~: ((a + 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 (a + m) -> SNat ((a + m) + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat a
a SNat a -> SNat m -> SNat (a + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat ((a + m) + 1)
-> ((a + (m + 1)) :~: ((a + m) + 1))
-> Reason (:~:) (a + (m + 1)) ((a + 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 a -> SNat m -> (a + (m + 1)) :~: ((a + m) + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + S m) :~: S (n + m)
plusSuccR SNat a
a SNat m
k
                  ((a + (m + 1)) :~: ((a + m) + 1))
-> Reason (:~:) ((a + m) + 1) b -> (a + (m + 1)) :~: 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 (S a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
a SNat (S a) -> SNat m -> SNat (S a + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k SNat b -> (((a + m) + 1) :~: b) -> Reason (:~:) ((a + m) + 1) 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` (b :~: ((a + m) + 1)) -> ((a + m) + 1) :~: b
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat a -> SNat m -> (S a + m) :~: ((a + m) + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat a
a SNat m
k)
                  ((a + (m + 1)) :~: b) -> SNat b -> (a + (m + 1)) :~: b
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat b
b
                  ((a + (m + 1)) :~: b) -> Reason (:~:) b a -> (a + (m + 1)) :~: 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 a
a SNat a -> (b :~: a) -> Reason (:~:) b 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` (a :~: b) -> b :~: a
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym a :~: b
aeqb
                  ((a + (m + 1)) :~: a) -> Reason (:~:) a a -> (a + (m + 1)) :~: 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 a
a SNat a -> SNat 0 -> SNat (a + 0)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat 0
sZero SNat a -> (a :~: a) -> Reason (:~:) a 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` (a :~: a) -> a :~: a
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat a -> (a + 0) :~: a
forall (n :: Nat). SNat n -> (n + 0) :~: n
plusZeroR SNat a
a)
       in SNat a
-> SNat b
-> IsTrue (a <=? b)
-> ((a :~: b) -> Void)
-> CmpNat a b :~: 'LT
forall (a :: Nat) (b :: Nat).
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

ltToLeq ::
  SNat a ->
  SNat b ->
  CmpNat a b :~: 'LT ->
  IsTrue (a <=? b)
ltToLeq :: SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)
ltToLeq SNat a
_ SNat b
_ CmpNat a b :~: 'LT
Refl = IsTrue (a <=? b)
IsTrue 'True
Witness

gtToLeq ::
  SNat a ->
  SNat b ->
  CmpNat a b :~: 'GT ->
  IsTrue (b <=? a)
gtToLeq :: SNat a -> SNat b -> (CmpNat a b :~: 'GT) -> IsTrue (b <=? a)
gtToLeq SNat a
n SNat b
m CmpNat a b :~: 'GT
nGTm =
  SNat b -> SNat a -> (CmpNat b a :~: 'LT) -> IsTrue (b <=? a)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)
ltToLeq SNat b
m SNat a
n ((CmpNat b a :~: 'LT) -> IsTrue (b <=? a))
-> (CmpNat b a :~: 'LT) -> IsTrue (b <=? a)
forall a b. (a -> b) -> a -> b
$
    SOrdering (CmpNat b a) -> CmpNat b a :~: CmpNat b a
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat b -> SNat a -> SOrdering (CmpNat b a)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat b
m SNat a
n) (CmpNat b a :~: CmpNat b a)
-> Reason (:~:) (CmpNat b a) (FlipOrdering (CmpNat a b))
-> CmpNat b a :~: FlipOrdering (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
=== SOrdering (CmpNat a b) -> SOrdering (FlipOrdering (CmpNat a b))
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering (SNat a -> SNat b -> SOrdering (CmpNat a b)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
n SNat b
m) SOrdering (FlipOrdering (CmpNat a b))
-> (CmpNat b a :~: FlipOrdering (CmpNat a b))
-> Reason (:~:) (CmpNat b a) (FlipOrdering (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` (FlipOrdering (CmpNat a b) :~: CmpNat b a)
-> CmpNat b a :~: FlipOrdering (CmpNat a b)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat SNat a
n SNat b
m)
      (CmpNat b a :~: FlipOrdering (CmpNat a b))
-> Reason (:~:) (FlipOrdering (CmpNat a b)) 'LT
-> CmpNat b a :~: '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 'GT -> SOrdering (FlipOrdering 'GT)
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering SOrdering 'GT
SGT SOrdering 'LT
-> (FlipOrdering (CmpNat a b) :~: 'LT)
-> Reason (:~:) (FlipOrdering (CmpNat a b)) '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 a b :~: 'GT)
-> FlipOrdering (CmpNat a b) :~: FlipOrdering 'GT
forall (a :: Ordering) (b :: Ordering).
(a :~: b) -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering CmpNat a b :~: 'GT
nGTm
      (CmpNat b a :~: 'LT) -> SOrdering 'LT -> CmpNat b a :~: 'LT
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SOrdering 'LT
SLT

congFlipOrdering ::
  a :~: b -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering :: (a :~: b) -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering a :~: b
Refl = 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 :: SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)
ltToSuccLeq SNat a
n SNat b
m CmpNat a b :~: 'LT
nLTm =
  SNat a
-> SNat b
-> IsTrue (a <=? b)
-> ((a :~: b) -> Void)
-> IsTrue (Succ a <=? b)
forall (n :: Nat) (m :: Nat).
SNat n
-> SNat m
-> IsTrue (n <=? m)
-> ((n :~: m) -> Void)
-> IsTrue (Succ n <=? m)
leqNeqToSuccLeq SNat a
n SNat b
m (SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)
ltToLeq SNat a
n SNat b
m CmpNat a b :~: 'LT
nLTm) (SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> (a :~: b) -> Void
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> (a :~: b) -> Void
ltToNeq SNat a
n SNat b
m CmpNat a b :~: 'LT
nLTm)

cmpZero :: SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero :: SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero SNat a
sn =
  SNat 0
-> SNat (Succ a)
-> IsTrue (Succ 0 <=? Succ a)
-> CmpNat 0 (Succ a) :~: 'LT
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT
leqToLT SNat 0
sZero (SNat a -> SNat (Succ a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
sn) (IsTrue (Succ 0 <=? Succ a) -> CmpNat 0 (Succ a) :~: 'LT)
-> IsTrue (Succ 0 <=? Succ a) -> CmpNat 0 (Succ a) :~: 'LT
forall a b. (a -> b) -> a -> b
$
    SNat 1
-> SNat (Succ a)
-> SNat a
-> ((1 + a) :~: Succ a)
-> IsTrue (1 <=? Succ a)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep (SNat 0 -> SNat (Succ 0)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat 0
sZero) (SNat a -> SNat (Succ a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
sn) SNat a
sn (((1 + a) :~: Succ a) -> IsTrue (1 <=? Succ a))
-> ((1 + a) :~: Succ a) -> IsTrue (1 <=? Succ a)
forall a b. (a -> b) -> a -> b
$
      SNat (1 + a) -> (1 + a) :~: (1 + a)
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat 0 -> SNat (Succ 0)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat 0
sZero SNat 1 -> SNat a -> SNat (1 + a)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat a
sn)
        ((1 + a) :~: (1 + a))
-> Reason (:~:) (1 + a) (Succ a) -> (1 + a) :~: Succ 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 a -> SNat (Succ a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat 0
sZero SNat 0 -> SNat a -> SNat (0 + a)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat a
sn) SNat (Succ a)
-> ((1 + a) :~: Succ a) -> Reason (:~:) (1 + a) (Succ 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 0 -> SNat a -> (Succ 0 + a) :~: S (0 + a)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat 0
sZero SNat a
sn
        ((1 + a) :~: Succ a)
-> Reason (:~:) (Succ a) (Succ a) -> (1 + a) :~: Succ 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 a -> SNat (Succ a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
sn SNat (Succ a)
-> (Succ a :~: Succ a) -> Reason (:~:) (Succ a) (Succ 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` (a :~: a) -> Succ a :~: Succ a
forall (n :: Nat) (m :: Nat). (n :~: m) -> S n :~: S m
succCong (SNat a -> (0 + a) :~: a
forall (n :: Nat). SNat n -> (0 + n) :~: n
plusZeroL SNat a
sn)

leqToGT ::
  SNat a ->
  SNat b ->
  IsTrue (Succ b <=? a) ->
  CmpNat a b :~: 'GT
leqToGT :: SNat a -> SNat b -> IsTrue (Succ b <=? a) -> CmpNat a b :~: 'GT
leqToGT SNat a
a SNat b
b IsTrue (Succ b <=? a)
sbLEQa =
  SOrdering (CmpNat a b) -> CmpNat a b :~: CmpNat a b
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat a -> SNat b -> SOrdering (CmpNat a b)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
a SNat b
b)
    (CmpNat a b :~: CmpNat a b)
-> Reason (:~:) (CmpNat a b) (FlipOrdering (CmpNat b a))
-> CmpNat a b :~: FlipOrdering (CmpNat b 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
=== SOrdering (CmpNat b a) -> SOrdering (FlipOrdering (CmpNat b a))
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering (SNat b -> SNat a -> SOrdering (CmpNat b a)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat b
b SNat a
a) SOrdering (FlipOrdering (CmpNat b a))
-> (CmpNat a b :~: FlipOrdering (CmpNat b a))
-> Reason (:~:) (CmpNat a b) (FlipOrdering (CmpNat b 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` (FlipOrdering (CmpNat b a) :~: CmpNat a b)
-> CmpNat a b :~: FlipOrdering (CmpNat b a)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat b -> SNat a -> FlipOrdering (CmpNat b a) :~: CmpNat a b
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat SNat b
b SNat a
a)
    (CmpNat a b :~: FlipOrdering (CmpNat b a))
-> Reason (:~:) (FlipOrdering (CmpNat b a)) 'GT
-> CmpNat a b :~: 'GT
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 -> SOrdering (FlipOrdering 'LT)
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering SOrdering 'LT
SLT SOrdering 'GT
-> (FlipOrdering (CmpNat b a) :~: 'GT)
-> Reason (:~:) (FlipOrdering (CmpNat b a)) 'GT
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 b a :~: 'LT)
-> FlipOrdering (CmpNat b a) :~: FlipOrdering 'LT
forall (a :: Ordering) (b :: Ordering).
(a :~: b) -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering (SNat b -> SNat a -> IsTrue (Succ b <=? a) -> CmpNat b a :~: 'LT
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT
leqToLT SNat b
b SNat a
a IsTrue (Succ b <=? a)
sbLEQa)
    (CmpNat a b :~: 'GT) -> SOrdering 'GT -> CmpNat a b :~: 'GT
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SOrdering 'GT
SGT

cmpZero' :: SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
cmpZero' :: SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
cmpZero' SNat a
n =
  case SNat a -> ZeroOrSucc a
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc SNat a
n of
    ZeroOrSucc a
IsZero -> ('EQ :~: 'EQ) -> Either ('EQ :~: 'EQ) ('EQ :~: 'LT)
forall a b. a -> Either a b
Left (('EQ :~: 'EQ) -> Either ('EQ :~: 'EQ) ('EQ :~: 'LT))
-> ('EQ :~: 'EQ) -> Either ('EQ :~: 'EQ) ('EQ :~: 'LT)
forall a b. (a -> b) -> a -> b
$ SNat 0 -> SNat a -> (0 :~: a) -> CmpNat 0 a :~: 'EQ
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ
eqlCmpEQ SNat 0
sZero SNat a
n 0 :~: a
forall k (a :: k). a :~: a
Refl
    IsSucc SNat n
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 n -> CmpNat 0 (Succ n) :~: 'LT
forall (a :: Nat). SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero SNat n
n'

zeroNoLT :: SNat a -> CmpNat a 0 :~: 'LT -> Void
zeroNoLT :: 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 :: Nat).
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 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 :: Nat) (m :: Nat).
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 :: Nat) (m :: Nat).
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 :: Nat) (b :: Nat).
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 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 :: Nat) (m :: Nat).
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 :: Nat) (m :: Nat).
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 :: Nat) (b :: Nat).
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 :: SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> b :~: Succ (Pred b)
ltRightPredSucc SNat a
a SNat b
b CmpNat a b :~: 'LT
aLTb =
  case SNat b -> ZeroOrSucc b
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc SNat b
b of
    ZeroOrSucc b
IsZero -> Void -> 0 :~: ((0 - 1) + 1)
forall a. Void -> a
absurd (Void -> 0 :~: ((0 - 1) + 1)) -> Void -> 0 :~: ((0 - 1) + 1)
forall a b. (a -> b) -> a -> b
$ SNat a -> (CmpNat a 0 :~: 'LT) -> Void
forall (a :: Nat). SNat a -> (CmpNat a 0 :~: 'LT) -> Void
zeroNoLT SNat a
a CmpNat a b :~: 'LT
CmpNat a 0 :~: 'LT
aLTb
    IsSucc SNat n
b' ->
      (Succ (Pred b) :~: b) -> b :~: Succ (Pred b)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((Succ (Pred b) :~: b) -> b :~: Succ (Pred b))
-> (Succ (Pred b) :~: b) -> b :~: Succ (Pred b)
forall a b. (a -> b) -> a -> b
$
        SNat (Succ (Pred b)) -> Succ (Pred b) :~: Succ (Pred b)
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat (Pred b) -> SNat (Succ (Pred b))
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat b -> SNat (Pred b)
forall (n :: Nat). SNat n -> SNat (Pred n)
sPred SNat b
b))
          (Succ (Pred b) :~: Succ (Pred b))
-> SNat (Succ (Pred b)) -> Succ (Pred b) :~: Succ (Pred b)
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat (Pred b) -> SNat (Succ (Pred b))
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat b -> SNat (Pred b)
forall (n :: Nat). SNat n -> SNat (Pred n)
sPred (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
b'))
          (Succ (Pred b) :~: Succ (Pred b))
-> Reason (:~:) (Succ (Pred b)) b -> Succ (Pred b) :~: 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 n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
b' SNat b -> (Succ (Pred b) :~: b) -> Reason (:~:) (Succ (Pred b)) 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` (Pred b :~: n) -> Succ (Pred b) :~: Succ n
forall (n :: Nat) (m :: Nat). (n :~: m) -> S n :~: S m
succCong (SNat n -> Pred (Succ n) :~: n
forall (n :: Nat). SNat n -> Pred (Succ n) :~: n
predSucc SNat n
b')
          (Succ (Pred b) :~: b) -> SNat b -> Succ (Pred b) :~: b
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat b
b

cmpSucc :: SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc :: SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat n
n SNat m
m =
  case SNat n -> SNat m -> SOrdering (CmpNat n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n SNat m
m of
    SOrdering (CmpNat n m)
SEQ ->
      let nEQm :: n :~: m
nEQm = SNat n -> SNat m -> (CmpNat n m :~: 'EQ) -> n :~: m
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'EQ) -> a :~: b
eqToRefl SNat n
n SNat m
m CmpNat n m :~: 'EQ
forall k (a :: k). a :~: a
Refl
       in (CmpNat (Succ n) (Succ m) :~: 'EQ)
-> 'EQ :~: CmpNat (Succ n) (Succ m)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((CmpNat (Succ n) (Succ m) :~: 'EQ)
 -> 'EQ :~: CmpNat (Succ n) (Succ m))
-> (CmpNat (Succ n) (Succ m) :~: 'EQ)
-> 'EQ :~: CmpNat (Succ n) (Succ m)
forall a b. (a -> b) -> a -> b
$ SNat (Succ n)
-> SNat (Succ m)
-> (Succ n :~: Succ m)
-> CmpNat (Succ n) (Succ m) :~: 'EQ
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ
eqlCmpEQ (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) ((Succ n :~: Succ m) -> CmpNat (Succ n) (Succ m) :~: 'EQ)
-> (Succ n :~: Succ m) -> CmpNat (Succ n) (Succ m) :~: 'EQ
forall a b. (a -> b) -> a -> b
$ (n :~: m) -> Succ n :~: Succ m
forall (n :: Nat) (m :: Nat). (n :~: m) -> S n :~: S m
succCong n :~: m
nEQm
    SOrdering (CmpNat n m)
SLT -> case SNat (Succ n)
-> SNat m -> IsTrue (Succ n <=? m) -> DiffNat (Succ n) m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m (IsTrue (Succ n <=? m) -> DiffNat (Succ n) m)
-> IsTrue (Succ n <=? m) -> DiffNat (Succ n) m
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> IsTrue (Succ n <=? m)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)
ltToSuccLeq SNat n
n SNat m
m CmpNat n m :~: 'LT
forall k (a :: k). a :~: a
Refl of
      DiffNat SNat (Succ n)
_ SNat m
k ->
        (CmpNat (Succ n) (Succ m) :~: 'LT)
-> 'LT :~: CmpNat (Succ n) (Succ m)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((CmpNat (Succ n) (Succ m) :~: 'LT)
 -> 'LT :~: CmpNat (Succ n) (Succ m))
-> (CmpNat (Succ n) (Succ m) :~: 'LT)
-> 'LT :~: CmpNat (Succ n) (Succ m)
forall a b. (a -> b) -> a -> b
$
          SNat (Succ n)
-> SNat (Succ m)
-> IsTrue (S (Succ n) <=? Succ m)
-> CmpNat (Succ n) (Succ m) :~: 'LT
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT
succLeqToLT (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) (IsTrue (S (Succ n) <=? Succ m)
 -> CmpNat (Succ n) (Succ m) :~: 'LT)
-> IsTrue (S (Succ n) <=? Succ m)
-> CmpNat (Succ n) (Succ m) :~: 'LT
forall a b. (a -> b) -> a -> b
$
            SNat (S (Succ n))
-> SNat (Succ m)
-> SNat m
-> ((S (Succ n) + m) :~: Succ m)
-> IsTrue (S (Succ n) <=? Succ m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep (SNat (Succ n) -> SNat (S (Succ n))
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n)) (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) SNat m
k (((S (Succ n) + m) :~: Succ m) -> IsTrue (S (Succ n) <=? Succ m))
-> ((S (Succ n) + m) :~: Succ m) -> IsTrue (S (Succ n) <=? Succ m)
forall a b. (a -> b) -> a -> b
$
              SNat (S (Succ n) + m) -> (S (Succ n) + m) :~: (S (Succ n) + m)
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat (Succ n) -> SNat (S (Succ n))
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat (S (Succ n)) -> SNat m -> SNat (S (Succ n) + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k)
                ((S (Succ n) + m) :~: (S (Succ n) + m))
-> Reason (:~:) (S (Succ n) + m) (Succ m)
-> (S (Succ n) + m) :~: Succ 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 (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n SNat (Succ n) -> SNat m -> SNat (Succ n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat (Succ m)
-> ((S (Succ n) + m) :~: Succ m)
-> Reason (:~:) (S (Succ n) + m) (Succ 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 (Succ n) -> SNat m -> (S (Succ n) + m) :~: S (Succ n + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
k
                ((S (Succ n) + m) :~: Succ m)
-> SNat (Succ m) -> (S (Succ n) + m) :~: Succ 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 -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m
    SOrdering (CmpNat n m)
SGT -> case SNat (Succ m)
-> SNat n -> IsTrue (Succ m <=? n) -> DiffNat (Succ m) n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) SNat n
n (IsTrue (Succ m <=? n) -> DiffNat (Succ m) n)
-> IsTrue (Succ m <=? n) -> DiffNat (Succ m) n
forall a b. (a -> b) -> a -> b
$ SNat m -> SNat n -> (CmpNat m n :~: 'LT) -> IsTrue (Succ m <=? n)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)
ltToSuccLeq SNat m
m SNat n
n (('LT :~: CmpNat m n) -> CmpNat m n :~: 'LT
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (('LT :~: CmpNat m n) -> CmpNat m n :~: 'LT)
-> ('LT :~: CmpNat m n) -> CmpNat m n :~: 'LT
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> FlipOrdering (CmpNat n m) :~: CmpNat m n
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat SNat n
n SNat m
m) of
      DiffNat SNat (Succ m)
_ SNat m
k ->
        let pf :: CmpNat (Succ m) (Succ n) :~: 'LT
pf =
              ( SNat (Succ m)
-> SNat (Succ n)
-> IsTrue (S (Succ m) <=? Succ n)
-> CmpNat (Succ m) (Succ n) :~: 'LT
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT
succLeqToLT (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) (IsTrue (S (Succ m) <=? Succ n)
 -> CmpNat (Succ m) (Succ n) :~: 'LT)
-> IsTrue (S (Succ m) <=? Succ n)
-> CmpNat (Succ m) (Succ n) :~: 'LT
forall a b. (a -> b) -> a -> b
$
                  SNat (S (Succ m))
-> SNat (Succ n)
-> SNat m
-> ((S (Succ m) + m) :~: Succ n)
-> IsTrue (S (Succ m) <=? Succ n)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep (SNat (Succ m) -> SNat (S (Succ m))
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m)) (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
k (((S (Succ m) + m) :~: Succ n) -> IsTrue (S (Succ m) <=? Succ n))
-> ((S (Succ m) + m) :~: Succ n) -> IsTrue (S (Succ m) <=? Succ n)
forall a b. (a -> b) -> a -> b
$
                    SNat (S (Succ m) + m) -> (S (Succ m) + m) :~: (S (Succ m) + m)
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat (Succ m) -> SNat (S (Succ m))
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) SNat (S (Succ m)) -> SNat m -> SNat (S (Succ m) + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k)
                      ((S (Succ m) + m) :~: (S (Succ m) + m))
-> Reason (:~:) (S (Succ m) + m) (Succ n)
-> (S (Succ m) + m) :~: Succ 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 -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m SNat (Succ m) -> SNat m -> SNat (Succ m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat (Succ n)
-> ((S (Succ m) + m) :~: Succ n)
-> Reason (:~:) (S (Succ m) + m) (Succ 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 (Succ m) -> SNat m -> (S (Succ m) + m) :~: S (Succ m + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) SNat m
k
                      ((S (Succ m) + m) :~: Succ n)
-> SNat (Succ n) -> (S (Succ m) + m) :~: Succ 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 -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n
              )
         in SOrdering 'GT -> 'GT :~: 'GT
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 :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n SNat m
m)
              ('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 '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 (Succ m) (Succ n)))
-> 'GT :~: FlipOrdering (CmpNat (Succ m) (Succ 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
=== SOrdering (CmpNat (Succ m) (Succ n))
-> SOrdering (FlipOrdering (CmpNat (Succ m) (Succ n)))
forall (ord :: Ordering).
SOrdering ord -> SOrdering (FlipOrdering ord)
sFlipOrdering (SNat (Succ m)
-> SNat (Succ n) -> SOrdering (CmpNat (Succ m) (Succ n))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n)) SOrdering (FlipOrdering (CmpNat (Succ m) (Succ n)))
-> ('GT :~: FlipOrdering (CmpNat (Succ m) (Succ n)))
-> Reason (:~:) 'GT (FlipOrdering (CmpNat (Succ m) (Succ 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` ('LT :~: CmpNat (Succ m) (Succ n))
-> FlipOrdering 'LT :~: FlipOrdering (CmpNat (Succ m) (Succ n))
forall (a :: Ordering) (b :: Ordering).
(a :~: b) -> FlipOrdering a :~: FlipOrdering b
congFlipOrdering ((CmpNat (Succ m) (Succ n) :~: 'LT)
-> 'LT :~: CmpNat (Succ m) (Succ n)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym CmpNat (Succ m) (Succ n) :~: 'LT
pf)
              ('GT :~: FlipOrdering (CmpNat (Succ m) (Succ n)))
-> Reason
     (:~:)
     (FlipOrdering (CmpNat (Succ m) (Succ n)))
     (CmpNat (Succ n) (Succ m))
-> 'GT :~: CmpNat (Succ n) (Succ 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 (Succ n)
-> SNat (Succ m) -> SOrdering (CmpNat (Succ n) (Succ m))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) SOrdering (CmpNat (Succ n) (Succ m))
-> (FlipOrdering (CmpNat (Succ m) (Succ n))
    :~: CmpNat (Succ n) (Succ m))
-> Reason
     (:~:)
     (FlipOrdering (CmpNat (Succ m) (Succ n)))
     (CmpNat (Succ n) (Succ 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 (Succ m)
-> SNat (Succ n)
-> FlipOrdering (CmpNat (Succ m) (Succ n))
   :~: CmpNat (Succ n) (Succ m)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
flipCmpNat (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n)

ltSucc :: SNat a -> CmpNat a (Succ a) :~: 'LT
ltSucc :: SNat a -> CmpNat a (Succ a) :~: 'LT
ltSucc = LTSucc a -> CmpNat a (Succ a) :~: 'LT
forall (n :: Nat). LTSucc n -> CmpNat n (Succ n) :~: 'LT
proofLTSucc (LTSucc a -> CmpNat a (Succ a) :~: 'LT)
-> (SNat a -> LTSucc a) -> SNat a -> CmpNat a (Succ a) :~: 'LT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LTSucc 0
-> (forall (n :: Nat). SNat n -> LTSucc n -> LTSucc (S n))
-> SNat a
-> LTSucc a
forall (p :: Nat -> Type) (k :: Nat).
p 0
-> (forall (n :: Nat). SNat n -> p n -> p (S n)) -> SNat k -> p k
induction LTSucc 0
base forall (n :: Nat). SNat n -> LTSucc n -> LTSucc (S n)
step
  where
    base :: LTSucc 0
    base :: LTSucc 0
base = (CmpNat 0 (Succ 0) :~: 'LT) -> LTSucc 0
forall (n :: Nat). (CmpNat n (Succ n) :~: 'LT) -> LTSucc n
LTSucc ((CmpNat 0 (Succ 0) :~: 'LT) -> LTSucc 0)
-> (CmpNat 0 (Succ 0) :~: 'LT) -> LTSucc 0
forall a b. (a -> b) -> a -> b
$ SNat 0 -> CmpNat 0 (Succ 0) :~: 'LT
forall (a :: Nat). SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero (SNat 0
sZero :: SNat 0)

    step :: SNat n -> LTSucc n -> LTSucc (Succ n)
    step :: SNat n -> LTSucc n -> LTSucc (Succ n)
step SNat n
n (LTSucc CmpNat n (Succ n) :~: 'LT
ih) =
      (CmpNat (Succ n) (Succ (Succ n)) :~: 'LT) -> LTSucc (Succ n)
forall (n :: Nat). (CmpNat n (Succ n) :~: 'LT) -> LTSucc n
LTSucc ((CmpNat (Succ n) (Succ (Succ n)) :~: 'LT) -> LTSucc (Succ n))
-> (CmpNat (Succ n) (Succ (Succ n)) :~: 'LT) -> LTSucc (Succ n)
forall a b. (a -> b) -> a -> b
$
        SOrdering (CmpNat (Succ n) (Succ (Succ n)))
-> CmpNat (Succ n) (Succ (Succ n))
   :~: CmpNat (Succ n) (Succ (Succ n))
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat (Succ n)
-> SNat (Succ (Succ n))
-> SOrdering (CmpNat (Succ n) (Succ (Succ n)))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) (SNat (Succ n) -> SNat (Succ (Succ n))
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n)))
          (CmpNat (Succ n) (Succ (Succ n))
 :~: CmpNat (Succ n) (Succ (Succ n)))
-> Reason
     (:~:) (CmpNat (Succ n) (Succ (Succ n))) (CmpNat n (Succ n))
-> CmpNat (Succ n) (Succ (Succ n)) :~: CmpNat n (Succ 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 -> SNat (Succ n) -> SOrdering (CmpNat n (Succ n))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SOrdering (CmpNat n (Succ n))
-> (CmpNat (Succ n) (Succ (Succ n)) :~: CmpNat n (Succ n))
-> Reason
     (:~:) (CmpNat (Succ n) (Succ (Succ n))) (CmpNat n (Succ 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` (CmpNat n (Succ n) :~: CmpNat (Succ n) (Succ (Succ n)))
-> CmpNat (Succ n) (Succ (Succ n)) :~: CmpNat n (Succ n)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat n
-> SNat (Succ n)
-> CmpNat n (Succ n) :~: CmpNat (Succ n) (Succ (Succ n))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat n
n (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n))
          (CmpNat (Succ n) (Succ (Succ n)) :~: CmpNat n (Succ n))
-> Reason (:~:) (CmpNat n (Succ n)) 'LT
-> CmpNat (Succ n) (Succ (Succ n)) :~: '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 (Succ n) :~: 'LT)
-> Reason (:~:) (CmpNat n (Succ n)) '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 n (Succ n) :~: 'LT
ih

cmpSuccStepR ::
  SNat n ->
  SNat m ->
  CmpNat n m :~: 'LT ->
  CmpNat n (Succ m) :~: 'LT
cmpSuccStepR :: SNat n
-> SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
cmpSuccStepR = CmpSuccStepR n
-> SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
forall (n :: Nat).
CmpSuccStepR n
-> forall (m :: Nat).
   SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
proofCmpSuccStepR (CmpSuccStepR n
 -> SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT)
-> (SNat n -> CmpSuccStepR n)
-> SNat n
-> SNat m
-> (CmpNat n m :~: 'LT)
-> CmpNat n (Succ m) :~: 'LT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmpSuccStepR 0
-> (forall (n :: Nat).
    SNat n -> CmpSuccStepR n -> CmpSuccStepR (S n))
-> SNat n
-> CmpSuccStepR n
forall (p :: Nat -> Type) (k :: Nat).
p 0
-> (forall (n :: Nat). SNat n -> p n -> p (S n)) -> SNat k -> p k
induction CmpSuccStepR 0
base forall (n :: Nat). SNat n -> CmpSuccStepR n -> CmpSuccStepR (S n)
step
  where
    base :: CmpSuccStepR 0
    base :: CmpSuccStepR 0
base = (forall (m :: Nat).
 SNat m -> (CmpNat 0 m :~: 'LT) -> CmpNat 0 (Succ m) :~: 'LT)
-> CmpSuccStepR 0
forall (n :: Nat).
(forall (m :: Nat).
 SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT)
-> CmpSuccStepR n
CmpSuccStepR ((forall (m :: Nat).
  SNat m -> (CmpNat 0 m :~: 'LT) -> CmpNat 0 (Succ m) :~: 'LT)
 -> CmpSuccStepR 0)
-> (forall (m :: Nat).
    SNat m -> (CmpNat 0 m :~: 'LT) -> CmpNat 0 (Succ m) :~: 'LT)
-> CmpSuccStepR 0
forall a b. (a -> b) -> a -> b
$ \SNat m
m CmpNat 0 m :~: 'LT
_ -> SNat m -> CmpNat 0 (Succ m) :~: 'LT
forall (a :: Nat). SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero SNat m
m

    step :: SNat n -> CmpSuccStepR n -> CmpSuccStepR (Succ n)
    step :: SNat n -> CmpSuccStepR n -> CmpSuccStepR (Succ n)
step SNat n
n (CmpSuccStepR forall (m :: Nat).
SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
ih) = (forall (m :: Nat).
 SNat m
 -> (CmpNat (Succ n) m :~: 'LT) -> CmpNat (Succ n) (Succ m) :~: 'LT)
-> CmpSuccStepR (Succ n)
forall (n :: Nat).
(forall (m :: Nat).
 SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT)
-> CmpSuccStepR n
CmpSuccStepR ((forall (m :: Nat).
  SNat m
  -> (CmpNat (Succ n) m :~: 'LT) -> CmpNat (Succ n) (Succ m) :~: 'LT)
 -> CmpSuccStepR (Succ n))
-> (forall (m :: Nat).
    SNat m
    -> (CmpNat (Succ n) m :~: 'LT) -> CmpNat (Succ n) (Succ m) :~: 'LT)
-> CmpSuccStepR (Succ n)
forall a b. (a -> b) -> a -> b
$ \SNat m
m CmpNat (Succ n) m :~: 'LT
snltm ->
      case SNat m -> ZeroOrSucc m
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc SNat m
m of
        ZeroOrSucc m
IsZero -> Void -> CmpNat (Succ n) 1 :~: 'LT
forall a. Void -> a
absurd (Void -> CmpNat (Succ n) 1 :~: 'LT)
-> Void -> CmpNat (Succ n) 1 :~: 'LT
forall a b. (a -> b) -> a -> b
$ SNat (Succ n) -> (CmpNat (Succ n) 0 :~: 'LT) -> Void
forall (a :: Nat). SNat a -> (CmpNat a 0 :~: 'LT) -> Void
zeroNoLT (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) CmpNat (Succ n) m :~: 'LT
CmpNat (Succ n) 0 :~: 'LT
snltm
        IsSucc SNat n
m' ->
          let nLTm' :: CmpNat n n :~: 'LT
nLTm' = (CmpNat n n :~: CmpNat (Succ n) m)
-> (CmpNat (Succ n) m :~: 'LT) -> CmpNat n n :~: 'LT
forall k (a :: k) (b :: k) (c :: k).
(a :~: b) -> (b :~: c) -> a :~: c
trans (SNat n -> SNat n -> CmpNat n n :~: CmpNat (Succ n) (Succ n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat n
n SNat n
m') CmpNat (Succ n) m :~: 'LT
snltm
           in SOrdering (CmpNat (Succ n) (Succ m))
-> CmpNat (Succ n) (Succ m) :~: CmpNat (Succ n) (Succ m)
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat (Succ n)
-> SNat (Succ m) -> SOrdering (CmpNat (Succ n) (Succ m))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m))
                (CmpNat (Succ n) (Succ m) :~: CmpNat (Succ n) (Succ m))
-> SOrdering (CmpNat (Succ n) (Succ m))
-> CmpNat (Succ n) (Succ m) :~: CmpNat (Succ n) (Succ m)
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat (Succ n)
-> SNat (Succ m) -> SOrdering (CmpNat (Succ n) (Succ m))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
m'))
                (CmpNat (Succ n) (Succ m) :~: CmpNat (Succ n) (Succ m))
-> Reason (:~:) (CmpNat (Succ n) (Succ m)) (CmpNat n m)
-> CmpNat (Succ n) (Succ m) :~: CmpNat 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 -> SOrdering (CmpNat n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
m') SOrdering (CmpNat n m)
-> (CmpNat (Succ n) (Succ m) :~: CmpNat n m)
-> Reason (:~:) (CmpNat (Succ n) (Succ m)) (CmpNat 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` (CmpNat n m :~: CmpNat (Succ n) (Succ m))
-> CmpNat (Succ n) (Succ m) :~: CmpNat n m
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat n
n (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
m'))
                (CmpNat (Succ n) (Succ m) :~: CmpNat n m)
-> Reason (:~:) (CmpNat n m) 'LT
-> CmpNat (Succ n) (Succ 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 -> (CmpNat n n :~: 'LT) -> CmpNat n (Succ n) :~: 'LT
forall (m :: Nat).
SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
ih SNat n
m' CmpNat n n :~: 'LT
nLTm'

ltSuccLToLT ::
  SNat n ->
  SNat m ->
  CmpNat (Succ n) m :~: 'LT ->
  CmpNat n m :~: 'LT
ltSuccLToLT :: 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 :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc SNat m
m of
    ZeroOrSucc m
IsZero -> Void -> CmpNat n 0 :~: 'LT
forall a. Void -> a
absurd (Void -> CmpNat n 0 :~: 'LT) -> Void -> CmpNat n 0 :~: 'LT
forall a b. (a -> b) -> a -> b
$ SNat (Succ n) -> (CmpNat (Succ n) 0 :~: 'LT) -> Void
forall (a :: Nat). SNat a -> (CmpNat a 0 :~: 'LT) -> Void
zeroNoLT (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) CmpNat (Succ n) m :~: 'LT
CmpNat (Succ n) 0 :~: 'LT
snLTm
    IsSucc SNat n
m' ->
      let nLTm :: CmpNat n n :~: 'LT
nLTm = SNat n -> SNat n -> CmpNat n n :~: CmpNat (Succ n) (Succ n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat n
n SNat n
m' (CmpNat n n :~: CmpNat (Succ n) m)
-> (CmpNat (Succ n) m :~: 'LT) -> CmpNat n n :~: '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 :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
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 n -> (CmpNat n n :~: 'LT) -> CmpNat n (Succ n) :~: 'LT
forall (n :: Nat) (m :: Nat).
SNat n
-> SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
cmpSuccStepR SNat n
n SNat n
m' CmpNat n n :~: 'LT
nLTm

leqToLT ::
  SNat a ->
  SNat b ->
  IsTrue (Succ a <=? b) ->
  CmpNat a b :~: 'LT
leqToLT :: SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT
leqToLT SNat a
n SNat b
m IsTrue (Succ a <=? b)
snLEQm =
  case SNat (Succ a)
-> SNat b
-> IsTrue (Succ a <=? b)
-> Either (Succ a :~: b) (CmpNat (Succ a) b :~: 'LT)
forall (a :: Nat) (b :: Nat).
SNat a
-> SNat b
-> IsTrue (a <=? b)
-> Either (a :~: b) (CmpNat a b :~: 'LT)
leqToCmp (SNat a -> SNat (Succ a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
n) SNat b
m IsTrue (Succ a <=? b)
snLEQm of
    Left Succ a :~: b
eql ->
      (Succ a :~: b)
-> ((Succ a ~ b) => CmpNat a b :~: 'LT) -> CmpNat a b :~: 'LT
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
withRefl Succ a :~: b
eql (((Succ a ~ b) => CmpNat a b :~: 'LT) -> CmpNat a b :~: 'LT)
-> ((Succ a ~ b) => CmpNat a b :~: 'LT) -> CmpNat a b :~: 'LT
forall a b. (a -> b) -> a -> b
$
        SOrdering (CmpNat a b) -> CmpNat a b :~: CmpNat a b
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat a -> SNat b -> SOrdering (CmpNat a b)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
n SNat b
m)
          (CmpNat a b :~: CmpNat a b)
-> SOrdering (CmpNat a b) -> CmpNat a b :~: CmpNat a b
forall k1 k2 (r :: k1 -> k2 -> Type) (x :: k1) (y :: k2)
       (proxy :: k2 -> Type).
r x y -> proxy y -> r x y
=~= SNat a -> SNat b -> SOrdering (CmpNat a b)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat a
n (SNat a -> SNat (Succ a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
n)
          (CmpNat a b :~: CmpNat a b)
-> Reason (:~:) (CmpNat a b) 'LT -> CmpNat a b :~: '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 a b :~: 'LT) -> Reason (:~:) (CmpNat a b) '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 a -> CmpNat a (Succ a) :~: 'LT
forall (a :: Nat). SNat a -> CmpNat a (Succ a) :~: 'LT
ltSucc SNat a
n
    Right CmpNat (Succ a) b :~: 'LT
nLTm -> SNat a
-> SNat b -> (CmpNat (Succ a) b :~: 'LT) -> CmpNat a b :~: 'LT
forall (n :: Nat) (m :: Nat).
SNat n
-> SNat m -> (CmpNat (Succ n) m :~: 'LT) -> CmpNat n m :~: 'LT
ltSuccLToLT SNat a
n SNat b
m CmpNat (Succ a) b :~: 'LT
nLTm

leqZero :: SNat n -> IsTrue (0 <=? n)
leqZero :: SNat n -> IsTrue (0 <=? n)
leqZero SNat n
_ = IsTrue (0 <=? n)
IsTrue 'True
Witness

leqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m)
leqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m)
leqSucc SNat n
_ SNat m
_ IsTrue (n <=? m)
Witness = IsTrue (Succ n <=? Succ m)
IsTrue 'True
Witness

fromLeqView :: LeqView n m -> IsTrue (n <=? m)
fromLeqView :: LeqView n m -> IsTrue (n <=? m)
fromLeqView (LeqZero SNat m
n) = SNat m -> IsTrue (0 <=? m)
forall (n :: Nat). 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 (Succ n <=? Succ m)
forall (n :: Nat) (m :: Nat).
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 :: SNat n -> LeqView n n
leqViewRefl = LeqViewRefl n -> LeqView n n
forall (n :: Nat). 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 :: Nat).
    SNat n -> LeqViewRefl n -> LeqViewRefl (S n))
-> SNat n
-> LeqViewRefl n
forall (p :: Nat -> Type) (k :: Nat).
p 0
-> (forall (n :: Nat). SNat n -> p n -> p (S n)) -> SNat k -> p k
induction LeqViewRefl 0
base forall (n :: Nat). SNat n -> LeqViewRefl n -> LeqViewRefl (S n)
step
  where
    base :: LeqViewRefl 0
    base :: LeqViewRefl 0
base = LeqView 0 0 -> LeqViewRefl 0
forall (n :: Nat). 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 :: Nat). SNat n -> LeqView 0 n
LeqZero SNat 0
sZero
    step :: SNat n -> LeqViewRefl n -> LeqViewRefl (Succ n)
    step :: SNat n -> LeqViewRefl n -> LeqViewRefl (Succ n)
step SNat n
n (LeqViewRefl LeqView n n
nLEQn) =
      LeqView (Succ n) (Succ n) -> LeqViewRefl (Succ n)
forall (n :: Nat). 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 :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView (Succ n) (Succ m)
LeqSucc SNat n
n SNat n
n (LeqView n n -> IsTrue (n <=? n)
forall (n :: Nat) (m :: Nat). 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 :: 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 :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc SNat n
n, SNat n
-> SNat m
-> IsTrue (n <=? m)
-> Either (n :~: m) (CmpNat n m :~: 'LT)
forall (a :: Nat) (b :: Nat).
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 :: Nat). SNat n -> LeqView 0 n
LeqZero SNat m
m
    (ZeroOrSucc n
_, Left n :~: m
Refl) -> SNat n -> LeqView n n
forall (n :: Nat). SNat n -> LeqView n n
leqViewRefl SNat n
n
    (IsSucc SNat n
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 :: Nat) (b :: Nat).
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 :: Nat). SNat n -> SNat (Pred n)
sPred SNat m
m
          n'LTm' :: CmpNat n (Pred m) :~: 'LT
n'LTm' = SNat n
-> SNat (Pred m)
-> CmpNat n (Pred m) :~: CmpNat (Succ n) (Succ (Pred m))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
cmpSucc SNat n
n' SNat (Pred m)
m' (CmpNat n (Pred m) :~: CmpNat n (Succ (Pred m)))
-> (CmpNat n (Succ (Pred m)) :~: CmpNat n m)
-> CmpNat n (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 :: Nat) (b :: Nat) (c :: Nat).
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 n (Pred m) :~: CmpNat n m)
-> (CmpNat n m :~: 'LT) -> CmpNat n (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 n
-> SNat (Pred m)
-> IsTrue (n <=? Pred m)
-> LeqView (Succ n) (Succ (Pred m))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView (Succ n) (Succ m)
LeqSucc SNat n
n' SNat (Pred m)
m' (IsTrue (n <=? Pred m) -> LeqView (Succ n) (Succ (Pred m)))
-> IsTrue (n <=? Pred m) -> LeqView (Succ n) (Succ (Pred m))
forall a b. (a -> b) -> a -> b
$ SNat n
-> SNat (Pred m)
-> (CmpNat n (Pred m) :~: 'LT)
-> IsTrue (n <=? Pred m)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)
ltToLeq SNat n
n' SNat (Pred m)
m' CmpNat n (Pred m) :~: 'LT
n'LTm'

leqWitness :: SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness :: SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness = LeqWitPf n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
forall (n :: Nat).
LeqWitPf n
-> forall (m :: Nat). SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitPf (LeqWitPf n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m)
-> (SNat n -> LeqWitPf n)
-> SNat n
-> SNat m
-> IsTrue (n <=? m)
-> DiffNat n m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LeqWitPf 0
-> (forall (n :: Nat). SNat n -> LeqWitPf n -> LeqWitPf (S n))
-> SNat n
-> LeqWitPf n
forall (p :: Nat -> Type) (k :: Nat).
p 0
-> (forall (n :: Nat). SNat n -> p n -> p (S n)) -> SNat k -> p k
induction LeqWitPf 0
base forall (n :: Nat). SNat n -> LeqWitPf n -> LeqWitPf (S n)
step
  where
    base :: LeqWitPf 0
    base :: LeqWitPf 0
base = (forall (m :: Nat). SNat m -> IsTrue (0 <=? m) -> DiffNat 0 m)
-> LeqWitPf 0
forall (n :: Nat).
(forall (m :: Nat). SNat m -> IsTrue (n <=? m) -> DiffNat n m)
-> LeqWitPf n
LeqWitPf ((forall (m :: Nat). SNat m -> IsTrue (0 <=? m) -> DiffNat 0 m)
 -> LeqWitPf 0)
-> (forall (m :: Nat). 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 :: Nat). 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 :: Nat) (m :: Nat). SNat n -> SNat m -> DiffNat n (n + m)
DiffNat SNat 0
sZero SNat m
sm

    step :: SNat n -> LeqWitPf n -> LeqWitPf (Succ n)
    step :: SNat n -> LeqWitPf n -> LeqWitPf (Succ n)
step (SNat n
n :: SNat n) (LeqWitPf forall (m :: Nat). SNat m -> IsTrue (n <=? m) -> DiffNat n m
ih) = (forall (m :: Nat).
 SNat m -> IsTrue (Succ n <=? m) -> DiffNat (Succ n) m)
-> LeqWitPf (Succ n)
forall (n :: Nat).
(forall (m :: Nat). SNat m -> IsTrue (n <=? m) -> DiffNat n m)
-> LeqWitPf n
LeqWitPf ((forall (m :: Nat).
  SNat m -> IsTrue (Succ n <=? m) -> DiffNat (Succ n) m)
 -> LeqWitPf (Succ n))
-> (forall (m :: Nat).
    SNat m -> IsTrue (Succ n <=? m) -> DiffNat (Succ n) m)
-> LeqWitPf (Succ n)
forall a b. (a -> b) -> a -> b
$ \SNat m
m IsTrue (Succ n <=? m)
snLEQm ->
      case SNat (Succ n)
-> SNat m -> IsTrue (Succ n <=? m) -> LeqView (Succ n) m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView n m
viewLeq (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m IsTrue (Succ n <=? m)
snLEQm of
        LeqZero SNat m
_ -> Void -> DiffNat (Succ n) m
forall a. Void -> a
absurd (Void -> DiffNat (Succ n) m) -> Void -> DiffNat (Succ n) m
forall a b. (a -> b) -> a -> b
$ SNat n -> (Succ n :~: 0) -> Void
forall (n :: Nat). SNat n -> (Succ n :~: 0) -> Void
succNonCyclic SNat n
n Succ n :~: 0
forall k (a :: k). a :~: a
Refl
        LeqSucc (SNat n
_ :: SNat n') SNat m
pm IsTrue (n <=? m)
nLEQpm ->
          SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m)
succDiffNat SNat n
n SNat m
pm (DiffNat n m -> DiffNat (Succ n) (Succ m))
-> DiffNat n m -> DiffNat (Succ n) (Succ m)
forall a b. (a -> b) -> a -> b
$ SNat m -> IsTrue (n <=? m) -> DiffNat n m
forall (m :: Nat). SNat m -> IsTrue (n <=? m) -> DiffNat n m
ih SNat m
pm (IsTrue (n <=? m) -> DiffNat n m)
-> IsTrue (n <=? m) -> DiffNat n m
forall a b. (a -> b) -> a -> b
$ (n :~: n) -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
(n :~: m) -> SNat l -> IsTrue (n <=? l) -> IsTrue (m <=? l)
coerceLeqL ((Succ n :~: Succ n) -> n :~: n
forall (n :: Nat) (m :: Nat). (Succ n :~: Succ m) -> n :~: m
succInj Succ n :~: Succ n
forall k (a :: k). a :~: a
Refl :: n' :~: n) SNat m
pm IsTrue (n <=? m)
nLEQpm

leqStep :: SNat n -> SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m)
leqStep :: SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep = LeqStepPf n
-> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
forall (n :: Nat).
LeqStepPf n
-> forall (m :: Nat) (l :: Nat).
   SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStepPf (LeqStepPf n
 -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m))
-> (SNat n -> LeqStepPf n)
-> SNat n
-> SNat m
-> SNat l
-> ((n + l) :~: m)
-> IsTrue (n <=? m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LeqStepPf 0
-> (forall (n :: Nat). SNat n -> LeqStepPf n -> LeqStepPf (S n))
-> SNat n
-> LeqStepPf n
forall (p :: Nat -> Type) (k :: Nat).
p 0
-> (forall (n :: Nat). SNat n -> p n -> p (S n)) -> SNat k -> p k
induction LeqStepPf 0
base forall (n :: Nat). SNat n -> LeqStepPf n -> LeqStepPf (S n)
step
  where
    base :: LeqStepPf 0
    base :: LeqStepPf 0
base = (forall (m :: Nat) (l :: Nat).
 SNat m -> SNat l -> ((0 + l) :~: m) -> IsTrue (0 <=? m))
-> LeqStepPf 0
forall (n :: Nat).
(forall (m :: Nat) (l :: Nat).
 SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m))
-> LeqStepPf n
LeqStepPf ((forall (m :: Nat) (l :: Nat).
  SNat m -> SNat l -> ((0 + l) :~: m) -> IsTrue (0 <=? m))
 -> LeqStepPf 0)
-> (forall (m :: Nat) (l :: Nat).
    SNat m -> SNat l -> ((0 + l) :~: m) -> IsTrue (0 <=? m))
-> LeqStepPf 0
forall a b. (a -> b) -> a -> b
$ \SNat m
k SNat l
_ (0 + l) :~: m
_ -> SNat m -> IsTrue (0 <=? m)
forall (n :: Nat). SNat n -> IsTrue (0 <=? n)
leqZero SNat m
k

    step :: SNat n -> LeqStepPf n -> LeqStepPf (Succ n)
    step :: SNat n -> LeqStepPf n -> LeqStepPf (Succ n)
step SNat n
n (LeqStepPf forall (m :: Nat) (l :: Nat).
SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
ih) =
      (forall (m :: Nat) (l :: Nat).
 SNat m -> SNat l -> ((Succ n + l) :~: m) -> IsTrue (Succ n <=? m))
-> LeqStepPf (Succ n)
forall (n :: Nat).
(forall (m :: Nat) (l :: Nat).
 SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m))
-> LeqStepPf n
LeqStepPf ((forall (m :: Nat) (l :: Nat).
  SNat m -> SNat l -> ((Succ n + l) :~: m) -> IsTrue (Succ n <=? m))
 -> LeqStepPf (Succ n))
-> (forall (m :: Nat) (l :: Nat).
    SNat m -> SNat l -> ((Succ n + l) :~: m) -> IsTrue (Succ n <=? m))
-> LeqStepPf (Succ n)
forall a b. (a -> b) -> a -> b
$ \SNat m
k SNat l
l (Succ n + l) :~: m
snPlEqk ->
        let kEQspk :: m :~: ((n + l) + 1)
kEQspk =
              SNat m -> m :~: m
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start SNat m
k
                (m :~: m) -> Reason (:~:) m (Succ n + l) -> m :~: (Succ n + l)
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 (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n SNat (Succ n) -> SNat l -> SNat (Succ n + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l SNat (Succ n + l)
-> (m :~: (Succ n + l)) -> Reason (:~:) m (Succ n + l)
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 + l) :~: m) -> m :~: (Succ n + l)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (Succ n + l) :~: m
snPlEqk
                (m :~: (Succ n + l))
-> Reason (:~:) (Succ n + l) ((n + l) + 1) -> m :~: ((n + l) + 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 + l) -> SNat ((n + l) + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n
n SNat n -> SNat l -> SNat (n + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l) SNat ((n + l) + 1)
-> ((Succ n + l) :~: ((n + l) + 1))
-> Reason (:~:) (Succ n + l) ((n + l) + 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 l -> (Succ n + l) :~: ((n + l) + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat n
n SNat l
l
            pk :: SNat (n + l)
pk = SNat n
n SNat n -> SNat l -> SNat (n + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l
         in SNat (Succ n)
-> (((n + l) + 1) :~: m)
-> IsTrue (Succ n <=? ((n + l) + 1))
-> IsTrue (Succ n <=? m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat l -> (n :~: m) -> IsTrue (l <=? n) -> IsTrue (l <=? m)
coerceLeqR (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) ((m :~: ((n + l) + 1)) -> ((n + l) + 1) :~: m
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym m :~: ((n + l) + 1)
kEQspk) (IsTrue (Succ n <=? ((n + l) + 1)) -> IsTrue (Succ n <=? m))
-> IsTrue (Succ n <=? ((n + l) + 1)) -> IsTrue (Succ n <=? m)
forall a b. (a -> b) -> a -> b
$ SNat n
-> SNat (n + l)
-> IsTrue (n <=? (n + l))
-> IsTrue (Succ n <=? ((n + l) + 1))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m)
leqSucc SNat n
n SNat (n + l)
pk (IsTrue (n <=? (n + l)) -> IsTrue (Succ n <=? ((n + l) + 1)))
-> IsTrue (n <=? (n + l)) -> IsTrue (Succ n <=? ((n + l) + 1))
forall a b. (a -> b) -> a -> b
$ SNat (n + l)
-> SNat l -> ((n + l) :~: (n + l)) -> IsTrue (n <=? (n + l))
forall (m :: Nat) (l :: Nat).
SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
ih SNat (n + l)
pk SNat l
l (n + l) :~: (n + l)
forall k (a :: k). a :~: a
Refl

leqNeqToSuccLeq :: SNat n -> SNat m -> IsTrue (n <=? m) -> (n :~: m -> Void) -> IsTrue (Succ n <=? m)
leqNeqToSuccLeq :: 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 :: Nat) (m :: Nat).
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 :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc SNat m
k of
        ZeroOrSucc m
IsZero -> Void -> IsTrue (Succ n <=? n)
forall a. Void -> a
absurd (Void -> IsTrue (Succ n <=? n)) -> Void -> IsTrue (Succ n <=? n)
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 :: Nat). SNat n -> (n + 0) :~: n
plusZeroR SNat n
n
        IsSucc SNat n
k' ->
          SNat (Succ n)
-> SNat m
-> SNat n
-> ((Succ n + n) :~: m)
-> IsTrue (Succ n <=? m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m SNat n
k' (((Succ n + n) :~: m) -> IsTrue (Succ n <=? m))
-> ((Succ n + n) :~: m) -> IsTrue (Succ n <=? m)
forall a b. (a -> b) -> a -> b
$
            SNat (Succ n + n) -> (Succ n + n) :~: (Succ n + n)
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 :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n SNat (Succ n) -> SNat n -> SNat (Succ n + n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat n
k')
              ((Succ n + n) :~: (Succ n + n))
-> Reason (:~:) (Succ n + n) ((n + n) + 1)
-> (Succ n + n) :~: ((n + n) + 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 + n) -> SNat ((n + n) + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n
n SNat n -> SNat n -> SNat (n + n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat n
k') SNat ((n + n) + 1)
-> ((Succ n + n) :~: ((n + n) + 1))
-> Reason (:~:) (Succ n + n) ((n + n) + 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 n -> (Succ n + n) :~: ((n + n) + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat n
n SNat n
k'
              ((Succ n + n) :~: ((n + n) + 1))
-> Reason (:~:) ((n + n) + 1) m -> (Succ 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
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
k' SNat m -> (((n + n) + 1) :~: m) -> Reason (:~:) ((n + n) + 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 + n) + 1)) -> ((n + n) + 1) :~: m
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat n -> SNat n -> (n + Succ n) :~: ((n + n) + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + S m) :~: S (n + m)
plusSuccR SNat n
n SNat n
k')
              ((Succ n + n) :~: m) -> SNat m -> (Succ 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 m
m

leqRefl :: SNat n -> IsTrue (n <=? n)
leqRefl :: SNat n -> IsTrue (n <=? n)
leqRefl SNat n
sn = SNat n -> SNat n -> SNat 0 -> ((n + 0) :~: n) -> IsTrue (n <=? n)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep SNat n
sn SNat n
sn SNat 0
sZero (SNat n -> (n + 0) :~: n
forall (n :: Nat). SNat n -> (n + 0) :~: n
plusZeroR SNat n
sn)

leqSuccStepR :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)
leqSuccStepR :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)
leqSuccStepR SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm =
  case SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
forall (n :: Nat) (m :: Nat).
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 ->
      SNat n
-> SNat (Succ m)
-> SNat (m + 1)
-> ((n + (m + 1)) :~: Succ m)
-> IsTrue (n <=? Succ m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep SNat n
n (SNat m -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m) (SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k) (((n + (m + 1)) :~: Succ m) -> IsTrue (n <=? Succ m))
-> ((n + (m + 1)) :~: Succ m) -> IsTrue (n <=? Succ m)
forall a b. (a -> b) -> a -> b
$
        SNat (n + (m + 1)) -> (n + (m + 1)) :~: (n + (m + 1))
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 + 1) -> SNat (n + (m + 1))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k) ((n + (m + 1)) :~: (n + (m + 1)))
-> Reason (:~:) (n + (m + 1)) (Succ m) -> (n + (m + 1)) :~: Succ 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 (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat (Succ m)
-> ((n + (m + 1)) :~: Succ m)
-> Reason (:~:) (n + (m + 1)) (Succ 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 -> (n + (m + 1)) :~: S (n + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + S m) :~: S (n + m)
plusSuccR SNat n
n SNat m
k ((n + (m + 1)) :~: Succ m)
-> SNat (Succ m) -> (n + (m + 1)) :~: Succ 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 -> SNat (Succ m)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
m

leqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m)
leqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m)
leqSuccStepL SNat n
n SNat m
m IsTrue (Succ n <=? m)
snLEQm =
  SNat n
-> SNat (Succ n)
-> SNat m
-> IsTrue (n <=? Succ n)
-> IsTrue (Succ n <=? m)
-> IsTrue (n <=? m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (m <=? l)
-> IsTrue (n <=? l)
leqTrans SNat n
n (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m (SNat n -> SNat n -> IsTrue (n <=? n) -> IsTrue (n <=? Succ n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)
leqSuccStepR SNat n
n SNat n
n (IsTrue (n <=? n) -> IsTrue (n <=? Succ n))
-> IsTrue (n <=? n) -> IsTrue (n <=? Succ n)
forall a b. (a -> b) -> a -> b
$ SNat n -> IsTrue (n <=? n)
forall (n :: Nat). SNat n -> IsTrue (n <=? n)
leqRefl SNat n
n) IsTrue (Succ n <=? m)
snLEQm

leqReflexive :: SNat n -> SNat m -> n :~: m -> IsTrue (n <=? m)
leqReflexive :: SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive SNat n
n SNat m
_ n :~: m
Refl = SNat n -> IsTrue (n <=? n)
forall (n :: Nat). SNat n -> IsTrue (n <=? n)
leqRefl SNat n
n

leqTrans :: 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)
-> IsTrue (m <=? l)
-> IsTrue (n <=? l)
leqTrans SNat n
n SNat m
m SNat l
k IsTrue (n <=? m)
nLEm IsTrue (m <=? l)
mLEk =
  case SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat n
n SNat m
m IsTrue (n <=? m)
nLEm of
    DiffNat SNat n
_ SNat m
mMn -> case SNat m -> SNat l -> IsTrue (m <=? l) -> DiffNat m l
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat m
m SNat l
k IsTrue (m <=? l)
mLEk of
      DiffNat SNat m
_ SNat m
kMn -> SNat n
-> SNat l
-> SNat (m + m)
-> ((n + (m + m)) :~: l)
-> IsTrue (n <=? l)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep SNat n
n SNat l
k (SNat m
mMn SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
kMn) ((l :~: (n + (m + m))) -> (n + (m + m)) :~: l
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((l :~: (n + (m + m))) -> (n + (m + m)) :~: l)
-> (l :~: (n + (m + m))) -> (n + (m + m)) :~: l
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> SNat m -> ((n + m) + m) :~: (n + (m + m))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) + l) :~: (n + (m + l))
plusAssoc SNat n
n SNat m
mMn SNat m
kMn)

leqAntisymm :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m
leqAntisymm :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m
leqAntisymm SNat n
n SNat m
m IsTrue (n <=? m)
nLEm IsTrue (m <=? n)
mLEn =
  case (SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat n
n SNat m
m IsTrue (n <=? m)
nLEm, SNat m -> SNat n -> IsTrue (m <=? n) -> DiffNat m n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat m
m SNat n
n IsTrue (m <=? n)
mLEn) of
    (DiffNat SNat n
_ SNat m
mMn, DiffNat SNat m
_ SNat m
nMm) ->
      let pEQ0 :: (m + m) :~: 0
pEQ0 =
            SNat n
-> SNat (m + m)
-> SNat 0
-> ((n + (m + m)) :~: (n + 0))
-> (m + m) :~: 0
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) :~: (n + l)) -> m :~: l
plusEqCancelL SNat n
n (SNat m
mMn SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
nMm) SNat 0
sZero (((n + (m + m)) :~: (n + 0)) -> (m + m) :~: 0)
-> ((n + (m + m)) :~: (n + 0)) -> (m + m) :~: 0
forall a b. (a -> b) -> a -> b
$
              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 + m) -> SNat (n + (m + m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat m
mMn SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
nMm))
                ((n + (m + m)) :~: (n + (m + m)))
-> Reason (:~:) (n + (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 n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
mMn) SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
nMm
                  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` (n :~: (n + (m + m))) -> (n + (m + m)) :~: n
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat n -> SNat m -> SNat m -> ((n + m) + m) :~: (n + (m + m))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) + l) :~: (n + (m + l))
plusAssoc SNat n
n SNat m
mMn SNat m
nMm)
                ((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 m
m SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
nMm
                ((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
                ((n + (m + m)) :~: n) -> Reason (:~:) n 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 n
n SNat n -> SNat 0 -> SNat (n + 0)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat 0
sZero
                  SNat n -> (n :~: n) -> Reason (:~:) 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` (n :~: n) -> n :~: n
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat n -> (n + 0) :~: n
forall (n :: Nat). SNat n -> (n + 0) :~: n
plusZeroR SNat n
n)
          nMmEQ0 :: m :~: 0
nMmEQ0 = SNat m -> SNat m -> ((m + m) :~: 0) -> m :~: 0
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> ((n + m) :~: 0) -> n :~: 0
plusEqZeroL SNat m
mMn SNat m
nMm (m + m) :~: 0
pEQ0
       in (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 m -> m :~: m
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start SNat m
m
              (m :~: m) -> SNat m -> 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 n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
mMn
              (m :~: m) -> Reason (:~:) 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 -> SNat 0 -> SNat (n + 0)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat 0
sZero SNat n -> (m :~: n) -> Reason (:~:) 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 -> (m :~: 0) -> (n + m) :~: (n + 0)
forall (k :: Nat) (n :: Nat) (m :: Nat).
SNat k -> (n :~: m) -> (k + n) :~: (k + m)
plusCongR SNat n
n m :~: 0
nMmEQ0
              (m :~: n) -> Reason (:~:) 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 -> (n :~: n) -> Reason (:~:) 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 -> (n + 0) :~: n
forall (n :: Nat). SNat n -> (n + 0) :~: n
plusZeroR SNat n
n

plusMonotone ::
  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)
-> IsTrue (l <=? k)
-> IsTrue ((n + l) <=? (m + k))
plusMonotone SNat n
n SNat m
m SNat l
l SNat k
k IsTrue (n <=? m)
nLEm IsTrue (l <=? k)
lLEk =
  case (SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat n
n SNat m
m IsTrue (n <=? m)
nLEm, SNat l -> SNat k -> IsTrue (l <=? k) -> DiffNat l k
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness SNat l
l SNat k
k IsTrue (l <=? k)
lLEk) of
    (DiffNat SNat n
_ SNat m
mMINn, DiffNat SNat l
_ SNat m
kMINl) ->
      let r :: SNat (m + m)
r = SNat m
mMINn SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
kMINl
       in SNat (n + l)
-> SNat (m + k)
-> SNat (m + m)
-> (((n + l) + (m + m)) :~: (m + k))
-> IsTrue ((n + l) <=? (m + k))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep (SNat n
n SNat n -> SNat l -> SNat (n + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l) (SNat m
m SNat m -> SNat k -> SNat (m + k)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat k
k) SNat (m + m)
r ((((n + l) + (m + m)) :~: (m + k)) -> IsTrue ((n + l) <=? (m + k)))
-> (((n + l) + (m + m)) :~: (m + k))
-> IsTrue ((n + l) <=? (m + k))
forall a b. (a -> b) -> a -> b
$
            SNat ((n + l) + (m + m))
-> ((n + l) + (m + m)) :~: ((n + l) + (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 l -> SNat (n + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l SNat (n + l) -> SNat (m + m) -> SNat ((n + l) + (m + m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat (m + m)
r)
              (((n + l) + (m + m)) :~: ((n + l) + (m + m)))
-> Reason (:~:) ((n + l) + (m + m)) (n + (l + (m + m)))
-> ((n + l) + (m + m)) :~: (n + (l + (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 (l + (m + m)) -> SNat (n + (l + (m + m)))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat l
l SNat l -> SNat (m + m) -> SNat (l + (m + m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat (m + m)
r)
                SNat (n + (l + (m + m)))
-> (((n + l) + (m + m)) :~: (n + (l + (m + m))))
-> Reason (:~:) ((n + l) + (m + m)) (n + (l + (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 l
-> SNat (m + m)
-> ((n + l) + (m + m)) :~: (n + (l + (m + m)))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) + l) :~: (n + (m + l))
plusAssoc SNat n
n SNat l
l SNat (m + m)
r
              (((n + l) + (m + m)) :~: (n + (l + (m + m))))
-> SNat (n + (l + (m + m)))
-> ((n + l) + (m + m)) :~: (n + (l + (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 n
n SNat n -> SNat (l + (m + m)) -> SNat (n + (l + (m + m)))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat l
l SNat l -> SNat (m + m) -> SNat (l + (m + m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat m
mMINn SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
kMINl))
              (((n + l) + (m + m)) :~: (n + (l + (m + m))))
-> Reason (:~:) (n + (l + (m + m))) (n + (l + (m + m)))
-> ((n + l) + (m + m)) :~: (n + (l + (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 (l + (m + m)) -> SNat (n + (l + (m + m)))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat l
l SNat l -> SNat (m + m) -> SNat (l + (m + m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat m
kMINl SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
mMINn))
                SNat (n + (l + (m + m)))
-> ((n + (l + (m + m))) :~: (n + (l + (m + m))))
-> Reason (:~:) (n + (l + (m + m))) (n + (l + (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
-> ((l + (m + m)) :~: (l + (m + m)))
-> (n + (l + (m + m))) :~: (n + (l + (m + m)))
forall (k :: Nat) (n :: Nat) (m :: Nat).
SNat k -> (n :~: m) -> (k + n) :~: (k + m)
plusCongR SNat n
n (SNat l -> ((m + m) :~: (m + m)) -> (l + (m + m)) :~: (l + (m + m))
forall (k :: Nat) (n :: Nat) (m :: Nat).
SNat k -> (n :~: m) -> (k + n) :~: (k + m)
plusCongR SNat l
l (SNat m -> SNat m -> (m + m) :~: (m + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
mMINn SNat m
kMINl))
              (((n + l) + (m + m)) :~: (n + (l + (m + m))))
-> Reason (:~:) (n + (l + (m + m))) (n + (k + m))
-> ((n + l) + (m + m)) :~: (n + (k + 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 (k + m) -> SNat (n + (k + m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ ((SNat l
l SNat l -> SNat m -> SNat (l + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
kMINl) SNat k -> SNat m -> SNat (k + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
mMINn)
                SNat (n + (k + m))
-> ((n + (l + (m + m))) :~: (n + (k + m)))
-> Reason (:~:) (n + (l + (m + m))) (n + (k + 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
-> ((l + (m + m)) :~: (k + m))
-> (n + (l + (m + m))) :~: (n + (k + m))
forall (k :: Nat) (n :: Nat) (m :: Nat).
SNat k -> (n :~: m) -> (k + n) :~: (k + m)
plusCongR SNat n
n (((k + m) :~: (l + (m + m))) -> (l + (m + m)) :~: (k + m)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (((k + m) :~: (l + (m + m))) -> (l + (m + m)) :~: (k + m))
-> ((k + m) :~: (l + (m + m))) -> (l + (m + m)) :~: (k + m)
forall a b. (a -> b) -> a -> b
$ SNat l -> SNat m -> SNat m -> ((l + m) + m) :~: (l + (m + m))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) + l) :~: (n + (m + l))
plusAssoc SNat l
l SNat m
kMINl SNat m
mMINn)
              (((n + l) + (m + m)) :~: (n + (k + m)))
-> SNat (n + (k + m)) -> ((n + l) + (m + m)) :~: (n + (k + 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
n SNat n -> SNat (k + m) -> SNat (n + (k + m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat k
k SNat k -> SNat m -> SNat (k + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
mMINn)
              (((n + l) + (m + m)) :~: (n + (k + m)))
-> Reason (:~:) (n + (k + m)) (n + (m + k))
-> ((n + l) + (m + m)) :~: (n + (m + k))
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 + k) -> SNat (n + (m + k))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat m
mMINn SNat m -> SNat k -> SNat (m + k)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat k
k)
                SNat (n + (m + k))
-> ((n + (k + m)) :~: (n + (m + k)))
-> Reason (:~:) (n + (k + m)) (n + (m + k))
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 -> ((k + m) :~: (m + k)) -> (n + (k + m)) :~: (n + (m + k))
forall (k :: Nat) (n :: Nat) (m :: Nat).
SNat k -> (n :~: m) -> (k + n) :~: (k + m)
plusCongR SNat n
n (SNat k -> SNat m -> (k + m) :~: (m + k)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat k
k SNat m
mMINn)
              (((n + l) + (m + m)) :~: (n + (m + k)))
-> Reason (:~:) (n + (m + k)) (m + k)
-> ((n + l) + (m + m)) :~: (m + k)
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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
mMINn SNat m -> SNat k -> SNat (m + k)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat k
k
                SNat (m + k)
-> ((n + (m + k)) :~: (m + k))
-> Reason (:~:) (n + (m + k)) (m + k)
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 + k) :~: (n + (m + k))) -> (n + (m + k)) :~: (m + k)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat n -> SNat m -> SNat k -> ((n + m) + k) :~: (n + (m + k))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) + l) :~: (n + (m + l))
plusAssoc SNat n
n SNat m
mMINn SNat k
k)
              (((n + l) + (m + m)) :~: (m + k))
-> SNat (m + k) -> ((n + l) + (m + m)) :~: (m + k)
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 k -> SNat (m + k)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat k
k

leqZeroElim :: SNat n -> IsTrue (n <=? 0) -> n :~: 0
leqZeroElim :: SNat n -> IsTrue (n <=? 0) -> n :~: 0
leqZeroElim SNat n
n IsTrue (n <=? 0)
nLE0 =
  case SNat n -> SNat 0 -> IsTrue (n <=? 0) -> LeqView n 0
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView n m
viewLeq SNat n
n SNat 0
sZero IsTrue (n <=? 0)
nLE0 of
    LeqZero SNat 0
_ -> n :~: 0
forall k (a :: k). a :~: a
Refl
    LeqSucc SNat n
_ SNat m
pZ IsTrue (n <=? m)
_ -> Void -> n :~: 0
forall a. Void -> a
absurd (Void -> n :~: 0) -> Void -> n :~: 0
forall a b. (a -> b) -> a -> b
$ SNat m -> (Succ m :~: 0) -> Void
forall (n :: Nat). SNat n -> (Succ n :~: 0) -> Void
succNonCyclic SNat m
pZ Succ m :~: 0
forall k (a :: k). a :~: a
Refl

plusMonotoneL ::
  SNat n ->
  SNat m ->
  SNat l ->
  IsTrue (n <=? m) ->
  IsTrue ((n + l) <=? (m + l))
plusMonotoneL :: SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue ((n + l) <=? (m + l))
plusMonotoneL SNat n
n SNat m
m SNat l
l IsTrue (n <=? m)
leq = SNat n
-> SNat m
-> SNat l
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (l <=? l)
-> IsTrue ((n + l) <=? (m + l))
forall (n :: Nat) (m :: Nat) (l :: Nat) (k :: Nat).
SNat n
-> SNat m
-> SNat l
-> SNat k
-> IsTrue (n <=? m)
-> IsTrue (l <=? k)
-> IsTrue ((n + l) <=? (m + k))
plusMonotone SNat n
n SNat m
m SNat l
l SNat l
l IsTrue (n <=? m)
leq (SNat l -> IsTrue (l <=? l)
forall (n :: Nat). SNat n -> IsTrue (n <=? n)
leqRefl SNat l
l)

plusMonotoneR ::
  SNat n ->
  SNat m ->
  SNat l ->
  IsTrue (m <=? l) ->
  IsTrue ((n + m) <=? (n + l))
plusMonotoneR :: SNat n
-> SNat m
-> SNat l
-> IsTrue (m <=? l)
-> IsTrue ((n + m) <=? (n + l))
plusMonotoneR SNat n
n SNat m
m SNat l
l IsTrue (m <=? l)
leq = SNat n
-> SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? n)
-> IsTrue (m <=? l)
-> IsTrue ((n + m) <=? (n + l))
forall (n :: Nat) (m :: Nat) (l :: Nat) (k :: Nat).
SNat n
-> SNat m
-> SNat l
-> SNat k
-> IsTrue (n <=? m)
-> IsTrue (l <=? k)
-> IsTrue ((n + l) <=? (m + k))
plusMonotone SNat n
n SNat n
n SNat m
m SNat l
l (SNat n -> IsTrue (n <=? n)
forall (n :: Nat). SNat n -> IsTrue (n <=? n)
leqRefl SNat n
n) IsTrue (m <=? l)
leq

plusLeqL :: SNat n -> SNat m -> IsTrue (n <=? (n + m))
plusLeqL :: SNat n -> SNat m -> IsTrue (n <=? (n + m))
plusLeqL SNat n
n SNat m
m = SNat n
-> SNat (n + m)
-> SNat m
-> ((n + m) :~: (n + m))
-> IsTrue (n <=? (n + m))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep SNat n
n (SNat n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m) SNat m
m (n + m) :~: (n + m)
forall k (a :: k). a :~: a
Refl

plusLeqR :: SNat n -> SNat m -> IsTrue (m <=? (n + m))
plusLeqR :: SNat n -> SNat m -> IsTrue (m <=? (n + m))
plusLeqR SNat n
n SNat m
m = SNat m
-> SNat (n + m)
-> SNat n
-> ((m + n) :~: (n + m))
-> IsTrue (m <=? (n + m))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep SNat m
m (SNat n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m) SNat n
n (((m + n) :~: (n + m)) -> IsTrue (m <=? (n + m)))
-> ((m + n) :~: (n + m)) -> IsTrue (m <=? (n + m))
forall a b. (a -> b) -> a -> b
$ SNat m -> SNat n -> (m + n) :~: (n + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
m SNat n
n

plusCancelLeqR ::
  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))
-> IsTrue (n <=? m)
plusCancelLeqR SNat n
n SNat m
m SNat l
l IsTrue ((n + l) <=? (m + l))
nlLEQml =
  case SNat (n + l)
-> SNat (m + l)
-> IsTrue ((n + l) <=? (m + l))
-> DiffNat (n + l) (m + l)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
leqWitness (SNat n
n SNat n -> SNat l -> SNat (n + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l) (SNat m
m SNat m -> SNat l -> SNat (m + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l) IsTrue ((n + l) <=? (m + l))
nlLEQml of
    DiffNat SNat (n + l)
_ SNat m
k ->
      let pf :: (n + m) :~: m
pf =
            SNat (n + m)
-> SNat m -> SNat l -> (((n + m) + l) :~: (m + l)) -> (n + m) :~: m
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: (m + l)) -> n :~: m
plusEqCancelR (SNat n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat m
m SNat l
l ((((n + m) + l) :~: (m + l)) -> (n + m) :~: m)
-> (((n + m) + l) :~: (m + l)) -> (n + m) :~: m
forall a b. (a -> b) -> a -> b
$
              SNat ((n + m) + l) -> ((n + m) + l) :~: ((n + m) + l)
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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat (n + m) -> SNat l -> SNat ((n + m) + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l)
                (((n + m) + l) :~: ((n + m) + l))
-> Reason (:~:) ((n + m) + l) (n + (m + l))
-> ((n + m) + l) :~: (n + (m + l))
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 + l) -> SNat (n + (m + l))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat m
k SNat m -> SNat l -> SNat (m + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l) SNat (n + (m + l))
-> (((n + m) + l) :~: (n + (m + l)))
-> Reason (:~:) ((n + m) + l) (n + (m + l))
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 -> SNat l -> ((n + m) + l) :~: (n + (m + l))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) + l) :~: (n + (m + l))
plusAssoc SNat n
n SNat m
k SNat l
l
                (((n + m) + l) :~: (n + (m + l)))
-> Reason (:~:) (n + (m + l)) (n + (l + m))
-> ((n + m) + l) :~: (n + (l + 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 (l + m) -> SNat (n + (l + m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat l
l SNat l -> SNat m -> SNat (l + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat (n + (l + m))
-> ((n + (m + l)) :~: (n + (l + m)))
-> Reason (:~:) (n + (m + l)) (n + (l + 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 -> ((m + l) :~: (l + m)) -> (n + (m + l)) :~: (n + (l + m))
forall (k :: Nat) (n :: Nat) (m :: Nat).
SNat k -> (n :~: m) -> (k + n) :~: (k + m)
plusCongR SNat n
n (SNat m -> SNat l -> (m + l) :~: (l + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
k SNat l
l)
                (((n + m) + l) :~: (n + (l + m)))
-> Reason (:~:) (n + (l + m)) ((n + l) + m)
-> ((n + m) + l) :~: ((n + l) + 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 l -> SNat (n + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l SNat (n + l) -> SNat m -> SNat ((n + l) + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k SNat ((n + l) + m)
-> ((n + (l + m)) :~: ((n + l) + m))
-> Reason (:~:) (n + (l + m)) ((n + l) + 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 + l) + m) :~: (n + (l + m)))
-> (n + (l + m)) :~: ((n + l) + m)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat n -> SNat l -> SNat m -> ((n + l) + m) :~: (n + (l + m))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + m) + l) :~: (n + (m + l))
plusAssoc SNat n
n SNat l
l SNat m
k)
                (((n + m) + l) :~: ((n + l) + m))
-> SNat ((n + l) + m) -> ((n + m) + l) :~: ((n + l) + 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 l -> SNat (m + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l
       in SNat n -> SNat m -> SNat m -> ((n + m) :~: m) -> IsTrue (n <=? m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
leqStep SNat n
n SNat m
m SNat m
k (n + m) :~: m
pf

plusCancelLeqL ::
  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))
-> IsTrue (m <=? l)
plusCancelLeqL SNat n
n SNat m
m SNat l
l IsTrue ((n + m) <=? (n + l))
nmLEQnl =
  SNat m
-> SNat l
-> SNat n
-> IsTrue ((m + n) <=? (l + n))
-> IsTrue (m <=? l)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n
-> SNat m
-> SNat l
-> IsTrue ((n + l) <=? (m + l))
-> IsTrue (n <=? m)
plusCancelLeqR SNat m
m SNat l
l SNat n
n (IsTrue ((m + n) <=? (l + n)) -> IsTrue (m <=? l))
-> IsTrue ((m + n) <=? (l + n)) -> IsTrue (m <=? l)
forall a b. (a -> b) -> a -> b
$
    ((n + m) :~: (m + n))
-> SNat (l + n)
-> IsTrue ((n + m) <=? (l + n))
-> IsTrue ((m + n) <=? (l + n))
forall (n :: Nat) (m :: Nat) (l :: Nat).
(n :~: m) -> SNat l -> IsTrue (n <=? l) -> IsTrue (m <=? l)
coerceLeqL (SNat n -> SNat m -> (n + m) :~: (m + n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat n
n SNat m
m) (SNat l
l SNat l -> SNat n -> SNat (l + n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat n
n) (IsTrue ((n + m) <=? (l + n)) -> IsTrue ((m + n) <=? (l + n)))
-> IsTrue ((n + m) <=? (l + n)) -> IsTrue ((m + n) <=? (l + n))
forall a b. (a -> b) -> a -> b
$
      SNat (n + m)
-> ((n + l) :~: (l + n))
-> IsTrue ((n + m) <=? (n + l))
-> IsTrue ((n + m) <=? (l + n))
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat l -> (n :~: m) -> IsTrue (l <=? n) -> IsTrue (l <=? m)
coerceLeqR (SNat n
n SNat n -> SNat m -> SNat (n + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m) (SNat n -> SNat l -> (n + l) :~: (l + n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat n
n SNat l
l) IsTrue ((n + m) <=? (n + l))
nmLEQnl

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

succLeqZeroAbsurd' :: SNat n -> (S n <=? 0) :~: 'False
succLeqZeroAbsurd' :: SNat n -> (S n <=? 0) :~: 'False
succLeqZeroAbsurd' SNat n
n =
  case SNat n -> SNat (S n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n SNat (S n) -> SNat 0 -> SBool (S n <=? 0)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat 0
sZero of
    SBool (S n <=? 0)
STrue -> Void -> 'True :~: 'False
forall a. Void -> a
absurd (Void -> 'True :~: 'False) -> Void -> 'True :~: 'False
forall a b. (a -> b) -> a -> b
$ SNat n -> IsTrue (S n <=? 0) -> Void
forall (n :: Nat). SNat n -> IsTrue (S n <=? 0) -> Void
succLeqZeroAbsurd SNat n
n IsTrue (S n <=? 0)
IsTrue 'True
Witness
    SBool (S n <=? 0)
SFalse -> (S n <=? 0) :~: 'False
forall k (a :: k). a :~: a
Refl

succLeqAbsurd :: SNat n -> IsTrue (S n <=? n) -> Void
succLeqAbsurd :: SNat n -> IsTrue (S n <=? n) -> Void
succLeqAbsurd SNat n
n IsTrue (S n <=? n)
snLEQn =
  ('LT :~: 'EQ) -> Void
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 :: Nat) (m :: Nat).
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 :: Nat) (b :: Nat).
SNat a -> SNat b -> IsTrue (Succ 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 :: Nat) (b :: Nat).
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' :: SNat n -> (S n <=? n) :~: 'False
succLeqAbsurd' SNat n
n =
  case SNat n -> SNat (S n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n SNat (S n) -> SNat n -> SBool (S n <=? n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat n
n of
    SBool (S n <=? n)
STrue -> Void -> 'True :~: 'False
forall a. Void -> a
absurd (Void -> 'True :~: 'False) -> Void -> 'True :~: 'False
forall a b. (a -> b) -> a -> b
$ SNat n -> IsTrue (S n <=? n) -> Void
forall (n :: Nat). SNat n -> IsTrue (S n <=? n) -> Void
succLeqAbsurd SNat n
n IsTrue (S n <=? n)
IsTrue 'True
Witness
    SBool (S n <=? n)
SFalse -> (S n <=? n) :~: 'False
forall k (a :: k). a :~: a
Refl

notLeqToLeq :: ((n <=? m) ~ 'False) => SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq :: SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m =
  case SNat n -> SNat m -> SOrdering (CmpNat n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> SOrdering (CmpNat n m)
sCmpNat SNat n
n SNat m
m of
    SOrdering (CmpNat n m)
SLT -> IsTrue 'False -> IsTrue (m <=? n)
forall a x. Empty a => a -> x
eliminate (IsTrue 'False -> IsTrue (m <=? n))
-> IsTrue 'False -> IsTrue (m <=? n)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> IsTrue (n <=? m)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)
ltToLeq SNat n
n SNat m
m CmpNat n m :~: 'LT
forall k (a :: k). a :~: a
Refl
    SOrdering (CmpNat n m)
SEQ -> IsTrue 'False -> IsTrue (m <=? n)
forall a x. Empty a => a -> x
eliminate (IsTrue 'False -> IsTrue (m <=? n))
-> IsTrue 'False -> IsTrue (m <=? n)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive SNat n
n SNat m
m ((n :~: m) -> IsTrue (n <=? m)) -> (n :~: m) -> IsTrue (n <=? m)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> (CmpNat n m :~: 'EQ) -> n :~: m
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'EQ) -> a :~: b
eqToRefl SNat n
n SNat m
m CmpNat n m :~: 'EQ
forall k (a :: k). a :~: a
Refl
    SOrdering (CmpNat n m)
SGT -> SNat n -> SNat m -> (CmpNat n m :~: 'GT) -> IsTrue (m <=? n)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'GT) -> IsTrue (b <=? a)
gtToLeq SNat n
n SNat m
m CmpNat n m :~: 'GT
forall k (a :: k). a :~: a
Refl

leqSucc' :: SNat n -> SNat m -> (n <=? m) :~: (Succ n <=? Succ m)
leqSucc' :: SNat n -> SNat m -> (n <=? m) :~: (Succ n <=? Succ m)
leqSucc' SNat n
_ SNat m
_ = (n <=? m) :~: (Succ n <=? Succ m)
forall k (a :: k). a :~: a
Refl

leqToMin :: SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin :: SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin SNat n
_ SNat m
_ IsTrue (n <=? m)
Witness = Min n m :~: n
forall k (a :: k). a :~: a
Refl

geqToMin :: SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin :: SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin SNat n
n SNat m
m IsTrue (m <=? n)
Witness =
  case SNat n
n SNat n -> SNat m -> SBool (n <=? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
    SBool (n <=? m)
SFalse -> Min n m :~: m
forall k (a :: k). a :~: a
Refl
    SBool (n <=? m)
STrue -> Min n m :~: m
forall k (a :: k). a :~: a
Refl

minComm :: SNat n -> SNat m -> Min n m :~: Min m n
minComm :: 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
    SBool (n <=? m)
STrue ->
      SNat n -> n :~: 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 (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m) (n :~: n) -> Reason (:~:) n n -> 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 -> (n :~: n) -> Reason (:~:) 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 (n <=? m) -> Min n m :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin SNat n
n SNat m
m IsTrue (n <=? m)
IsTrue 'True
Witness
        (n :~: n) -> Reason (:~:) n (Min m n) -> n :~: Min 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat m
m SNat n
n SNat (Min m n) -> (n :~: Min m n) -> Reason (:~:) n (Min 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` (Min m n :~: n) -> n :~: Min 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 :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin SNat m
m SNat n
n IsTrue (n <=? m)
IsTrue 'True
Witness)
    SBool (n <=? m)
SFalse ->
      SNat m -> m :~: 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m) (m :~: m) -> Reason (:~:) 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
m SNat m -> (m :~: m) -> Reason (:~:) 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 :: Nat) (m :: Nat).
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 :: Nat) (m :: Nat).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m)
        (m :~: m) -> Reason (:~:) m (Min m n) -> m :~: Min 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat m
m SNat n
n SNat (Min m n) -> (m :~: Min m n) -> Reason (:~:) m (Min 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` (Min m n :~: m) -> m :~: Min 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 :: Nat) (m :: Nat).
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 :: Nat) (m :: Nat).
((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 :: 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
    SBool (n <=? m)
STrue -> SNat n -> SNat n -> (n :~: n) -> IsTrue (n <=? n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m) SNat n
n ((n :~: n) -> IsTrue (n <=? n)) -> (n :~: n) -> IsTrue (n <=? n)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
leqToMin SNat n
n SNat m
m IsTrue (n <=? m)
IsTrue 'True
Witness
    SBool (n <=? m)
SFalse ->
      let mLEQn :: IsTrue (m <=? n)
mLEQn = SNat n -> SNat m -> IsTrue (m <=? n)
forall (n :: Nat) (m :: Nat).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m
       in SNat m
-> SNat m
-> SNat n
-> IsTrue (m <=? m)
-> IsTrue (m <=? n)
-> IsTrue (m <=? n)
forall (n :: Nat) (m :: Nat) (l :: Nat).
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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m)
            SNat m
m
            SNat n
n
            (SNat m -> SNat m -> (m :~: m) -> IsTrue (m <=? m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). 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 :: Nat) (m :: Nat).
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 (m <=? n))
-> IsTrue (m <=? n) -> IsTrue (m <=? n)
forall a b. (a -> b) -> a -> b
$ IsTrue (m <=? n)
mLEQn

minLeqR :: SNat n -> SNat m -> IsTrue (Min n m <=? m)
minLeqR :: SNat n -> SNat m -> IsTrue (Min n m <=? m)
minLeqR SNat n
n SNat m
m =
  SNat (Min n m)
-> SNat (MinAux (m <=? n) m n)
-> SNat m
-> IsTrue (Min n m <=? MinAux (m <=? n) m n)
-> IsTrue (MinAux (m <=? n) m n <=? m)
-> IsTrue (Min n m <=? m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m)
    (SNat m -> SNat n -> SNat (MinAux (m <=? n) m n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat m
m SNat n
n)
    SNat m
m
    (SNat (Min n m)
-> SNat (MinAux (m <=? n) m n)
-> (Min n m :~: MinAux (m <=? n) m n)
-> IsTrue (Min n m <=? MinAux (m <=? n) m n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m) (SNat m -> SNat n -> SNat (MinAux (m <=? n) m n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat m
m SNat n
n) ((Min n m :~: MinAux (m <=? n) m n)
 -> IsTrue (Min n m <=? MinAux (m <=? n) m n))
-> (Min n m :~: MinAux (m <=? n) m n)
-> IsTrue (Min n m <=? MinAux (m <=? n) m n)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> Min n m :~: MinAux (m <=? n) m n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> Min n m :~: Min m n
minComm SNat n
n SNat m
m)
    (SNat m -> SNat n -> IsTrue (MinAux (m <=? n) m n <=? m)
forall (n :: Nat) (m :: Nat).
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 :: SNat l
-> SNat n
-> SNat m
-> IsTrue (l <=? n)
-> IsTrue (l <=? m)
-> IsTrue (l <=? Min n m)
minLargest SNat l
l SNat n
n SNat m
m IsTrue (l <=? n)
lLEQn IsTrue (l <=? m)
lLEQm =
  SNat l
-> (KnownNat l => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat l
l ((KnownNat l => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m))
-> (KnownNat l => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m)
forall a b. (a -> b) -> a -> b
$
    SNat n
-> (KnownNat n => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n ((KnownNat n => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m))
-> (KnownNat n => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m)
forall a b. (a -> b) -> a -> b
$
      SNat m
-> (KnownNat m => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat m
m ((KnownNat m => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m))
-> (KnownNat m => IsTrue (l <=? Min n m)) -> IsTrue (l <=? Min n m)
forall a b. (a -> b) -> a -> b
$
        SNat (Min n m)
-> (KnownNat (Min n m) => IsTrue (l <=? Min n m))
-> IsTrue (l <=? Min n m)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m) ((KnownNat (Min n m) => IsTrue (l <=? Min n m))
 -> IsTrue (l <=? Min n m))
-> (KnownNat (Min n m) => IsTrue (l <=? Min n m))
-> IsTrue (l <=? Min n m)
forall a b. (a -> b) -> a -> b
$
          case SNat n
n SNat n -> SNat m -> SBool (n <=? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
            SBool (n <=? m)
STrue -> IsTrue (l <=? n)
IsTrue (l <=? Min n m)
lLEQn
            SBool (n <=? m)
SFalse -> IsTrue (l <=? m)
IsTrue (l <=? Min n m)
lLEQm

leqToMax :: SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax :: SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm =
  SNat (Max n m)
-> SNat m
-> IsTrue (Max n m <=? m)
-> IsTrue (m <=? Max n m)
-> Max n m :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m
leqAntisymm (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) SNat m
m (SNat m
-> SNat n
-> SNat m
-> IsTrue (n <=? m)
-> IsTrue (m <=? m)
-> IsTrue (Max n m <=? m)
forall (l :: Nat) (n :: Nat) (m :: Nat).
SNat l
-> SNat n
-> SNat m
-> IsTrue (n <=? l)
-> IsTrue (m <=? l)
-> IsTrue (Max n m <=? l)
maxLeast SNat m
m SNat n
n SNat m
m IsTrue (n <=? m)
nLEQm (SNat m -> IsTrue (m <=? m)
forall (n :: Nat). SNat n -> IsTrue (n <=? n)
leqRefl SNat m
m)) (SNat n -> SNat m -> IsTrue (m <=? Max n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? Max n m)
maxLeqR SNat n
n SNat m
m)

geqToMax :: SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax :: SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax SNat n
n SNat m
m IsTrue (m <=? n)
mLEQn =
  SNat (Max n m)
-> SNat n
-> IsTrue (Max n m <=? n)
-> IsTrue (n <=? Max n m)
-> Max n m :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m
leqAntisymm (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) SNat n
n (SNat n
-> SNat n
-> SNat m
-> IsTrue (n <=? n)
-> IsTrue (m <=? n)
-> IsTrue (Max n m <=? n)
forall (l :: Nat) (n :: Nat) (m :: Nat).
SNat l
-> SNat n
-> SNat m
-> IsTrue (n <=? l)
-> IsTrue (m <=? l)
-> IsTrue (Max n m <=? l)
maxLeast SNat n
n SNat n
n SNat m
m (SNat n -> IsTrue (n <=? n)
forall (n :: Nat). SNat n -> IsTrue (n <=? n)
leqRefl SNat n
n) IsTrue (m <=? n)
mLEQn) (SNat n -> SNat m -> IsTrue (n <=? Max n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? Max n m)
maxLeqL SNat n
n SNat m
m)

maxComm :: SNat n -> SNat m -> Max n m :~: Max m n
maxComm :: 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
    SBool (n <=? m)
STrue ->
      SNat (Max n m) -> Max n m :~: Max 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 (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) (Max n m :~: Max n m) -> Reason (:~:) (Max n m) m -> Max 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 -> (Max n m :~: m) -> Reason (:~:) (Max 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 (n <=? m) -> Max n m :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax SNat n
n SNat m
m IsTrue (n <=? m)
IsTrue 'True
Witness
        (Max n m :~: m) -> Reason (:~:) m m -> Max 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 -> SNat n -> SNat (Max m n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat m
m SNat n
n SNat m -> (m :~: m) -> Reason (:~:) 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
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat m -> SNat n -> IsTrue (n <=? m) -> Max m n :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax SNat m
m SNat n
n IsTrue (n <=? m)
IsTrue 'True
Witness)
    SBool (n <=? m)
SFalse ->
      SNat (Max n m) -> Max n m :~: Max 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 (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) (Max n m :~: Max n m) -> Reason (:~:) (Max n m) n -> Max 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 -> (Max n m :~: n) -> Reason (:~:) (Max 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 (m <=? n) -> Max n m :~: n
forall (n :: Nat) (m :: Nat).
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 :: Nat) (m :: Nat).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m)
        (Max n m :~: n) -> Reason (:~:) n n -> Max 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 m -> SNat n -> SNat (Max m n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat m
m SNat n
n SNat n -> (n :~: n) -> Reason (:~:) 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` (n :~: n) -> n :~: n
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (SNat m -> SNat n -> IsTrue (m <=? n) -> Max m n :~: n
forall (n :: Nat) (m :: Nat).
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 :: Nat) (m :: Nat).
((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 :: 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
    SBool (n <=? m)
STrue -> SNat m
-> SNat (Max n m) -> (m :~: Max n m) -> IsTrue (m <=? Max n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive SNat m
m (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) ((m :~: Max n m) -> IsTrue (m <=? Max n m))
-> (m :~: Max n m) -> IsTrue (m <=? Max n m)
forall a b. (a -> b) -> a -> b
$ (Max n m :~: m) -> m :~: Max n m
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((Max n m :~: m) -> m :~: Max n m)
-> (Max n m :~: m) -> m :~: Max n m
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax SNat n
n SNat m
m IsTrue (n <=? m)
IsTrue 'True
Witness
    SBool (n <=? m)
SFalse ->
      let mLEQn :: IsTrue (m <=? n)
mLEQn = SNat n -> SNat m -> IsTrue (m <=? n)
forall (n :: Nat) (m :: Nat).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m
       in SNat m
-> SNat n
-> SNat (Max n m)
-> IsTrue (m <=? n)
-> IsTrue (n <=? Max n m)
-> IsTrue (m <=? Max n m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m)
            IsTrue (m <=? n)
mLEQn
            (SNat n
-> SNat (Max n m) -> (n :~: Max n m) -> IsTrue (n <=? Max n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive SNat n
n (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) ((Max n m :~: n) -> n :~: Max n m
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((Max n m :~: n) -> n :~: Max n m)
-> (Max n m :~: n) -> n :~: Max n m
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
forall (n :: Nat) (m :: Nat).
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 :: SNat n -> SNat m -> IsTrue (n <=? Max n m)
maxLeqL SNat n
n SNat m
m =
  SNat n
-> SNat (MaxAux (n <=? m) m n)
-> SNat (Max n m)
-> IsTrue (n <=? MaxAux (n <=? m) m n)
-> IsTrue (MaxAux (n <=? m) m n <=? Max n m)
-> IsTrue (n <=? Max n m)
forall (n :: Nat) (m :: Nat) (l :: Nat).
SNat n
-> SNat m
-> SNat l
-> IsTrue (n <=? m)
-> IsTrue (m <=? l)
-> IsTrue (n <=? l)
leqTrans
    SNat n
n
    (SNat m -> SNat n -> SNat (MaxAux (n <=? m) m n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat m
m SNat n
n)
    (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m)
    (SNat m -> SNat n -> IsTrue (n <=? MaxAux (n <=? m) m n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? Max n m)
maxLeqR SNat m
m SNat n
n)
    (SNat (MaxAux (n <=? m) m n)
-> SNat (Max n m)
-> (MaxAux (n <=? m) m n :~: Max n m)
-> IsTrue (MaxAux (n <=? m) m n <=? Max n m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
leqReflexive (SNat m -> SNat n -> SNat (MaxAux (n <=? m) m n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat m
m SNat n
n) (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) ((MaxAux (n <=? m) m n :~: Max n m)
 -> IsTrue (MaxAux (n <=? m) m n <=? Max n m))
-> (MaxAux (n <=? m) m n :~: Max n m)
-> IsTrue (MaxAux (n <=? m) m n <=? Max n m)
forall a b. (a -> b) -> a -> b
$ SNat m -> SNat n -> MaxAux (n <=? m) m n :~: Max n m
forall (n :: Nat) (m :: Nat).
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 :: SNat l
-> SNat n
-> SNat m
-> IsTrue (n <=? l)
-> IsTrue (m <=? l)
-> IsTrue (Max n m <=? l)
maxLeast SNat l
l SNat n
n SNat m
m IsTrue (n <=? l)
lLEQn IsTrue (m <=? l)
lLEQm =
  SNat l
-> (KnownNat l => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat l
l ((KnownNat l => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l))
-> (KnownNat l => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l)
forall a b. (a -> b) -> a -> b
$
    SNat n
-> (KnownNat n => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n ((KnownNat n => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l))
-> (KnownNat n => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l)
forall a b. (a -> b) -> a -> b
$
      SNat m
-> (KnownNat m => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat m
m ((KnownNat m => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l))
-> (KnownNat m => IsTrue (Max n m <=? l)) -> IsTrue (Max n m <=? l)
forall a b. (a -> b) -> a -> b
$
        SNat (Max n m)
-> (KnownNat (Max n m) => IsTrue (Max n m <=? l))
-> IsTrue (Max n m <=? l)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m) ((KnownNat (Max n m) => IsTrue (Max n m <=? l))
 -> IsTrue (Max n m <=? l))
-> (KnownNat (Max n m) => IsTrue (Max n m <=? l))
-> IsTrue (Max n m <=? l)
forall a b. (a -> b) -> a -> b
$
          case SNat n
n SNat n -> SNat m -> SBool (n >=? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n >=? m)
%>=? SNat m
m of
            SBool (n >=? m)
STrue -> IsTrue (n <=? l)
IsTrue (Max n m <=? l)
lLEQn
            SBool (n >=? m)
SFalse -> IsTrue (m <=? l)
IsTrue (Max n m <=? l)
lLEQm

lneqSuccLeq :: SNat n -> SNat m -> (n < m) :~: (Succ n <= m)
lneqSuccLeq :: SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq SNat n
_ SNat m
_ = (n < m) :~: (n < m)
forall k (a :: k). a :~: a
Refl

lneqReversed :: SNat n -> SNat m -> (n < m) :~: (m > n)
lneqReversed :: SNat n -> SNat m -> (n < m) :~: (n < m)
lneqReversed SNat n
_ SNat m
_ = (n < m) :~: (n < m)
forall k (a :: k). a :~: a
Refl

lneqToLT ::
  SNat n ->
  SNat m ->
  IsTrue (n <? m) ->
  CmpNat n m :~: 'LT
lneqToLT :: SNat n -> SNat m -> IsTrue (n <? m) -> CmpNat n m :~: 'LT
lneqToLT SNat n
n SNat m
m IsTrue (n <? m)
nLNEm =
  SNat n -> SNat m -> IsTrue (n <? m) -> CmpNat n m :~: 'LT
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT
succLeqToLT SNat n
n SNat m
m (IsTrue (n <? m) -> CmpNat n m :~: 'LT)
-> IsTrue (n <? m) -> CmpNat n m :~: 'LT
forall a b. (a -> b) -> a -> b
$ (((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
-> IsTrue (n <? m)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n -> SNat m -> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq SNat n
n SNat m
m) IsTrue (n <? m)
(((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m)
nLNEm

ltToLneq ::
  SNat n ->
  SNat m ->
  CmpNat n m :~: 'LT ->
  IsTrue (n <? m)
ltToLneq :: SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> IsTrue (n <? m)
ltToLneq SNat n
n SNat m
m CmpNat n m :~: 'LT
nLTm =
  (((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
-> IsTrue (n <? m)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith ((((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
 -> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> (((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq SNat n
n SNat m
m) (((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
 -> IsTrue (n <? m))
-> ((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
-> IsTrue (n <? m)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> IsTrue (n <? m)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)
ltToSuccLeq SNat n
n SNat m
m CmpNat n m :~: 'LT
nLTm

lneqZero :: SNat a -> IsTrue (0 <? Succ a)
lneqZero :: SNat a -> IsTrue (0 <? Succ a)
lneqZero SNat a
n = SNat 0
-> SNat (Succ a)
-> (CmpNat 0 (Succ a) :~: 'LT)
-> IsTrue (0 <? Succ a)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)
ltToLneq SNat 0
sZero (SNat a -> SNat (Succ a)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat a
n) ((CmpNat 0 (Succ a) :~: 'LT) -> IsTrue (0 <? Succ a))
-> (CmpNat 0 (Succ a) :~: 'LT) -> IsTrue (0 <? Succ a)
forall a b. (a -> b) -> a -> b
$ SNat a -> CmpNat 0 (Succ a) :~: 'LT
forall (a :: Nat). SNat a -> CmpNat 0 (Succ a) :~: 'LT
cmpZero SNat a
n

lneqSucc :: SNat n -> IsTrue (n <? Succ n)
lneqSucc :: SNat n -> IsTrue (n <? Succ n)
lneqSucc SNat n
n = SNat n
-> SNat (Succ n)
-> (CmpNat n (Succ n) :~: 'LT)
-> IsTrue (n <? Succ n)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)
ltToLneq SNat n
n (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) ((CmpNat n (Succ n) :~: 'LT) -> IsTrue (n <? Succ n))
-> (CmpNat n (Succ n) :~: 'LT) -> IsTrue (n <? Succ n)
forall a b. (a -> b) -> a -> b
$ SNat n -> CmpNat n (Succ n) :~: 'LT
forall (a :: Nat). SNat a -> CmpNat a (Succ a) :~: 'LT
ltSucc SNat n
n

succLneqSucc ::
  SNat n ->
  SNat m ->
  (n <? m) :~: (Succ n <? Succ m)
succLneqSucc :: SNat n -> SNat m -> (n <? m) :~: (Succ n <? Succ m)
succLneqSucc SNat n
_ SNat m
_ = (n <? m) :~: (Succ n <? Succ m)
forall k (a :: k). a :~: a
Refl

lneqRightPredSucc ::
  SNat n ->
  SNat m ->
  IsTrue (n <? m) ->
  m :~: Succ (Pred m)
lneqRightPredSucc :: 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 :~: Succ (Pred m)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> b :~: Succ (Pred b)
ltRightPredSucc SNat n
n SNat m
m ((CmpNat n m :~: 'LT) -> m :~: Succ (Pred m))
-> (CmpNat n m :~: 'LT) -> m :~: Succ (Pred m)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> IsTrue (n <? m) -> CmpNat n m :~: 'LT
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: '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 :: SNat n -> SNat m -> IsTrue (Succ n <? m) -> IsTrue (n <? m)
lneqSuccStepL SNat n
n SNat m
m IsTrue (Succ n <? m)
snLNEQm =
  (((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
-> IsTrue (n <? m)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith ((((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
 -> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> (((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq SNat n
n SNat m
m) (((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
 -> IsTrue (n <? m))
-> ((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
-> IsTrue (n <? m)
forall a b. (a -> b) -> a -> b
$
    SNat (Succ n) -> SNat m -> IsTrue (Succ n <? m) -> IsTrue (n <? m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m)
leqSuccStepL (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m (IsTrue (Succ n <? m) -> IsTrue (n <? m))
-> IsTrue (Succ n <? m) -> IsTrue (n <? m)
forall a b. (a -> b) -> a -> b
$
      (((Succ n <? m) ~ 'True) :~: ((Succ n <? m) ~ 'True))
-> ((((Succ n <? m) ~ 'True) ~ ((Succ n <? m) ~ 'True)) =>
    IsTrue (Succ n <? m))
-> IsTrue (Succ n <? m)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat (Succ n)
-> SNat m -> ((Succ n <? m) ~ 'True) :~: ((Succ n <? m) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n) SNat m
m) IsTrue (Succ n <? m)
(((Succ n <? m) ~ 'True) ~ ((Succ n <? m) ~ 'True)) =>
IsTrue (Succ n <? m)
snLNEQm

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

plusStrictMonotone ::
  SNat n ->
  SNat m ->
  SNat l ->
  SNat k ->
  IsTrue (n <? m) ->
  IsTrue (l <? k) ->
  IsTrue ((n + l) <? (m + k))
plusStrictMonotone :: 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 =
  ((((n + l) <? (m + k)) ~ 'True) :~: (((n + l) <? (m + k)) ~ 'True))
-> (((((n + l) <? (m + k)) ~ 'True)
     ~ (((n + l) <? (m + k)) ~ 'True)) =>
    IsTrue ((n + l) <? (m + k)))
-> IsTrue ((n + l) <? (m + k))
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (((((n + l) <? (m + k)) ~ 'True) :~: (((n + l) <? (m + k)) ~ 'True))
-> (((n + l) <? (m + k)) ~ 'True)
   :~: (((n + l) <? (m + k)) ~ 'True)
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (((((n + l) <? (m + k)) ~ 'True)
  :~: (((n + l) <? (m + k)) ~ 'True))
 -> (((n + l) <? (m + k)) ~ 'True)
    :~: (((n + l) <? (m + k)) ~ 'True))
-> ((((n + l) <? (m + k)) ~ 'True)
    :~: (((n + l) <? (m + k)) ~ 'True))
-> (((n + l) <? (m + k)) ~ 'True)
   :~: (((n + l) <? (m + k)) ~ 'True)
forall a b. (a -> b) -> a -> b
$ SNat (n + l)
-> SNat (m + k)
-> (((n + l) <? (m + k)) ~ 'True)
   :~: (((n + l) <? (m + k)) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq (SNat n
n SNat n -> SNat l -> SNat (n + l)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat l
l) (SNat m
m SNat m -> SNat k -> SNat (m + k)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat k
k)) ((((((n + l) <? (m + k)) ~ 'True)
   ~ (((n + l) <? (m + k)) ~ 'True)) =>
  IsTrue ((n + l) <? (m + k)))
 -> IsTrue ((n + l) <? (m + k)))
-> (((((n + l) <? (m + k)) ~ 'True)
     ~ (((n + l) <? (m + k)) ~ 'True)) =>
    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 (((n + 1) + l) <=? (m + k))
 -> IsTrue ((n + l) <? (m + k)))
-> SNat (m + k)
-> (((n + 1) + l) :~: ((n + l) + 1))
-> IsTrue (((n + 1) + l) <=? (m + k))
-> 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 (((n + 1) + l) <=? (m + k))
-> IsTrue ((n + l) <? (m + k))
forall (n :: Nat) (m :: Nat) (l :: Nat).
(n :~: m) -> SNat l -> IsTrue (n <=? l) -> IsTrue (m <=? l)
coerceLeqL (SNat m
m SNat m -> SNat k -> SNat (m + k)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat k
k) (SNat n -> SNat l -> ((n + 1) + l) :~: ((n + l) + 1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (S n + m) :~: S (n + m)
plusSuccL SNat n
n SNat l
l) (IsTrue (((n + 1) + l) <=? (m + k)) -> IsTrue ((n + l) <? (m + k)))
-> IsTrue (((n + 1) + l) <=? (m + k))
-> IsTrue ((n + l) <? (m + k))
forall a b. (a -> b) -> a -> b
$
      SNat (n + 1)
-> SNat m
-> SNat l
-> SNat k
-> IsTrue (n <? m)
-> IsTrue (l <=? k)
-> IsTrue (((n + 1) + l) <=? (m + k))
forall (n :: Nat) (m :: Nat) (l :: Nat) (k :: Nat).
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 :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n)
        SNat m
m
        SNat l
l
        SNat k
k
        ((((n <? m) ~ 'True) :~: ((n <? m) ~ 'True))
-> ((((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m))
-> IsTrue (n <? m)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n -> SNat m -> ((n <? m) ~ 'True) :~: ((n <? m) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq SNat n
n SNat m
m) IsTrue (n <? m)
(((n <? m) ~ 'True) ~ ((n <? m) ~ 'True)) => IsTrue (n <? m)
nLNm)
        ( SNat l
-> SNat (l + 1)
-> SNat k
-> IsTrue (l <=? (l + 1))
-> IsTrue (l <? k)
-> IsTrue (l <=? k)
forall (n :: Nat) (m :: Nat) (l :: Nat).
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 :: Nat). 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 :: Nat) (m :: Nat).
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 :: Nat). SNat n -> IsTrue (n <=? n)
leqRefl SNat l
l)) (IsTrue (l <? k) -> IsTrue (l <=? k))
-> IsTrue (l <? k) -> IsTrue (l <=? k)
forall a b. (a -> b) -> a -> b
$
            (((l <? k) ~ 'True) :~: ((l <? k) ~ 'True))
-> ((((l <? k) ~ 'True) ~ ((l <? k) ~ 'True)) => IsTrue (l <? k))
-> IsTrue (l <? k)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat l -> SNat k -> ((l <? k) ~ 'True) :~: ((l <? k) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq SNat l
l SNat k
k) IsTrue (l <? k)
(((l <? k) ~ 'True) ~ ((l <? k) ~ 'True)) => IsTrue (l <? k)
lLNk
        )

maxZeroL :: SNat n -> Max 0 n :~: n
maxZeroL :: SNat n -> Max 0 n :~: n
maxZeroL SNat n
n = SNat 0 -> SNat n -> IsTrue (0 <=? n) -> Max 0 n :~: n
forall (n :: Nat) (m :: Nat).
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 :: Nat). SNat n -> IsTrue (0 <=? n)
leqZero SNat n
n)

maxZeroR :: SNat n -> Max n 0 :~: n
maxZeroR :: SNat n -> Max n 0 :~: n
maxZeroR SNat n
n = SNat n -> SNat 0 -> IsTrue (0 <=? n) -> Max n 0 :~: n
forall (n :: Nat) (m :: Nat).
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 :: Nat). SNat n -> IsTrue (0 <=? n)
leqZero SNat n
n)

minZeroL :: SNat n -> Min 0 n :~: 0
minZeroL :: SNat n -> Min 0 n :~: 0
minZeroL SNat n
n = SNat 0 -> SNat n -> IsTrue (0 <=? n) -> Min 0 n :~: 0
forall (n :: Nat) (m :: Nat).
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 :: Nat). SNat n -> IsTrue (0 <=? n)
leqZero SNat n
n)

minZeroR :: SNat n -> Min n 0 :~: 0
minZeroR :: SNat n -> Min n 0 :~: 0
minZeroR SNat n
n = SNat n -> SNat 0 -> IsTrue (0 <=? n) -> Min n 0 :~: 0
forall (n :: Nat) (m :: Nat).
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 :: Nat). SNat n -> IsTrue (0 <=? n)
leqZero SNat n
n)

minusSucc :: SNat n -> SNat m -> IsTrue (m <=? n) -> Succ n - m :~: Succ (n - m)
minusSucc :: 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 :: Nat) (m :: Nat).
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 :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n SNat (Succ n) -> SNat m -> SNat (Succ n - m)
forall (n :: Nat) (m :: Nat). 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 :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat m
m SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k) SNat (Succ n) -> SNat m -> SNat (Succ n - m)
forall (n :: Nat) (m :: Nat). 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m -> SNat (m + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k) SNat (m + (m + 1)) -> SNat m -> SNat ((m + (m + 1)) - m)
forall (n :: Nat) (m :: Nat). 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 :: Nat) (m :: Nat) (k :: Nat).
(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 :: Nat) (m :: Nat).
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 :: Nat). SNat n -> SNat (Succ n)
sSucc SNat m
k SNat (m + 1) -> SNat m -> SNat ((m + 1) + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m) SNat ((m + 1) + m) -> SNat m -> SNat (((m + 1) + m) - m)
forall (n :: Nat) (m :: Nat). 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 :: Nat) (m :: Nat) (k :: Nat).
(n :~: m) -> SNat k -> (n - k) :~: (m - k)
minusCongL (SNat m -> SNat (m + 1) -> (m + (m + 1)) :~: ((m + 1) + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
m (SNat m -> SNat (m + 1)
forall (n :: Nat). 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 :: Nat). 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 :: Nat) (m :: Nat).
SNat n -> SNat m -> ((n + m) - m) :~: n
plusMinus (SNat m -> SNat (m + 1)
forall (n :: Nat). 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 :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat m
k SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m SNat (m + m) -> SNat m -> SNat ((m + m) - m)
forall (n :: Nat) (m :: Nat). 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 :: Nat) (m :: Nat). (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 :: Nat) (m :: Nat).
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 :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat m
m SNat m -> SNat m -> SNat (m + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). 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 :: Nat) (m :: Nat). (n :~: m) -> S n :~: S m
succCong (((m + m) :~: n) -> SNat m -> ((m + m) - m) :~: (n - m)
forall (n :: Nat) (m :: Nat) (k :: Nat).
(n :~: m) -> SNat k -> (n - k) :~: (m - k)
minusCongL (SNat m -> SNat m -> (m + m) :~: (m + m)
forall (n :: Nat) (m :: Nat).
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 :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m)

lneqZeroAbsurd :: SNat n -> IsTrue (n <? 0) -> Void
lneqZeroAbsurd :: SNat n -> IsTrue (n <? 0) -> Void
lneqZeroAbsurd SNat n
n IsTrue (n <? 0)
leq =
  SNat n -> IsTrue (n <? 0) -> Void
forall (n :: Nat). SNat n -> IsTrue (S n <=? 0) -> Void
succLeqZeroAbsurd SNat n
n ((((n <? 0) ~ 'True) :~: ((n <? 0) ~ 'True))
-> ((((n <? 0) ~ 'True) ~ ((n <? 0) ~ 'True)) => IsTrue (n <? 0))
-> IsTrue (n <? 0)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n -> SNat 0 -> ((n <? 0) ~ 'True) :~: ((n <? 0) ~ 'True)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n < m) :~: (n < m)
lneqSuccLeq SNat n
n SNat 0
sZero) IsTrue (n <? 0)
(((n <? 0) ~ 'True) ~ ((n <? 0) ~ 'True)) => IsTrue (n <? 0)
leq)

minusPlus ::
  forall n m.
  SNat n ->
  SNat m ->
  IsTrue (m <=? n) ->
  n - m + m :~: n
minusPlus :: 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 :: Nat) (m :: Nat).
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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m SNat (n - m) -> SNat m -> SNat ((n - m) + m)
forall (n :: Nat) (m :: Nat). 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
k SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m SNat (n - m) -> SNat m -> SNat ((n - m) + m)
forall (n :: Nat) (m :: Nat). 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m SNat (m + m) -> SNat m -> SNat ((m + m) - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m SNat ((m + m) - m) -> SNat m -> SNat (((m + m) - m) + m)
forall (n :: Nat) (m :: Nat). 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 :: Nat) (m :: Nat) (k :: Nat).
(n :~: m) -> SNat k -> (n + k) :~: (m + k)
plusCongL ((n :~: (m + m)) -> SNat m -> (n - m) :~: ((m + m) - m)
forall (n :: Nat) (m :: Nat) (k :: Nat).
(n :~: m) -> SNat k -> (n - k) :~: (m - k)
minusCongL (SNat m -> SNat m -> (m + m) :~: (m + m)
forall (n :: Nat) (m :: Nat).
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 :: Nat) (m :: Nat). 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 :: Nat) (m :: Nat) (k :: Nat).
(n :~: m) -> SNat k -> (n + k) :~: (m + k)
plusCongL (SNat m -> SNat m -> ((m + m) - m) :~: m
forall (n :: Nat) (m :: Nat).
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 :: Nat) (m :: Nat). 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 :: Nat) (m :: Nat).
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 %-. :: SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m =
  case SNat m
m SNat m -> SNat n -> SBool (m <=? n)
forall (n :: Nat) (m :: Nat). 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 :: Nat) (m :: Nat). 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 :: 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat n
n of
    SBool (m <=? n)
STrue ->
      SNat (Min n m + (n - m))
-> (Min n m + (n - m)) :~: (Min 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m SNat (Min n m) -> SNat (n - m) -> SNat (Min n m + (n - m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat n
n SNat n -> SNat m -> SNat (n -. m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m))
        ((Min n m + (n - m)) :~: (Min n m + (n - m)))
-> Reason (:~:) (Min n m + (n - m)) (m + (n - m))
-> (Min 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat n
n SNat n -> SNat m -> SNat (n -. m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m) SNat (m + (n - m))
-> ((Min n m + (n - m)) :~: (m + (n - m)))
-> Reason (:~:) (Min 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` (Min n m :~: m)
-> SNat (n - m) -> (Min n m + (n - m)) :~: (m + (n - m))
forall (n :: Nat) (m :: Nat) (k :: Nat).
(n :~: m) -> SNat k -> (n + k) :~: (m + k)
plusCongL (SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
geqToMin SNat n
n SNat m
m IsTrue (m <=? n)
IsTrue 'True
Witness) (SNat n
n SNat n -> SNat m -> SNat (n -. m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m)
        ((Min n m + (n - m)) :~: (m + (n - m)))
-> SNat (m + (n - m)) -> (Min 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m)
        ((Min n m + (n - m)) :~: (m + (n - m)))
-> Reason (:~:) (m + (n - m)) ((n - m) + m)
-> (Min 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m) SNat (n - m) -> SNat m -> SNat ((n - m) + m)
forall (n :: Nat) (m :: Nat). 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 :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
m (SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m)
        ((Min n m + (n - m)) :~: ((n - m) + m))
-> Reason (:~:) ((n - m) + m) n -> (Min 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 :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
minusPlus SNat n
n SNat m
m IsTrue (m <=? n)
IsTrue 'True
Witness
    SBool (m <=? n)
SFalse ->
      SNat (Min n m) -> Min n m :~: Min 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m SNat (Min n m) -> SNat 0 -> SNat (Min n m + 0)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat n
n SNat n -> SNat m -> SNat (n -. m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n -. m)
%-. SNat m
m))
        (Min n m :~: Min n m) -> SNat (Min n m) -> Min n m :~: Min 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m SNat (Min n m) -> SNat 0 -> SNat (Min n m + 0)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat 0
sZero
        (Min n m :~: Min n m)
-> Reason (:~:) (Min n m) (Min n m) -> Min n m :~: Min 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 :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m SNat (Min n m)
-> (Min n m :~: Min n m) -> Reason (:~:) (Min n m) (Min 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 (Min n m) -> (Min n m + 0) :~: Min n m
forall (n :: Nat). SNat n -> (n + 0) :~: n
plusZeroR (SNat n -> SNat m -> SNat (Min n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
sMin SNat n
n SNat m
m)
        (Min n m :~: Min n m) -> Reason (:~:) (Min n m) n -> Min 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 -> (Min n m :~: n) -> Reason (:~:) (Min 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 :: Nat) (m :: Nat).
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 :: Nat) (m :: Nat).
((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 :: 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 :: Nat) (m :: Nat). 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 :: Nat) (m :: Nat) (l :: Nat).
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 :: Nat) (m :: Nat). 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 :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
minusPlus SNat n
n SNat m
m IsTrue (m <=? n)
IsTrue 'True
Witness
    SBool (m <=? n)
SFalse -> SNat n -> IsTrue (0 <=? n)
forall (n :: Nat). SNat n -> IsTrue (0 <=? n)
leqZero SNat n
n