    {-|
    Description : Type level natural number representation at runtime
    Copyright   : (c) Galois, Inc 2014-2019
    Maintainer  : Joe Hendrix <jhendrix@galois.com>

    This defines a type 'NatRepr' for representing a type-level natural
    at runtime.  This can be used to branch on a type-level value.  For
    each @n@, @NatRepr n@ contains a single value containing the value
    @n@.  This can be used to help use type-level variables on code
    with data dependendent types.

    The @TestEquality@ and @DecidableEq@ instances for 'NatRepr'
    are implemented using 'unsafeCoerce', as is the `isZeroNat` function. This
    should be typesafe because we maintain the invariant that the integer value
    contained in a NatRepr value matches its static type.
    -}
    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE DeriveDataTypeable #-}
    {-# LANGUAGE EmptyCase #-}
    {-# LANGUAGE EmptyDataDecls #-}
    {-# LANGUAGE ExplicitNamespaces #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE RoleAnnotations #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE Trustworthy #-}
    {-# LANGUAGE TypeApplications #-}
    {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
    #if __GLASGOW_HASKELL__ >= 805
    {-# LANGUAGE NoStarIsType #-}
    #endif
    module Data.Parameterized.NatRepr
      ( NatRepr
      , natValue
      , intValue
      , knownNat
      , withKnownNat
      , IsZeroNat(..)
      , isZeroNat
      , isZeroOrGT1
      , NatComparison(..)
      , compareNat
      , decNat
      , predNat
      , incNat
      , addNat
      , subNat
      , divNat
      , halfNat
      , withDivModNat
      , natMultiply
      , someNat
      , mkNatRepr
      , maxNat
      , natRec
      , natRecStrong
      , natRecBounded
      , natRecStrictlyBounded
      , natForEach
      , natFromZero
      , NatCases(..)
      , testNatCases
        -- * Strict order
      , lessThanIrreflexive
      , lessThanAsymmetric
        -- * Bitvector utilities
      , widthVal
      , minUnsigned
      , maxUnsigned
      , minSigned
      , maxSigned
      , toUnsigned
      , toSigned
      , unsignedClamp
      , signedClamp
        -- * LeqProof
      , LeqProof(..)
      , decideLeq
      , testLeq
      , testStrictLeq
      , leqRefl
      , leqSucc
      , leqTrans
      , leqZero
      , leqAdd2
      , leqSub2
      , leqMulCongr
        -- * LeqProof combinators
      , leqProof
      , withLeqProof
      , isPosNat
      , leqAdd
      , leqSub
      , leqMulPos
      , leqAddPos
      , addIsLeq
      , withAddLeq
      , addPrefixIsLeq
      , withAddPrefixLeq
      , addIsLeqLeft1
      , dblPosIsPos
      , leqMulMono
        -- * Arithmetic proof
      , plusComm
      , plusAssoc
      , mulComm
      , plusMinusCancel
      , minusPlusCancel
      , addMulDistribRight
      , withAddMulDistribRight
      , withSubMulDistribRight
      , mulCancelR
      , mul2Plus
      , lemmaMul
        -- * Re-exports typelists basics
    --  , NatK
      , type (+)
      , type (-)
      , type (*)
      , type (<=)
      , Equality.TestEquality(..)
      , (Equality.:~:)(..)
      , Data.Parameterized.Some.Some
      ) where

    import Data.Bits ((.&.), bit)
    import Data.Data
    import Data.Type.Equality as Equality
    import Data.Void as Void
    import Numeric.Natural
    import GHC.TypeNats ( KnownNat, Nat, SomeNat(..)
                        , type (+), type (-), type (*), type (<=)
                        , someNatVal )
    import Unsafe.Coerce

    import Data.Parameterized.Axiom
    import Data.Parameterized.NatRepr.Internal
    import Data.Parameterized.Some

    maxInt :: Natural
    maxInt :: Natural
    maxInt = Int -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int
    forall a. Bounded a => a
    maxBound :: Int)

    intValue :: NatRepr n -> Integer
    intValue :: forall (n :: Natural). NatRepr n -> Integer
    intValue NatRepr n
    n = Natural -> Integer
    forall a. Integral a => a -> Integer
    toInteger (NatRepr n -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr n
    n)
    {-# INLINE intValue #-}

    -- | Return the value of the nat representation.
    widthVal :: NatRepr n -> Int
    widthVal :: forall (n :: Natural). NatRepr n -> Int
    widthVal (NatRepr Natural
    i) | Natural
    i Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Natural
    maxInt = Natural -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    i
                         | Bool
    otherwise   = [Char] -> Int
    forall a. HasCallStack => [Char] -> a
    error ([Char]
    "Width is too large: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Natural -> [Char]
    forall a. Show a => a -> [Char]
    show Natural
    i)

    withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r
    withKnownNat :: forall (n :: Natural) r. NatRepr n -> (KnownNat n => r) -> r
    withKnownNat (NatRepr Natural
    nVal) KnownNat n => r
    v =
      case Natural -> SomeNat
    someNatVal Natural
    nVal of
        SomeNat (Proxy n
    Proxy :: Proxy n') ->
          case n :~: n
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom :: n :~: n' of
            n :~: n
    Refl -> r
    KnownNat n => r
    v

    data IsZeroNat n where
      ZeroNat    :: IsZeroNat 0
      NonZeroNat :: IsZeroNat (n+1)

    isZeroNat :: NatRepr n -> IsZeroNat n
    isZeroNat :: forall (n :: Natural). NatRepr n -> IsZeroNat n
    isZeroNat (NatRepr Natural
    0) = IsZeroNat 0 -> IsZeroNat n
    forall a b. a -> b
    unsafeCoerce IsZeroNat 0
    ZeroNat
    isZeroNat (NatRepr Natural
    _) = IsZeroNat (ZonkAny 4 + 1) -> IsZeroNat n
    forall a b. a -> b
    unsafeCoerce IsZeroNat (ZonkAny 4 + 1)
    forall (n :: Natural). IsZeroNat (n + 1)
    NonZeroNat

    -- | Every nat is either zero or >= 1.
    isZeroOrGT1 :: NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
    isZeroOrGT1 :: forall (n :: Natural). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
    isZeroOrGT1 NatRepr n
    n =
      case NatRepr n -> IsZeroNat n
    forall (n :: Natural). NatRepr n -> IsZeroNat n
    isZeroNat NatRepr n
    n of
        IsZeroNat n
    ZeroNat    -> (n :~: 0) -> Either (n :~: 0) (LeqProof 1 n)
    forall a b. a -> Either a b
    Left n :~: n
    n :~: 0
    forall {k} (a :: k). a :~: a
    Refl
        IsZeroNat n
    NonZeroNat -> LeqProof 1 n -> Either (n :~: 0) (LeqProof 1 n)
    forall a b. b -> Either a b
    Right (LeqProof 1 n -> Either (n :~: 0) (LeqProof 1 n))
    -> LeqProof 1 n -> Either (n :~: 0) (LeqProof 1 n)
    forall a b. (a -> b) -> a -> b
    $
          -- We have n = m + 1 for some m.
          let
            -- | x <= x + 1
            leqPlus :: forall f x y. ((x + 1) ~ y) => f x ->  LeqProof 1 y
            leqPlus :: forall (f :: Natural -> Type) (x :: Natural) (y :: Natural).
    ((x + 1) ~ y) =>
    f x -> LeqProof 1 y
    leqPlus f x
    fx =
              case (f x -> NatRepr 1 -> (x + 1) :~: (1 + x)
    forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> (m + n) :~: (n + m)
    plusComm f x
    fx (forall (n :: Natural). KnownNat n => NatRepr n
    knownNat @1) :: x + 1 :~: 1 + x)    of { (x + 1) :~: (1 + x)
    Refl ->
              case (NatRepr 1 -> f x -> ((1 + x) - x) :~: 1
    forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> ((m + n) - n) :~: m
    plusMinusCancel (forall (n :: Natural). KnownNat n => NatRepr n
    knownNat @1) f x
    fx :: 1+x-x :~: 1) of { ((1 + x) - x) :~: 1
    Refl ->
              case (LeqProof y y
    LeqProof (x + 1) y
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof (x+1) y)                    of { LeqProof (x + 1) y
    LeqProof ->
              case (LeqProof 1 1
    LeqProof ((1 + x) - x) (y - x)
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof (1+x-x) (y-x))              of { LeqProof ((1 + x) - x) (y - x)
    LeqProof ->
                LeqProof 1 1 -> LeqProof 1 y -> LeqProof 1 y
    forall (m :: Natural) (n :: Natural) (p :: Natural).
    LeqProof m n -> LeqProof n p -> LeqProof m p
    leqTrans (LeqProof 1 1
    LeqProof 1 (y - x)
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof 1 (y-x))
                         (LeqProof y y -> LeqProof x y -> LeqProof (y - x) y
    forall (m :: Natural) (n :: Natural) (p :: Natural).
    LeqProof m n -> LeqProof p m -> LeqProof (m - p) n
    leqSub (LeqProof y y
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof y y)
                                 (LeqProof x y -> LeqProof y y -> LeqProof x y
    forall (m :: Natural) (n :: Natural) (p :: Natural).
    LeqProof m n -> LeqProof n p -> LeqProof m p
    leqTrans (Proxy x -> LeqProof x (x + 1)
    forall (f :: Natural -> Type) (z :: Natural).
    f z -> LeqProof z (z + 1)
    leqSucc (Proxy x
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy x))
                                           (LeqProof y y
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof) :: LeqProof x y) :: LeqProof (y - x) y)
              }}}}
          in NatRepr n -> LeqProof 1 n
    forall (f :: Natural -> Type) (x :: Natural) (y :: Natural).
    ((x + 1) ~ y) =>
    f x -> LeqProof 1 y
    leqPlus (NatRepr (n + 1) -> NatRepr n
    forall (n :: Natural). NatRepr (n + 1) -> NatRepr n
    predNat NatRepr n
    NatRepr (n + 1)
    n)

    -- | Decrement a @NatRepr@
    decNat :: (1 <= n) => NatRepr n -> NatRepr (n-1)
    decNat :: forall (n :: Natural). (1 <= n) => NatRepr n -> NatRepr (n - 1)
    decNat (NatRepr Natural
    i) = Natural -> NatRepr (n - 1)
    forall (n :: Natural). Natural -> NatRepr n
    NatRepr (Natural
    iNatural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    -Natural
    1)

    -- | Get the predecessor of a nat
    predNat :: NatRepr (n+1) -> NatRepr n
    predNat :: forall (n :: Natural). NatRepr (n + 1) -> NatRepr n
    predNat (NatRepr Natural
    i) = Natural -> NatRepr n
    forall (n :: Natural). Natural -> NatRepr n
    NatRepr (Natural
    iNatural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    -Natural
    1)

    -- | Increment a @NatRepr@
    incNat :: NatRepr n -> NatRepr (n+1)
    incNat :: forall (n :: Natural). NatRepr n -> NatRepr (n + 1)
    incNat (NatRepr Natural
    x) = Natural -> NatRepr (n + 1)
    forall (n :: Natural). Natural -> NatRepr n
    NatRepr (Natural
    xNatural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    +Natural
    1)

    halfNat :: NatRepr (n+n) -> NatRepr n
    halfNat :: forall (n :: Natural). NatRepr (n + n) -> NatRepr n
    halfNat (NatRepr Natural
    x) = Natural -> NatRepr n
    forall (n :: Natural). Natural -> NatRepr n
    NatRepr (Natural
    x Natural -> Natural -> Natural
    forall a. Integral a => a -> a -> a
    `div` Natural
    2)

    addNat :: NatRepr m -> NatRepr n -> NatRepr (m+n)
    addNat :: forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    addNat (NatRepr Natural
    m) (NatRepr Natural
    n) = Natural -> NatRepr (m + n)
    forall (n :: Natural). Natural -> NatRepr n
    NatRepr (Natural
    mNatural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    +Natural
    n)

    subNat :: (n <= m) => NatRepr m -> NatRepr n -> NatRepr (m-n)
    subNat :: forall (n :: Natural) (m :: Natural).
    (n <= m) =>
    NatRepr m -> NatRepr n -> NatRepr (m - n)
    subNat (NatRepr Natural
    m) (NatRepr Natural
    n) = Natural -> NatRepr (m - n)
    forall (n :: Natural). Natural -> NatRepr n
    NatRepr (Natural
    mNatural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    -Natural
    n)

    divNat :: (1 <= n) => NatRepr (m * n) -> NatRepr n -> NatRepr m
    divNat :: forall (n :: Natural) (m :: Natural).
    (1 <= n) =>
    NatRepr (m * n) -> NatRepr n -> NatRepr m
    divNat (NatRepr Natural
    x) (NatRepr Natural
    y) = Natural -> NatRepr m
    forall (n :: Natural). Natural -> NatRepr n
    NatRepr (Natural -> Natural -> Natural
    forall a. Integral a => a -> a -> a
    div Natural
    x Natural
    y)

    withDivModNat :: forall n m a.
                     NatRepr n
                  -> NatRepr m
                  -> (forall div mod. (n ~ ((div * m) + mod)) =>
                      NatRepr div -> NatRepr mod -> a)
                  -> a
    withDivModNat :: forall (n :: Natural) (m :: Natural) a.
    NatRepr n
    -> NatRepr m
    -> (forall (div :: Natural) (mod :: Natural).
        (n ~ ((div * m) + mod)) =>
        NatRepr div -> NatRepr mod -> a)
    -> a
    withDivModNat NatRepr n
    n NatRepr m
    m forall (div :: Natural) (mod :: Natural).
    (n ~ ((div * m) + mod)) =>
    NatRepr div -> NatRepr mod -> a
    f =
      case ( NatRepr (ZonkAny 2) -> Some NatRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Natural -> NatRepr (ZonkAny 2)
    forall (n :: Natural). Natural -> NatRepr n
    NatRepr Natural
    divPart), NatRepr (ZonkAny 3) -> Some NatRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Natural -> NatRepr (ZonkAny 3)
    forall (n :: Natural). Natural -> NatRepr n
    NatRepr Natural
    modPart)) of
         ( Some (NatRepr x
    divn :: NatRepr div), Some (NatRepr x
    modn :: NatRepr mod) )
           -> case n :~: ((x * m) + x)
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom of
                (n :~: ((x * m) + x)
    Refl :: (n :~: ((div * m) + mod))) -> NatRepr x -> NatRepr x -> a
    forall (div :: Natural) (mod :: Natural).
    (n ~ ((div * m) + mod)) =>
    NatRepr div -> NatRepr mod -> a
    f NatRepr x
    divn NatRepr x
    modn
      where
        (Natural
    divPart, Natural
    modPart) = Natural -> Natural -> (Natural, Natural)
    forall a. Integral a => a -> a -> (a, a)
    divMod (NatRepr n -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr n
    n) (NatRepr m -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr m
    m)

    natMultiply :: NatRepr n -> NatRepr m -> NatRepr (n * m)
    natMultiply :: forall (n :: Natural) (m :: Natural).
    NatRepr n -> NatRepr m -> NatRepr (n * m)
    natMultiply (NatRepr Natural
    n) (NatRepr Natural
    m) = Natural -> NatRepr (n * m)
    forall (n :: Natural). Natural -> NatRepr n
    NatRepr (Natural
    n Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    * Natural
    m)

    ------------------------------------------------------------------------
    -- Operations for using NatRepr as a bitwidth.

    -- | Return minimum unsigned value for bitvector with given width (always 0).
    minUnsigned :: NatRepr w -> Integer
    minUnsigned :: forall (n :: Natural). NatRepr n -> Integer
    minUnsigned NatRepr w
    _ = Integer
    0

    -- | Return maximum unsigned value for bitvector with given width.
    maxUnsigned :: NatRepr w -> Integer
    maxUnsigned :: forall (n :: Natural). NatRepr n -> Integer
    maxUnsigned NatRepr w
    w = Int -> Integer
    forall a. Bits a => Int -> a
    bit (NatRepr w -> Int
    forall (n :: Natural). NatRepr n -> Int
    widthVal NatRepr w
    w) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1

    -- | Return minimum value for bitvector in two's complement with given width.
    minSigned :: (1 <= w) => NatRepr w -> Integer
    minSigned :: forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
    minSigned NatRepr w
    w = Integer -> Integer
    forall a. Num a => a -> a
    negate (Int -> Integer
    forall a. Bits a => Int -> a
    bit (NatRepr w -> Int
    forall (n :: Natural). NatRepr n -> Int
    widthVal NatRepr w
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1))

    -- | Return maximum value for bitvector in two's complement with given width.
    maxSigned :: (1 <= w) => NatRepr w -> Integer
    maxSigned :: forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
    maxSigned NatRepr w
    w = Int -> Integer
    forall a. Bits a => Int -> a
    bit (NatRepr w -> Int
    forall (n :: Natural). NatRepr n -> Int
    widthVal NatRepr w
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1

    -- | @toUnsigned w i@ maps @i@ to a @i `mod` 2^w@.
    toUnsigned :: NatRepr w -> Integer -> Integer
    toUnsigned :: forall (w :: Natural). NatRepr w -> Integer -> Integer
    toUnsigned NatRepr w
    w Integer
    i = NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    maxUnsigned NatRepr w
    w Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. Integer
    i

    -- | @toSigned w i@ interprets the least-significant @w@ bits in @i@ as a
    -- signed number in two's complement notation and returns that value.
    toSigned :: (1 <= w) => NatRepr w -> Integer -> Integer
    toSigned :: forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
    toSigned NatRepr w
    w Integer
    i0
        | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > NatRepr w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
    maxSigned NatRepr w
    w = Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Int -> Integer
    forall a. Bits a => Int -> a
    bit (NatRepr w -> Int
    forall (n :: Natural). NatRepr n -> Int
    widthVal NatRepr w
    w)
        | Bool
    otherwise       = Integer
    i
      where i :: Integer
    i = Integer
    i0 Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    maxUnsigned NatRepr w
    w

    -- | @unsignedClamp w i@ rounds @i@ to the nearest value between
    -- @0@ and @2^w-1@ (inclusive).
    unsignedClamp :: NatRepr w -> Integer -> Integer
    unsignedClamp :: forall (w :: Natural). NatRepr w -> Integer -> Integer
    unsignedClamp NatRepr w
    w Integer
    i
      | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    minUnsigned NatRepr w
    w = NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    minUnsigned NatRepr w
    w
      | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    maxUnsigned NatRepr w
    w = NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    maxUnsigned NatRepr w
    w
      | Bool
    otherwise         = Integer
    i

    -- | @signedClamp w i@ rounds @i@ to the nearest value between
    -- @-2^(w-1)@ and @2^(w-1)-1@ (inclusive).
    signedClamp :: (1 <= w) => NatRepr w -> Integer -> Integer
    signedClamp :: forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
    signedClamp NatRepr w
    w Integer
    i
      | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
    minSigned NatRepr w
    w = NatRepr w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
    minSigned NatRepr w
    w
      | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > NatRepr w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
    maxSigned NatRepr w
    w = NatRepr w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
    maxSigned NatRepr w
    w
      | Bool
    otherwise       = Integer
    i

    ------------------------------------------------------------------------
    -- Some NatRepr

    -- | Turn an @Integral@ value into a @NatRepr@.  Returns @Nothing@
    --   if the given value is negative.
    someNat :: Integral a => a -> Maybe (Some NatRepr)
    someNat :: forall a. Integral a => a -> Maybe (Some NatRepr)
    someNat a
    x | a
    x a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    >= a
    0 = Some NatRepr -> Maybe (Some NatRepr)
    forall a. a -> Maybe a
    Just (Some NatRepr -> Maybe (Some NatRepr))
    -> (Natural -> Some NatRepr) -> Natural -> Maybe (Some NatRepr)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NatRepr (ZonkAny 1) -> Some NatRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (NatRepr (ZonkAny 1) -> Some NatRepr)
    -> (Natural -> NatRepr (ZonkAny 1)) -> Natural -> Some NatRepr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Natural -> NatRepr (ZonkAny 1)
    forall (n :: Natural). Natural -> NatRepr n
    NatRepr (Natural -> Maybe (Some NatRepr))
    -> Natural -> Maybe (Some NatRepr)
    forall a b. (a -> b) -> a -> b
    $! a -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral a
    x
    someNat a
    _ = Maybe (Some NatRepr)
    forall a. Maybe a
    Nothing

    -- | Turn a @Natural@ into the corresponding @NatRepr@
    mkNatRepr :: Natural -> Some NatRepr
    mkNatRepr :: Natural -> Some NatRepr
    mkNatRepr Natural
    n = NatRepr (ZonkAny 0) -> Some NatRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Natural -> NatRepr (ZonkAny 0)
    forall (n :: Natural). Natural -> NatRepr n
    NatRepr Natural
    n)

    -- | Return the maximum of two nat representations.
    maxNat :: NatRepr m -> NatRepr n -> Some NatRepr
    maxNat :: forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> Some NatRepr
    maxNat NatRepr m
    x NatRepr n
    y
      | NatRepr m -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr m
    x Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    >= NatRepr n -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr n
    y = NatRepr m -> Some NatRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some NatRepr m
    x
      | Bool
    otherwise = NatRepr n -> Some NatRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some NatRepr n
    y

    ------------------------------------------------------------------------
    -- Arithmetic

    -- | Produce evidence that @+@ is commutative.
    plusComm :: forall f m g n . f m -> g n -> m+n :~: n+m
    plusComm :: forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> (m + n) :~: (n + m)
    plusComm f m
    _ g n
    _ = (m + n) :~: (n + m)
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom

    -- | Produce evidence that @+@ is associative.
    plusAssoc :: forall f m g n h o . f m -> g n -> h o -> m+(n+o) :~: (m+n)+o
    plusAssoc :: forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural) (h :: Natural -> Type) (o :: Natural).
    f m -> g n -> h o -> (m + (n + o)) :~: ((m + n) + o)
    plusAssoc f m
    _ g n
    _ h o
    _ = (m + (n + o)) :~: ((m + n) + o)
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom

    -- | Produce evidence that @*@ is commutative.
    mulComm :: forall f m g n. f m -> g n -> (m * n) :~: (n * m)
    mulComm :: forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> (m * n) :~: (n * m)
    mulComm f m
    _ g n
    _ = (m * n) :~: (n * m)
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom

    mul2Plus :: forall f n. f n -> (n + n) :~: (2 * n)
    mul2Plus :: forall (f :: Natural -> Type) (n :: Natural).
    f n -> (n + n) :~: (2 * n)
    mul2Plus f n
    n = case Proxy 1 -> Proxy 1 -> f n -> ((1 * n) + (1 * n)) :~: ((1 + 1) * n)
    forall (n :: Natural) (m :: Natural) (p :: Natural)
           (f :: Natural -> Type) (g :: Natural -> Type)
           (h :: Natural -> Type).
    f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p)
    addMulDistribRight (forall (t :: Natural). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @1) (forall (t :: Natural). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @1) f n
    n of
                   ((1 * n) + (1 * n)) :~: ((1 + 1) * n)
    Refl -> (n + n) :~: (n + n)
    (n + n) :~: (2 * n)
    forall {k} (a :: k). a :~: a
    Refl

    -- | Cancel an add followed by a subtract
    plusMinusCancel :: forall f m g n . f m -> g n -> (m + n) - n :~: m
    plusMinusCancel :: forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> ((m + n) - n) :~: m
    plusMinusCancel f m
    _ g n
    _ = ((m + n) - n) :~: m
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom

    minusPlusCancel :: forall f m g n . (n <= m) => f m -> g n -> (m - n) + n :~: m
    minusPlusCancel :: forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    (n <= m) =>
    f m -> g n -> ((m - n) + n) :~: m
    minusPlusCancel f m
    _ g n
    _ = ((m - n) + n) :~: m
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom

    addMulDistribRight :: forall n m p f g h. f n -> g m -> h p
                        -> ((n * p) + (m * p)) :~: ((n + m) * p)
    addMulDistribRight :: forall (n :: Natural) (m :: Natural) (p :: Natural)
           (f :: Natural -> Type) (g :: Natural -> Type)
           (h :: Natural -> Type).
    f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p)
    addMulDistribRight f n
    _n g m
    _m h p
    _p = ((n * p) + (m * p)) :~: ((n + m) * p)
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom

    withAddMulDistribRight :: forall n m p f g h a. f n -> g m -> h p
                        -> ( (((n * p) + (m * p)) ~ ((n + m) * p)) => a) -> a
    withAddMulDistribRight :: forall (n :: Natural) (m :: Natural) (p :: Natural)
           (f :: Natural -> Type) (g :: Natural -> Type)
           (h :: Natural -> Type) a.
    f n
    -> g m -> h p -> ((((n * p) + (m * p)) ~ ((n + m) * p)) => a) -> a
    withAddMulDistribRight f n
    n g m
    m h p
    p (((n * p) + (m * p)) ~ ((n + m) * p)) => a
    f =
      case f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p)
    forall (n :: Natural) (m :: Natural) (p :: Natural)
           (f :: Natural -> Type) (g :: Natural -> Type)
           (h :: Natural -> Type).
    f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p)
    addMulDistribRight f n
    n g m
    m h p
    p of
        ((n * p) + (m * p)) :~: ((n + m) * p)
    Refl -> a
    (((n * p) + (m * p)) ~ ((n + m) * p)) => a
    f

    withSubMulDistribRight :: forall n m p f g h a. (m <= n) => f n -> g m -> h p
                        -> ( (((n * p) - (m * p)) ~ ((n - m) * p)) => a) -> a
    withSubMulDistribRight :: forall (n :: Natural) (m :: Natural) (p :: Natural)
           (f :: Natural -> Type) (g :: Natural -> Type)
           (h :: Natural -> Type) a.
    (m <= n) =>
    f n
    -> g m -> h p -> ((((n * p) - (m * p)) ~ ((n - m) * p)) => a) -> a
    withSubMulDistribRight f n
    _n g m
    _m h p
    _p (((n * p) - (m * p)) ~ ((n - m) * p)) => a
    f =
      case ((n * p) - (m * p)) :~: ((n - m) * p)
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom of
        (((n * p) - (m * p)) :~: ((n - m) * p)
    Refl :: (((n * p) - (m * p)) :~: ((n - m) * p)) ) -> a
    (((n * p) - (m * p)) ~ ((n - m) * p)) => a
    f

    ------------------------------------------------------------------------
    -- LeqProof

    -- | @LeqProof m n@ is a type whose values are only inhabited when @m@
    -- is less than or equal to @n@.
    data LeqProof (m :: Nat) (n :: Nat) where
      LeqProof :: (m <= n) => LeqProof m n

    -- | (<=) is a decidable relation on nats.
    decideLeq :: NatRepr a -> NatRepr b -> Either (LeqProof a b) ((LeqProof a b) -> Void)
    decideLeq :: forall (a :: Natural) (b :: Natural).
    NatRepr a
    -> NatRepr b -> Either (LeqProof a b) (LeqProof a b -> Void)
    decideLeq (NatRepr Natural
    m) (NatRepr Natural
    n)
      | Natural
    m Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Natural
    n    = LeqProof a b -> Either (LeqProof a b) (LeqProof a b -> Void)
    forall a b. a -> Either a b
    Left (LeqProof a b -> Either (LeqProof a b) (LeqProof a b -> Void))
    -> LeqProof a b -> Either (LeqProof a b) (LeqProof a b -> Void)
    forall a b. (a -> b) -> a -> b
    $ LeqProof 0 0 -> LeqProof a b
    forall a b. a -> b
    unsafeCoerce (LeqProof 0 0
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof 0 0)
      | Bool
    otherwise = (LeqProof a b -> Void)
    -> Either (LeqProof a b) (LeqProof a b -> Void)
    forall a b. b -> Either a b
    Right ((LeqProof a b -> Void)
     -> Either (LeqProof a b) (LeqProof a b -> Void))
    -> (LeqProof a b -> Void)
    -> Either (LeqProof a b) (LeqProof a b -> Void)
    forall a b. (a -> b) -> a -> b
    $
          \LeqProof a b
    x -> LeqProof a b -> Void -> Void
    forall a b. a -> b -> b
    seq LeqProof a b
    x (Void -> Void) -> Void -> Void
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Void
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "Impossible [decidable <= on NatRepr]"

    testStrictLeq :: forall m n
                   . (m <= n)
                  => NatRepr m
                  -> NatRepr n
                  -> Either (LeqProof (m+1) n) (m :~: n)
    testStrictLeq :: forall (m :: Natural) (n :: Natural).
    (m <= n) =>
    NatRepr m -> NatRepr n -> Either (LeqProof (m + 1) n) (m :~: n)
    testStrictLeq (NatRepr Natural
    m) (NatRepr Natural
    n)
      | Natural
    m Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    < Natural
    n = LeqProof (m + 1) n -> Either (LeqProof (m + 1) n) (m :~: n)
    forall a b. a -> Either a b
    Left (LeqProof 0 0 -> LeqProof (m + 1) n
    forall a b. a -> b
    unsafeCoerce (LeqProof 0 0
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof 0 0))
      | Bool
    otherwise = (m :~: n) -> Either (LeqProof (m + 1) n) (m :~: n)
    forall a b. b -> Either a b
    Right m :~: n
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom
    {-# NOINLINE testStrictLeq #-}

    -- As for NatComparison above, but works with LeqProof
    data NatCases m n where
      -- First number is less than second.
      NatCaseLT :: LeqProof (m+1) n -> NatCases m n
      NatCaseEQ :: NatCases m m
      -- First number is greater than second.
      NatCaseGT :: LeqProof (n+1) m -> NatCases m n

    testNatCases ::  forall m n
                  . NatRepr m
                 -> NatRepr n
                 -> NatCases m n
    testNatCases :: forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> NatCases m n
    testNatCases NatRepr m
    m NatRepr n
    n =
      case Natural -> Natural -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (NatRepr m -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr m
    m) (NatRepr n -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr n
    n) of
        Ordering
    LT -> LeqProof (m + 1) n -> NatCases m n
    forall (m :: Natural) (n :: Natural).
    LeqProof (m + 1) n -> NatCases m n
    NatCaseLT (LeqProof 0 0 -> LeqProof (m + 1) n
    forall a b. a -> b
    unsafeCoerce (LeqProof 0 0
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof 0 0))
        Ordering
    EQ -> NatCases m m -> NatCases m n
    forall a b. a -> b
    unsafeCoerce (NatCases m m -> NatCases m n) -> NatCases m m -> NatCases m n
    forall a b. (a -> b) -> a -> b
    $ (NatCases m m
    forall (m :: Natural). NatCases m m
    NatCaseEQ :: NatCases m m)
        Ordering
    GT -> LeqProof (n + 1) m -> NatCases m n
    forall (n :: Natural) (m :: Natural).
    LeqProof (n + 1) m -> NatCases m n
    NatCaseGT (LeqProof 0 0 -> LeqProof (n + 1) m
    forall a b. a -> b
    unsafeCoerce (LeqProof 0 0
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof 0 0))
    {-# NOINLINE testNatCases #-}

    -- | The strict order (\<), defined by n \< m \<-> n + 1 \<= m, is irreflexive.
    lessThanIrreflexive :: forall f (a :: Nat). f a -> LeqProof (1 + a) a -> Void
    lessThanIrreflexive :: forall (f :: Natural -> Type) (a :: Natural).
    f a -> LeqProof (1 + a) a -> Void
    lessThanIrreflexive f a
    a LeqProof (1 + a) a
    prf =
      let prf1 :: LeqProof (1 + a - a) (a - a)
          prf1 :: LeqProof ((1 + a) - a) (a - a)
    prf1 = LeqProof (1 + a) a
    -> LeqProof a a -> LeqProof ((1 + a) - a) (a - a)
    forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
           (y_h :: Natural).
    LeqProof x_l x_h
    -> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)
    leqSub2 LeqProof (1 + a) a
    prf (LeqProof a a
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof a a)
          prf2 :: 1 + a - a :~: 1
          prf2 :: ((1 + a) - a) :~: 1
    prf2 = NatRepr 1 -> f a -> ((1 + a) - a) :~: 1
    forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> ((m + n) - n) :~: m
    plusMinusCancel (forall (n :: Natural). KnownNat n => NatRepr n
    knownNat @1) f a
    a
          prf3 :: a - a :~: 0
          prf3 :: (a - a) :~: 0
    prf3 = NatRepr 0 -> f a -> ((0 + a) - a) :~: 0
    forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> ((m + n) - n) :~: m
    plusMinusCancel (forall (n :: Natural). KnownNat n => NatRepr n
    knownNat @0) f a
    a
          prf4 :: LeqProof 1 0
          prf4 :: LeqProof 1 0
    prf4 = case ((1 + a) - a) :~: 1
    prf2 of ((1 + a) - a) :~: 1
    Refl -> case (a - a) :~: 0
    prf3 of { (a - a) :~: 0
    Refl -> LeqProof 1 0
    LeqProof ((1 + a) - a) (a - a)
    prf1 }
      in case LeqProof 1 0
    prf4 of {}

    -- | The strict order on the naturals is asymmetric
    lessThanAsymmetric :: forall m f n
                        . LeqProof (n+1) m
                       -> LeqProof (m+1) n
                       -> f n
                       -> Void
    lessThanAsymmetric :: forall (m :: Natural) (f :: Natural -> Type) (n :: Natural).
    LeqProof (n + 1) m -> LeqProof (m + 1) n -> f n -> Void
    lessThanAsymmetric LeqProof (n + 1) m
    nLTm LeqProof (m + 1) n
    mLTn f n
    n =
      case f n -> NatRepr 1 -> (n + 1) :~: (1 + n)
    forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> (m + n) :~: (n + m)
    plusComm f n
    n (forall (n :: Natural). KnownNat n => NatRepr n
    knownNat @1) :: n + 1 :~: 1 + n of { (n + 1) :~: (1 + n)
    Refl ->
      case LeqProof m m -> NatRepr 1 -> LeqProof m (m + 1)
    forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
           (p :: Natural).
    LeqProof m n -> f p -> LeqProof m (n + p)
    leqAdd (LeqProof m m
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof m m) (forall (n :: Natural). KnownNat n => NatRepr n
    knownNat @1) :: LeqProof m (m+1) of
        LeqProof m (m + 1)
    LeqProof -> f n -> LeqProof (1 + n) n -> Void
    forall (f :: Natural -> Type) (a :: Natural).
    f a -> LeqProof (1 + a) a -> Void
    lessThanIrreflexive f n
    n (LeqProof (1 + n) n -> Void) -> LeqProof (1 + n) n -> Void
    forall a b. (a -> b) -> a -> b
    $ LeqProof (n + 1) (m + 1)
    -> LeqProof (m + 1) n -> LeqProof (n + 1) n
    forall (m :: Natural) (n :: Natural) (p :: Natural).
    LeqProof m n -> LeqProof n p -> LeqProof m p
    leqTrans (LeqProof (n + 1) m
    -> LeqProof m (m + 1) -> LeqProof (n + 1) (m + 1)
    forall (m :: Natural) (n :: Natural) (p :: Natural).
    LeqProof m n -> LeqProof n p -> LeqProof m p
    leqTrans LeqProof (n + 1) m
    nLTm LeqProof m (m + 1)
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof) LeqProof (m + 1) n
    mLTn
      }

    -- | @x `testLeq` y@ checks whether @x@ is less than or equal to @y@.
    testLeq :: forall m n . NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
    testLeq :: forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
    testLeq (NatRepr Natural
    m) (NatRepr Natural
    n)
       | Natural
    m Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Natural
    n    = LeqProof m n -> Maybe (LeqProof m n)
    forall a. a -> Maybe a
    Just (LeqProof 0 0 -> LeqProof m n
    forall a b. a -> b
    unsafeCoerce (LeqProof 0 0
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof 0 0))
       | Bool
    otherwise = Maybe (LeqProof m n)
    forall a. Maybe a
    Nothing
    {-# NOINLINE testLeq #-}

    -- | Apply reflexivity to LeqProof
    leqRefl :: forall f n . f n -> LeqProof n n
    leqRefl :: forall (f :: Natural -> Type) (n :: Natural). f n -> LeqProof n n
    leqRefl f n
    _ = LeqProof n n
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof

    leqSucc :: forall f z. f z -> LeqProof z (z + 1)
    leqSucc :: forall (f :: Natural -> Type) (z :: Natural).
    f z -> LeqProof z (z + 1)
    leqSucc f z
    fz = LeqProof z z -> NatRepr 1 -> LeqProof z (z + 1)
    forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
           (p :: Natural).
    LeqProof m n -> f p -> LeqProof m (n + p)
    leqAdd (f z -> LeqProof z z
    forall (f :: Natural -> Type) (n :: Natural). f n -> LeqProof n n
    leqRefl f z
    fz :: LeqProof z z) (forall (n :: Natural). KnownNat n => NatRepr n
    knownNat @1)

    -- | Apply transitivity to LeqProof
    leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p
    leqTrans :: forall (m :: Natural) (n :: Natural) (p :: Natural).
    LeqProof m n -> LeqProof n p -> LeqProof m p
    leqTrans LeqProof m n
    LeqProof LeqProof n p
    LeqProof = LeqProof 0 0 -> LeqProof m p
    forall a b. a -> b
    unsafeCoerce (LeqProof 0 0
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof 0 0)
    {-# NOINLINE leqTrans #-}

    -- | Zero is less than or equal to any 'Nat'.
    leqZero :: LeqProof 0 n
    leqZero :: forall (n :: Natural). LeqProof 0 n
    leqZero = LeqProof 0 0 -> LeqProof 0 n
    forall a b. a -> b
    unsafeCoerce (LeqProof 0 0
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof 0 0)

    -- | Add both sides of two inequalities
    leqAdd2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
    leqAdd2 :: forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
           (y_h :: Natural).
    LeqProof x_l x_h
    -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
    leqAdd2 LeqProof x_l x_h
    x LeqProof y_l y_h
    y = LeqProof x_l x_h
    -> LeqProof (x_l + y_l) (x_h + y_h)
    -> LeqProof (x_l + y_l) (x_h + y_h)
    forall a b. a -> b -> b
    seq LeqProof x_l x_h
    x (LeqProof (x_l + y_l) (x_h + y_h)
     -> LeqProof (x_l + y_l) (x_h + y_h))
    -> LeqProof (x_l + y_l) (x_h + y_h)
    -> LeqProof (x_l + y_l) (x_h + y_h)
    forall a b. (a -> b) -> a -> b
    $ LeqProof y_l y_h
    -> LeqProof (x_l + y_l) (x_h + y_h)
    -> LeqProof (x_l + y_l) (x_h + y_h)
    forall a b. a -> b -> b
    seq LeqProof y_l y_h
    y (LeqProof (x_l + y_l) (x_h + y_h)
     -> LeqProof (x_l + y_l) (x_h + y_h))
    -> LeqProof (x_l + y_l) (x_h + y_h)
    -> LeqProof (x_l + y_l) (x_h + y_h)
    forall a b. (a -> b) -> a -> b
    $ LeqProof 0 0 -> LeqProof (x_l + y_l) (x_h + y_h)
    forall a b. a -> b
    unsafeCoerce (LeqProof 0 0
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof 0 0)
    {-# NOINLINE leqAdd2 #-}

    -- | Subtract sides of two inequalities.
    leqSub2 :: LeqProof x_l x_h
            -> LeqProof y_l y_h
            -> LeqProof (x_l-y_h) (x_h-y_l)
    leqSub2 :: forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
           (y_h :: Natural).
    LeqProof x_l x_h
    -> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)
    leqSub2 LeqProof x_l x_h
    LeqProof LeqProof y_l y_h
    LeqProof = LeqProof 0 0 -> LeqProof (x_l - y_h) (x_h - y_l)
    forall a b. a -> b
    unsafeCoerce (LeqProof 0 0
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof 0 0)
    {-# NOINLINE leqSub2 #-}

    ------------------------------------------------------------------------
    -- LeqProof combinators

    -- | Create a leqProof using two proxies
    leqProof :: (m <= n) => f m -> g n -> LeqProof m n
    leqProof :: forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
           (g :: Natural -> Type).
    (m <= n) =>
    f m -> g n -> LeqProof m n
    leqProof f m
    _ g n
    _ = LeqProof m n
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof

    withLeqProof :: LeqProof m n -> ((m <= n) => a) -> a
    withLeqProof :: forall (m :: Natural) (n :: Natural) a.
    LeqProof m n -> ((m <= n) => a) -> a
    withLeqProof LeqProof m n
    p (m <= n) => a
    a =
      case LeqProof m n
    p of
        LeqProof m n
    LeqProof -> a
    (m <= n) => a
    a

    -- | Test whether natural number is positive.
    isPosNat :: NatRepr n -> Maybe (LeqProof 1 n)
    isPosNat :: forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
    isPosNat = NatRepr 1 -> NatRepr n -> Maybe (LeqProof 1 n)
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
    testLeq (NatRepr 1
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat :: NatRepr 1)

    -- | Congruence rule for multiplication
    leqMulCongr :: LeqProof a x
                -> LeqProof b y
                -> LeqProof (a*b) (x*y)
    leqMulCongr :: forall (a :: Natural) (x :: Natural) (b :: Natural) (y :: Natural).
    LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)
    leqMulCongr LeqProof a x
    LeqProof LeqProof b y
    LeqProof = LeqProof 1 1 -> LeqProof (a * b) (x * y)
    forall a b. a -> b
    unsafeCoerce (LeqProof 1 1
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof 1 1)
    {-# NOINLINE leqMulCongr #-}

    -- | Multiplying two positive numbers results in a positive number.
    leqMulPos :: forall p q x y
              .  (1 <= x, 1 <= y)
              => p x
              -> q y
              -> LeqProof 1 (x*y)
    leqMulPos :: forall (p :: Natural -> Type) (q :: Natural -> Type) (x :: Natural)
           (y :: Natural).
    (1 <= x, 1 <= y) =>
    p x -> q y -> LeqProof 1 (x * y)
    leqMulPos p x
    _ q y
    _ = LeqProof 1 x -> LeqProof 1 y -> LeqProof (1 * 1) (x * y)
    forall (a :: Natural) (x :: Natural) (b :: Natural) (y :: Natural).
    LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)
    leqMulCongr (LeqProof 1 x
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof 1 x) (LeqProof 1 y
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof 1 y)

    leqMulMono :: (1 <= x) => p x -> q y -> LeqProof y (x * y)
    leqMulMono :: forall (x :: Natural) (p :: Natural -> Type) (q :: Natural -> Type)
           (y :: Natural).
    (1 <= x) =>
    p x -> q y -> LeqProof y (x * y)
    leqMulMono p x
    x q y
    y = LeqProof 1 x -> LeqProof y y -> LeqProof (1 * y) (x * y)
    forall (a :: Natural) (x :: Natural) (b :: Natural) (y :: Natural).
    LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)
    leqMulCongr (Proxy 1 -> p x -> LeqProof 1 x
    forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
           (g :: Natural -> Type).
    (m <= n) =>
    f m -> g n -> LeqProof m n
    leqProof (Proxy 1
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy 1) p x
    x) (q y -> LeqProof y y
    forall (f :: Natural -> Type) (n :: Natural). f n -> LeqProof n n
    leqRefl q y
    y)

    -- | Produce proof that adding a value to the larger element in an LeqProof
    -- is larger
    leqAdd :: forall f m n p . LeqProof m n -> f p -> LeqProof m (n+p)
    leqAdd :: forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
           (p :: Natural).
    LeqProof m n -> f p -> LeqProof m (n + p)
    leqAdd LeqProof m n
    x f p
    _ = LeqProof m n -> LeqProof 0 p -> LeqProof (m + 0) (n + p)
    forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
           (y_h :: Natural).
    LeqProof x_l x_h
    -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
    leqAdd2 LeqProof m n
    x (forall (n :: Natural). LeqProof 0 n
    leqZero @p)

    leqAddPos :: (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n)
    leqAddPos :: forall (m :: Natural) (n :: Natural) (p :: Natural -> Type)
           (q :: Natural -> Type).
    (1 <= m, 1 <= n) =>
    p m -> q n -> LeqProof 1 (m + n)
    leqAddPos p m
    m q n
    n = LeqProof 1 m -> q n -> LeqProof 1 (m + n)
    forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
           (p :: Natural).
    LeqProof m n -> f p -> LeqProof m (n + p)
    leqAdd (Proxy 1 -> p m -> LeqProof 1 m
    forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
           (g :: Natural -> Type).
    (m <= n) =>
    f m -> g n -> LeqProof m n
    leqProof (Proxy 1
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy 1) p m
    m) q n
    n

    -- | Produce proof that subtracting a value from the smaller element is smaller.
    leqSub :: forall m n p . LeqProof m n -> LeqProof p m -> LeqProof (m-p) n
    leqSub :: forall (m :: Natural) (n :: Natural) (p :: Natural).
    LeqProof m n -> LeqProof p m -> LeqProof (m - p) n
    leqSub LeqProof m n
    x LeqProof p m
    _ = LeqProof m n -> LeqProof 0 p -> LeqProof (m - p) (n - 0)
    forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
           (y_h :: Natural).
    LeqProof x_l x_h
    -> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)
    leqSub2 LeqProof m n
    x (forall (n :: Natural). LeqProof 0 n
    leqZero @p)

    addIsLeq :: f n -> g m -> LeqProof n (n + m)
    addIsLeq :: forall (f :: Natural -> Type) (n :: Natural) (g :: Natural -> Type)
           (m :: Natural).
    f n -> g m -> LeqProof n (n + m)
    addIsLeq f n
    n g m
    m = LeqProof n n -> g m -> LeqProof n (n + m)
    forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
           (p :: Natural).
    LeqProof m n -> f p -> LeqProof m (n + p)
    leqAdd (f n -> LeqProof n n
    forall (f :: Natural -> Type) (n :: Natural). f n -> LeqProof n n
    leqRefl f n
    n) g m
    m

    addPrefixIsLeq :: f m -> g n -> LeqProof n (m + n)
    addPrefixIsLeq :: forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> LeqProof n (m + n)
    addPrefixIsLeq f m
    m g n
    n =
      case g n -> f m -> (n + m) :~: (m + n)
    forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> (m + n) :~: (n + m)
    plusComm g n
    n f m
    m of
        (n + m) :~: (m + n)
    Refl -> g n -> f m -> LeqProof n (n + m)
    forall (f :: Natural -> Type) (n :: Natural) (g :: Natural -> Type)
           (m :: Natural).
    f n -> g m -> LeqProof n (n + m)
    addIsLeq g n
    n f m
    m

    dblPosIsPos :: forall n . LeqProof 1 n -> LeqProof 1 (n+n)
    dblPosIsPos :: forall (n :: Natural). LeqProof 1 n -> LeqProof 1 (n + n)
    dblPosIsPos LeqProof 1 n
    x = LeqProof 1 n -> Proxy n -> LeqProof 1 (n + n)
    forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
           (p :: Natural).
    LeqProof m n -> f p -> LeqProof m (n + p)
    leqAdd LeqProof 1 n
    x Proxy n
    forall {k} (t :: k). Proxy t
    Proxy

    addIsLeqLeft1 :: forall n n' m . LeqProof (n + n') m -> LeqProof n m
    addIsLeqLeft1 :: forall (n :: Natural) (n' :: Natural) (m :: Natural).
    LeqProof (n + n') m -> LeqProof n m
    addIsLeqLeft1 LeqProof (n + n') m
    p =
        case Proxy n -> Proxy n' -> ((n + n') - n') :~: n
    forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> ((m + n) - n) :~: m
    plusMinusCancel Proxy n
    n Proxy n'
    n' of
          ((n + n') - n') :~: n
    Refl -> LeqProof (n + n') m
    -> LeqProof n' (n + n') -> LeqProof ((n + n') - n') m
    forall (m :: Natural) (n :: Natural) (p :: Natural).
    LeqProof m n -> LeqProof p m -> LeqProof (m - p) n
    leqSub LeqProof (n + n') m
    p LeqProof n' (n + n')
    le
      where n :: Proxy n
            n :: Proxy n
    n = Proxy n
    forall {k} (t :: k). Proxy t
    Proxy
            n' :: Proxy n'
            n' :: Proxy n'
    n' = Proxy n'
    forall {k} (t :: k). Proxy t
    Proxy
            le :: LeqProof n' (n + n')
            le :: LeqProof n' (n + n')
    le = Proxy n -> Proxy n' -> LeqProof n' (n + n')
    forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> LeqProof n (m + n)
    addPrefixIsLeq Proxy n
    n Proxy n'
    n'

    {-# INLINE withAddPrefixLeq #-}
    withAddPrefixLeq :: NatRepr n -> NatRepr m -> ((m <= n + m) => a) -> a
    withAddPrefixLeq :: forall (n :: Natural) (m :: Natural) a.
    NatRepr n -> NatRepr m -> ((m <= (n + m)) => a) -> a
    withAddPrefixLeq NatRepr n
    n NatRepr m
    m = LeqProof m (n + m) -> ((m <= (n + m)) => a) -> a
    forall (m :: Natural) (n :: Natural) a.
    LeqProof m n -> ((m <= n) => a) -> a
    withLeqProof (NatRepr n -> NatRepr m -> LeqProof m (n + m)
    forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> LeqProof n (m + n)
    addPrefixIsLeq NatRepr n
    n NatRepr m
    m)

    withAddLeq :: forall n m a. NatRepr n -> NatRepr m -> ((n <= n + m) => NatRepr (n + m) -> a) -> a
    withAddLeq :: forall (n :: Natural) (m :: Natural) a.
    NatRepr n
    -> NatRepr m -> ((n <= (n + m)) => NatRepr (n + m) -> a) -> a
    withAddLeq NatRepr n
    n NatRepr m
    m (n <= (n + m)) => NatRepr (n + m) -> a
    f = LeqProof n (n + m) -> ((n <= (n + m)) => a) -> a
    forall (m :: Natural) (n :: Natural) a.
    LeqProof m n -> ((m <= n) => a) -> a
    withLeqProof (NatRepr n -> NatRepr m -> LeqProof n (n + m)
    forall (f :: Natural -> Type) (n :: Natural) (g :: Natural -> Type)
           (m :: Natural).
    f n -> g m -> LeqProof n (n + m)
    addIsLeq NatRepr n
    n NatRepr m
    m) ((n <= (n + m)) => NatRepr (n + m) -> a
    NatRepr (n + m) -> a
    f (NatRepr n -> NatRepr m -> NatRepr (n + m)
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    addNat NatRepr n
    n NatRepr m
    m))

    natForEach' :: forall l h a
                . NatRepr l
                -> NatRepr h
                -> (forall n. LeqProof l n -> LeqProof n h -> NatRepr n -> a)
                -> [a]
    natForEach' :: forall (l :: Natural) (h :: Natural) a.
    NatRepr l
    -> NatRepr h
    -> (forall (n :: Natural).
        LeqProof l n -> LeqProof n h -> NatRepr n -> a)
    -> [a]
    natForEach' NatRepr l
    l NatRepr h
    h forall (n :: Natural).
    LeqProof l n -> LeqProof n h -> NatRepr n -> a
    f
      | Just LeqProof l h
    LeqProof  <- NatRepr l -> NatRepr h -> Maybe (LeqProof l h)
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
    testLeq NatRepr l
    l NatRepr h
    h =
        let f' :: forall n. LeqProof (l + 1) n -> LeqProof n h -> NatRepr n -> a
            f' :: forall (n :: Natural).
    LeqProof (l + 1) n -> LeqProof n h -> NatRepr n -> a
    f' = \LeqProof (l + 1) n
    lp LeqProof n h
    hp -> LeqProof l n -> LeqProof n h -> NatRepr n -> a
    forall (n :: Natural).
    LeqProof l n -> LeqProof n h -> NatRepr n -> a
    f (LeqProof (l + 1) n -> LeqProof l n
    forall (n :: Natural) (n' :: Natural) (m :: Natural).
    LeqProof (n + n') m -> LeqProof n m
    addIsLeqLeft1 LeqProof (l + 1) n
    lp) LeqProof n h
    hp
         in LeqProof l l -> LeqProof l h -> NatRepr l -> a
    forall (n :: Natural).
    LeqProof l n -> LeqProof n h -> NatRepr n -> a
    f LeqProof l l
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof LeqProof l h
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof NatRepr l
    l a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : NatRepr (l + 1)
    -> NatRepr h
    -> (forall (n :: Natural).
        LeqProof (l + 1) n -> LeqProof n h -> NatRepr n -> a)
    -> [a]
    forall (l :: Natural) (h :: Natural) a.
    NatRepr l
    -> NatRepr h
    -> (forall (n :: Natural).
        LeqProof l n -> LeqProof n h -> NatRepr n -> a)
    -> [a]
    natForEach' (NatRepr l -> NatRepr (l + 1)
    forall (n :: Natural). NatRepr n -> NatRepr (n + 1)
    incNat NatRepr l
    l) NatRepr h
    h LeqProof (l + 1) n -> LeqProof n h -> NatRepr n -> a
    forall (n :: Natural).
    LeqProof (l + 1) n -> LeqProof n h -> NatRepr n -> a
    f'
      | Bool
    otherwise             = []

    -- | Apply a function to each element in a range; return the list of values
    -- obtained.
    natForEach :: forall l h a
                . NatRepr l
               -> NatRepr h
               -> (forall n. (l <= n, n <= h) => NatRepr n -> a)
               -> [a]
    natForEach :: forall (l :: Natural) (h :: Natural) a.
    NatRepr l
    -> NatRepr h
    -> (forall (n :: Natural). (l <= n, n <= h) => NatRepr n -> a)
    -> [a]
    natForEach NatRepr l
    l NatRepr h
    h forall (n :: Natural). (l <= n, n <= h) => NatRepr n -> a
    f = NatRepr l
    -> NatRepr h
    -> (forall (n :: Natural).
        LeqProof l n -> LeqProof n h -> NatRepr n -> a)
    -> [a]
    forall (l :: Natural) (h :: Natural) a.
    NatRepr l
    -> NatRepr h
    -> (forall (n :: Natural).
        LeqProof l n -> LeqProof n h -> NatRepr n -> a)
    -> [a]
    natForEach' NatRepr l
    l NatRepr h
    h (\LeqProof l n
    LeqProof LeqProof n h
    LeqProof -> NatRepr n -> a
    forall (n :: Natural). (l <= n, n <= h) => NatRepr n -> a
    f)

    -- | Apply a function to each element in a range starting at zero;
    -- return the list of values obtained.
    natFromZero :: forall h a
                . NatRepr h
               -> (forall n. (n <= h) => NatRepr n -> a)
               -> [a]
    natFromZero :: forall (h :: Natural) a.
    NatRepr h
    -> (forall (n :: Natural). (n <= h) => NatRepr n -> a) -> [a]
    natFromZero NatRepr h
    h forall (n :: Natural). (n <= h) => NatRepr n -> a
    f = NatRepr 0
    -> NatRepr h
    -> (forall (n :: Natural). (0 <= n, n <= h) => NatRepr n -> a)
    -> [a]
    forall (l :: Natural) (h :: Natural) a.
    NatRepr l
    -> NatRepr h
    -> (forall (n :: Natural). (l <= n, n <= h) => NatRepr n -> a)
    -> [a]
    natForEach (forall (n :: Natural). KnownNat n => NatRepr n
    knownNat @0) NatRepr h
    h NatRepr n -> a
    forall (n :: Natural). (n <= h) => NatRepr n -> a
    forall (n :: Natural). (0 <= n, n <= h) => NatRepr n -> a
    f

    -- | Recursor for natural numbeers.
    natRec :: forall p f
           .  NatRepr p
           -> f 0 {- ^ base case -}
           -> (forall n. NatRepr n -> f n -> f (n + 1))
           -> f p
    natRec :: forall (p :: Natural) (f :: Natural -> Type).
    NatRepr p
    -> f 0
    -> (forall (n :: Natural). NatRepr n -> f n -> f (n + 1))
    -> f p
    natRec NatRepr p
    n f 0
    base forall (n :: Natural). NatRepr n -> f n -> f (n + 1)
    ind =
      case NatRepr p -> IsZeroNat p
    forall (n :: Natural). NatRepr n -> IsZeroNat n
    isZeroNat NatRepr p
    n of
        IsZeroNat p
    ZeroNat    -> f p
    f 0
    base
        IsZeroNat p
    NonZeroNat -> let n' :: NatRepr n
    n' = NatRepr (n + 1) -> NatRepr n
    forall (n :: Natural). NatRepr (n + 1) -> NatRepr n
    predNat NatRepr p
    NatRepr (n + 1)
    n
                      in NatRepr n -> f n -> f (n + 1)
    forall (n :: Natural). NatRepr n -> f n -> f (n + 1)
    ind NatRepr n
    n' (NatRepr n
    -> f 0
    -> (forall (n :: Natural). NatRepr n -> f n -> f (n + 1))
    -> f n
    forall (p :: Natural) (f :: Natural -> Type).
    NatRepr p
    -> f 0
    -> (forall (n :: Natural). NatRepr n -> f n -> f (n + 1))
    -> f p
    natRec NatRepr n
    n' f 0
    base NatRepr n -> f n -> f (n + 1)
    forall (n :: Natural). NatRepr n -> f n -> f (n + 1)
    ind)

    -- | Strong induction variant of the recursor.
    natRecStrong :: forall p f
                 .  NatRepr p
                 -> f 0 {- ^ base case -}
                 -> (forall n.
                      NatRepr n ->
                      (forall m. (m <= n) => NatRepr m -> f m) ->
                      f (n + 1)) {- ^ inductive step -}
                 -> f p
    natRecStrong :: forall (p :: Natural) (f :: Natural -> Type).
    NatRepr p
    -> f 0
    -> (forall (n :: Natural).
        NatRepr n
        -> (forall (m :: Natural). (m <= n) => NatRepr m -> f m)
        -> f (n + 1))
    -> f p
    natRecStrong NatRepr p
    p f 0
    base forall (n :: Natural).
    NatRepr n
    -> (forall (m :: Natural). (m <= n) => NatRepr m -> f m)
    -> f (n + 1)
    ind = f 0
    -> (forall (n :: Natural).
        NatRepr n
        -> (forall (m :: Natural). (m <= n) => NatRepr m -> f m)
        -> f (n + 1))
    -> NatRepr p
    -> f p
    forall (p' :: Natural) (f' :: Natural -> Type).
    f' 0
    -> (forall (n :: Natural).
        NatRepr n
        -> (forall (m :: Natural). (m <= n) => NatRepr m -> f' m)
        -> f' (n + 1))
    -> NatRepr p'
    -> f' p'
    natRecStrong' f 0
    base NatRepr n
    -> (forall (m :: Natural). (m <= n) => NatRepr m -> f m)
    -> f (n + 1)
    forall (n :: Natural).
    NatRepr n
    -> (forall (m :: Natural). (m <= n) => NatRepr m -> f m)
    -> f (n + 1)
    ind NatRepr p
    p
      where -- We can't use use "flip" or some other basic combinator
            -- because type variables can't be instantiated to contain "forall"s.
            natRecStrong' :: forall p' f'
                          .  f' 0 {- ^ base case -}
                          -> (forall n.
                                NatRepr n ->
                                (forall m. (m <= n) => NatRepr m -> f' m) ->
                                f' (n + 1)) {- ^ inductive step -}
                          -> NatRepr p'
                          -> f' p'
            natRecStrong' :: forall (p' :: Natural) (f' :: Natural -> Type).
    f' 0
    -> (forall (n :: Natural).
        NatRepr n
        -> (forall (m :: Natural). (m <= n) => NatRepr m -> f' m)
        -> f' (n + 1))
    -> NatRepr p'
    -> f' p'
    natRecStrong' f' 0
    base' forall (n :: Natural).
    NatRepr n
    -> (forall (m :: Natural). (m <= n) => NatRepr m -> f' m)
    -> f' (n + 1)
    ind' NatRepr p'
    n =
              case NatRepr p' -> IsZeroNat p'
    forall (n :: Natural). NatRepr n -> IsZeroNat n
    isZeroNat NatRepr p'
    n of
                IsZeroNat p'
    ZeroNat    -> f' p'
    f' 0
    base'
                IsZeroNat p'
    NonZeroNat -> NatRepr n
    -> (forall (m :: Natural). (m <= n) => NatRepr m -> f' m)
    -> f' (n + 1)
    forall (n :: Natural).
    NatRepr n
    -> (forall (m :: Natural). (m <= n) => NatRepr m -> f' m)
    -> f' (n + 1)
    ind' (NatRepr (n + 1) -> NatRepr n
    forall (n :: Natural). NatRepr (n + 1) -> NatRepr n
    predNat NatRepr p'
    NatRepr (n + 1)
    n) (f' 0
    -> (forall (n :: Natural).
        NatRepr n
        -> (forall (m :: Natural). (m <= n) => NatRepr m -> f' m)
        -> f' (n + 1))
    -> NatRepr m
    -> f' m
    forall (p' :: Natural) (f' :: Natural -> Type).
    f' 0
    -> (forall (n :: Natural).
        NatRepr n
        -> (forall (m :: Natural). (m <= n) => NatRepr m -> f' m)
        -> f' (n + 1))
    -> NatRepr p'
    -> f' p'
    natRecStrong' f' 0
    base' NatRepr n
    -> (forall (m :: Natural). (m <= n) => NatRepr m -> f' m)
    -> f' (n + 1)
    forall (n :: Natural).
    NatRepr n
    -> (forall (m :: Natural). (m <= n) => NatRepr m -> f' m)
    -> f' (n + 1)
    ind')

    -- | Bounded recursor for natural numbers.
    --
    -- If you can prove:
    -- - Base case: f 0
    -- - Inductive step: if n <= h and (f n) then (f (n + 1))
    -- You can conclude: for all n <= h, (f (n + 1)).
    natRecBounded :: forall m h f. (m <= h)
                  => NatRepr m
                  -> NatRepr h
                  -> f 0
                  -> (forall n. (n <= h) => NatRepr n -> f n -> f (n + 1))
                  -> f (m + 1)
    natRecBounded :: forall (m :: Natural) (h :: Natural) (f :: Natural -> Type).
    (m <= h) =>
    NatRepr m
    -> NatRepr h
    -> f 0
    -> (forall (n :: Natural).
        (n <= h) =>
        NatRepr n -> f n -> f (n + 1))
    -> f (m + 1)
    natRecBounded NatRepr m
    m NatRepr h
    h f 0
    base forall (n :: Natural). (n <= h) => NatRepr n -> f n -> f (n + 1)
    indH =
      case NatRepr m -> Either (m :~: 0) (LeqProof 1 m)
    forall (n :: Natural). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
    isZeroOrGT1 NatRepr m
    m of
        Left m :~: 0
    Refl      -> NatRepr 0 -> f 0 -> f (0 + 1)
    forall (n :: Natural). (n <= h) => NatRepr n -> f n -> f (n + 1)
    indH (forall (n :: Natural). KnownNat n => NatRepr n
    knownNat @0) f 0
    base
        Right LeqProof 1 m
    LeqProof ->
          case NatRepr m
    -> NatRepr h -> Either (LeqProof m h) (LeqProof m h -> Void)
    forall (a :: Natural) (b :: Natural).
    NatRepr a
    -> NatRepr b -> Either (LeqProof a b) (LeqProof a b -> Void)
    decideLeq NatRepr m
    m NatRepr h
    h of
            Left LeqProof m h
    LeqProof {- :: m <= h -} ->
              let -- Since m is non-zero, it is n + 1 for some n.
                  lemma :: LeqProof (m-1) h
                  lemma :: LeqProof (m - 1) h
    lemma = LeqProof m h -> LeqProof 1 m -> LeqProof (m - 1) h
    forall (m :: Natural) (n :: Natural) (p :: Natural).
    LeqProof m n -> LeqProof p m -> LeqProof (m - p) n
    leqSub (LeqProof m h
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof m h) (LeqProof 1 m
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof 1 m)
              in NatRepr m -> f m -> f (m + 1)
    forall (n :: Natural). (n <= h) => NatRepr n -> f n -> f (n + 1)
    indH NatRepr m
    m (f m -> f (m + 1)) -> f m -> f (m + 1)
    forall a b. (a -> b) -> a -> b
    $
                case LeqProof (m - 1) h
    lemma of { LeqProof (m - 1) h
    LeqProof ->
                case NatRepr m -> NatRepr 1 -> ((m - 1) + 1) :~: m
    forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    (n <= m) =>
    f m -> g n -> ((m - n) + n) :~: m
    minusPlusCancel NatRepr m
    m (forall (n :: Natural). KnownNat n => NatRepr n
    knownNat @1) of { ((m - 1) + 1) :~: m
    Refl ->
                  forall (m :: Natural) (h :: Natural) (f :: Natural -> Type).
    (m <= h) =>
    NatRepr m
    -> NatRepr h
    -> f 0
    -> (forall (n :: Natural).
        (n <= h) =>
        NatRepr n -> f n -> f (n + 1))
    -> f (m + 1)
    natRecBounded @(m - 1) @h @f (NatRepr ((m - 1) + 1) -> NatRepr (m - 1)
    forall (n :: Natural). NatRepr (n + 1) -> NatRepr n
    predNat NatRepr m
    NatRepr ((m - 1) + 1)
    m) NatRepr h
    h f 0
    base NatRepr n -> f n -> f (n + 1)
    forall (n :: Natural). (n <= h) => NatRepr n -> f n -> f (n + 1)
    indH
                }}
            Right LeqProof m h -> Void
    f {- :: (m <= h) -> Void -} ->
              Void -> f (m + 1)
    forall a. Void -> a
    absurd (Void -> f (m + 1)) -> Void -> f (m + 1)
    forall a b. (a -> b) -> a -> b
    $ LeqProof m h -> Void
    f (LeqProof m h
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof m h)

    -- | A version of 'natRecBounded' which doesn't require the type index of the
    -- result to be greater than @0@ and provides a strict inequality constraint.
    natRecStrictlyBounded ::
      forall m f.
      NatRepr m ->
      f 0 ->
      (forall n. (n + 1 <= m) => NatRepr n -> f n -> f (n + 1)) ->
      f m
    natRecStrictlyBounded :: forall (m :: Natural) (f :: Natural -> Type).
    NatRepr m
    -> f 0
    -> (forall (n :: Natural).
        ((n + 1) <= m) =>
        NatRepr n -> f n -> f (n + 1))
    -> f m
    natRecStrictlyBounded NatRepr m
    m f 0
    base forall (n :: Natural).
    ((n + 1) <= m) =>
    NatRepr n -> f n -> f (n + 1)
    indH =
      case NatRepr m -> IsZeroNat m
    forall (n :: Natural). NatRepr n -> IsZeroNat n
    isZeroNat NatRepr m
    m of
        IsZeroNat m
    ZeroNat -> f m
    f 0
    base
        IsZeroNat m
    NonZeroNat ->
          case NatRepr (n + 1) -> NatRepr n
    forall (n :: Natural). NatRepr (n + 1) -> NatRepr n
    predNat NatRepr m
    NatRepr (n + 1)
    m of
            (NatRepr n
    p :: NatRepr p) ->
              NatRepr n
    -> NatRepr n
    -> f 0
    -> (forall (n :: Natural).
        (n <= n) =>
        NatRepr n -> f n -> f (n + 1))
    -> f (n + 1)
    forall (m :: Natural) (h :: Natural) (f :: Natural -> Type).
    (m <= h) =>
    NatRepr m
    -> NatRepr h
    -> f 0
    -> (forall (n :: Natural).
        (n <= h) =>
        NatRepr n -> f n -> f (n + 1))
    -> f (m + 1)
    natRecBounded
                NatRepr n
    p
                NatRepr n
    p
                f 0
    base
                (\(NatRepr n
    k :: NatRepr n) (f n
    v :: f n) ->
                  case LeqProof n n -> LeqProof 1 1 -> LeqProof (n + 1) (n + 1)
    forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
           (y_h :: Natural).
    LeqProof x_l x_h
    -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
    leqAdd2 (LeqProof n n
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof n p) (LeqProof 1 1
    forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
    LeqProof :: LeqProof 1 1) of
                    LeqProof (n + 1) (n + 1)
    LeqProof -> NatRepr n -> f n -> f (n + 1)
    forall (n :: Natural).
    ((n + 1) <= m) =>
    NatRepr n -> f n -> f (n + 1)
    indH NatRepr n
    k f n
    v)

    mulCancelR ::
      (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> (n1 :~: n2)
    mulCancelR :: forall (c :: Natural) (n1 :: Natural) (n2 :: Natural)
           (f1 :: Natural -> Type) (f2 :: Natural -> Type)
           (f3 :: Natural -> Type).
    (1 <= c, (n1 * c) ~ (n2 * c)) =>
    f1 n1 -> f2 n2 -> f3 c -> n1 :~: n2
    mulCancelR f1 n1
    _ f2 n2
    _ f3 c
    _ = n1 :~: n2
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom

    -- | Used in @Vector@
    lemmaMul :: (1 <= n) => p w -> q n -> (w + (n-1) * w) :~: (n * w)
    lemmaMul :: forall (n :: Natural) (p :: Natural -> Type) (w :: Natural)
           (q :: Natural -> Type).
    (1 <= n) =>
    p w -> q n -> (w + ((n - 1) * w)) :~: (n * w)
    lemmaMul p w
    _ q n
    _ = (w + ((n - 1) * w)) :~: (n * w)
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom