indique/elm-n-nat/2.0.0

NOTE: the latest version is 5.0.0

NNat

Representing natural numbers (>=0).

This module lets you represent exact values in the NNat type.

This means, packages like elm-n-array can use a NNat to promise:

fromRepeating : NNat n -> element -> NArray n element

→ repeating an element n times gives a Array with n elements!

The other use is to describe a difference between two values.

interval :
    { first : NNat (N first Is (Difference range To last))
    , last : NNat (N last Is lastDifference)
    }
-> Interval
→ because `range` is 0 or positive, `last` must also be at least as high as `first`.

See the readme for more information.

type alias NNat n =
NNat n

A natural number (<= 0), where you know the exact value.

NNat.n3 is of type

NNat (N N3Nat Is (Difference a To (N3NatPlus a)))

This means, its exact value can be described as

  • N3Nat

  • the Diffence of some a to a plus 3.

transform

toInt : NNat n -> Int

Convert a NNat to an Int.

NNat.n4 |> NNat.toInt
--> 4

values

n0 : NNat (N N0 Is (Difference a To a))

The NNat 0.

n1 : NNat (N N1 Is (Difference a To (N1Plus a)))

The NNat 1.

n10 : NNat (N N10 Is (Difference a To (N10Plus a)))

The NNat 10.

n100 : NNat (N N100 Is (Difference a To (N100Plus a)))

The NNat 100.

n101 : NNat (N N101 Is (Difference a To (N101Plus a)))

The NNat 101.

n102 : NNat (N N102 Is (Difference a To (N102Plus a)))

The NNat 102.

n103 : NNat (N N103 Is (Difference a To (N103Plus a)))

The NNat 103.

n104 : NNat (N N104 Is (Difference a To (N104Plus a)))

The NNat 104.

n105 : NNat (N N105 Is (Difference a To (N105Plus a)))

The NNat 105.

n106 : NNat (N N106 Is (Difference a To (N106Plus a)))

The NNat 106.

n107 : NNat (N N107 Is (Difference a To (N107Plus a)))

The NNat 107.

n108 : NNat (N N108 Is (Difference a To (N108Plus a)))

The NNat 108.

n109 : NNat (N N109 Is (Difference a To (N109Plus a)))

The NNat 109.

n11 : NNat (N N11 Is (Difference a To (N11Plus a)))

The NNat 11.

n110 : NNat (N N110 Is (Difference a To (N110Plus a)))

The NNat 110.

n111 : NNat (N N111 Is (Difference a To (N111Plus a)))

The NNat 111.

n112 : NNat (N N112 Is (Difference a To (N112Plus a)))

The NNat 112.

n113 : NNat (N N113 Is (Difference a To (N113Plus a)))

The NNat 113.

n114 : NNat (N N114 Is (Difference a To (N114Plus a)))

The NNat 114.

n115 : NNat (N N115 Is (Difference a To (N115Plus a)))

The NNat 115.

n116 : NNat (N N116 Is (Difference a To (N116Plus a)))

The NNat 116.

n117 : NNat (N N117 Is (Difference a To (N117Plus a)))

The NNat 117.

n118 : NNat (N N118 Is (Difference a To (N118Plus a)))

The NNat 118.

n119 : NNat (N N119 Is (Difference a To (N119Plus a)))

The NNat 119.

n12 : NNat (N N12 Is (Difference a To (N12Plus a)))

The NNat 12.

n120 : NNat (N N120 Is (Difference a To (N120Plus a)))

The NNat 120.

n121 : NNat (N N121 Is (Difference a To (N121Plus a)))

The NNat 121.

n122 : NNat (N N122 Is (Difference a To (N122Plus a)))

The NNat 122.

n123 : NNat (N N123 Is (Difference a To (N123Plus a)))

The NNat 123.

n124 : NNat (N N124 Is (Difference a To (N124Plus a)))

The NNat 124.

n125 : NNat (N N125 Is (Difference a To (N125Plus a)))

The NNat 125.

n126 : NNat (N N126 Is (Difference a To (N126Plus a)))

The NNat 126.

n127 : NNat (N N127 Is (Difference a To (N127Plus a)))

The NNat 127.

n128 : NNat (N N128 Is (Difference a To (N128Plus a)))

The NNat 128.

n129 : NNat (N N129 Is (Difference a To (N129Plus a)))

The NNat 129.

n13 : NNat (N N13 Is (Difference a To (N13Plus a)))

The NNat 13.

n130 : NNat (N N130 Is (Difference a To (N130Plus a)))

The NNat 130.

n131 : NNat (N N131 Is (Difference a To (N131Plus a)))

The NNat 131.

n132 : NNat (N N132 Is (Difference a To (N132Plus a)))

The NNat 132.

n133 : NNat (N N133 Is (Difference a To (N133Plus a)))

The NNat 133.

n134 : NNat (N N134 Is (Difference a To (N134Plus a)))

The NNat 134.

n135 : NNat (N N135 Is (Difference a To (N135Plus a)))

The NNat 135.

n136 : NNat (N N136 Is (Difference a To (N136Plus a)))

The NNat 136.

n137 : NNat (N N137 Is (Difference a To (N137Plus a)))

The NNat 137.

n138 : NNat (N N138 Is (Difference a To (N138Plus a)))

The NNat 138.

n139 : NNat (N N139 Is (Difference a To (N139Plus a)))

The NNat 139.

n14 : NNat (N N14 Is (Difference a To (N14Plus a)))

The NNat 14.

n140 : NNat (N N140 Is (Difference a To (N140Plus a)))

The NNat 140.

n141 : NNat (N N141 Is (Difference a To (N141Plus a)))

The NNat 141.

n142 : NNat (N N142 Is (Difference a To (N142Plus a)))

The NNat 142.

n143 : NNat (N N143 Is (Difference a To (N143Plus a)))

The NNat 143.

n144 : NNat (N N144 Is (Difference a To (N144Plus a)))

The NNat 144.

n145 : NNat (N N145 Is (Difference a To (N145Plus a)))

The NNat 145.

n146 : NNat (N N146 Is (Difference a To (N146Plus a)))

The NNat 146.

n147 : NNat (N N147 Is (Difference a To (N147Plus a)))

The NNat 147.

n148 : NNat (N N148 Is (Difference a To (N148Plus a)))

The NNat 148.

n149 : NNat (N N149 Is (Difference a To (N149Plus a)))

The NNat 149.

n15 : NNat (N N15 Is (Difference a To (N15Plus a)))

The NNat 15.

n150 : NNat (N N150 Is (Difference a To (N150Plus a)))

The NNat 150.

n151 : NNat (N N151 Is (Difference a To (N151Plus a)))

The NNat 151.

n152 : NNat (N N152 Is (Difference a To (N152Plus a)))

The NNat 152.

n153 : NNat (N N153 Is (Difference a To (N153Plus a)))

The NNat 153.

n154 : NNat (N N154 Is (Difference a To (N154Plus a)))

The NNat 154.

n155 : NNat (N N155 Is (Difference a To (N155Plus a)))

The NNat 155.

n156 : NNat (N N156 Is (Difference a To (N156Plus a)))

The NNat 156.

n157 : NNat (N N157 Is (Difference a To (N157Plus a)))

The NNat 157.

n158 : NNat (N N158 Is (Difference a To (N158Plus a)))

The NNat 158.

n159 : NNat (N N159 Is (Difference a To (N159Plus a)))

The NNat 159.

n16 : NNat (N N16 Is (Difference a To (N16Plus a)))

The NNat 16.

n160 : NNat (N N160 Is (Difference a To (N160Plus a)))

The NNat 160.

n161 : NNat (N N161 Is (Difference a To (N161Plus a)))

The NNat 161.

n162 : NNat (N N162 Is (Difference a To (N162Plus a)))

The NNat 162.

n163 : NNat (N N163 Is (Difference a To (N163Plus a)))

The NNat 163.

n164 : NNat (N N164 Is (Difference a To (N164Plus a)))

The NNat 164.

n165 : NNat (N N165 Is (Difference a To (N165Plus a)))

The NNat 165.

n166 : NNat (N N166 Is (Difference a To (N166Plus a)))

The NNat 166.

n167 : NNat (N N167 Is (Difference a To (N167Plus a)))

The NNat 167.

n168 : NNat (N N168 Is (Difference a To (N168Plus a)))

The NNat 168.

n169 : NNat (N N169 Is (Difference a To (N169Plus a)))

The NNat 169.

n17 : NNat (N N17 Is (Difference a To (N17Plus a)))

The NNat 17.

n170 : NNat (N N170 Is (Difference a To (N170Plus a)))

The NNat 170.

n171 : NNat (N N171 Is (Difference a To (N171Plus a)))

The NNat 171.

n172 : NNat (N N172 Is (Difference a To (N172Plus a)))

The NNat 172.

n173 : NNat (N N173 Is (Difference a To (N173Plus a)))

The NNat 173.

n174 : NNat (N N174 Is (Difference a To (N174Plus a)))

The NNat 174.

n175 : NNat (N N175 Is (Difference a To (N175Plus a)))

The NNat 175.

n176 : NNat (N N176 Is (Difference a To (N176Plus a)))

The NNat 176.

n177 : NNat (N N177 Is (Difference a To (N177Plus a)))

The NNat 177.

n178 : NNat (N N178 Is (Difference a To (N178Plus a)))

The NNat 178.

n179 : NNat (N N179 Is (Difference a To (N179Plus a)))

The NNat 179.

n18 : NNat (N N18 Is (Difference a To (N18Plus a)))

The NNat 18.

n180 : NNat (N N180 Is (Difference a To (N180Plus a)))

The NNat 180.

n181 : NNat (N N181 Is (Difference a To (N181Plus a)))

The NNat 181.

n182 : NNat (N N182 Is (Difference a To (N182Plus a)))

The NNat 182.

n183 : NNat (N N183 Is (Difference a To (N183Plus a)))

The NNat 183.

n184 : NNat (N N184 Is (Difference a To (N184Plus a)))

The NNat 184.

n185 : NNat (N N185 Is (Difference a To (N185Plus a)))

The NNat 185.

n186 : NNat (N N186 Is (Difference a To (N186Plus a)))

The NNat 186.

n187 : NNat (N N187 Is (Difference a To (N187Plus a)))

The NNat 187.

n188 : NNat (N N188 Is (Difference a To (N188Plus a)))

The NNat 188.

n189 : NNat (N N189 Is (Difference a To (N189Plus a)))

The NNat 189.

n19 : NNat (N N19 Is (Difference a To (N19Plus a)))

The NNat 19.

n190 : NNat (N N190 Is (Difference a To (N190Plus a)))

The NNat 190.

n191 : NNat (N N191 Is (Difference a To (N191Plus a)))

The NNat 191.

n192 : NNat (N N192 Is (Difference a To (N192Plus a)))

The NNat 192.

n2 : NNat (N N2 Is (Difference a To (N2Plus a)))

The NNat 2.

n20 : NNat (N N20 Is (Difference a To (N20Plus a)))

The NNat 20.

n21 : NNat (N N21 Is (Difference a To (N21Plus a)))

The NNat 21.

n22 : NNat (N N22 Is (Difference a To (N22Plus a)))

The NNat 22.

n23 : NNat (N N23 Is (Difference a To (N23Plus a)))

The NNat 23.

n24 : NNat (N N24 Is (Difference a To (N24Plus a)))

The NNat 24.

n25 : NNat (N N25 Is (Difference a To (N25Plus a)))

The NNat 25.

n26 : NNat (N N26 Is (Difference a To (N26Plus a)))

The NNat 26.

n27 : NNat (N N27 Is (Difference a To (N27Plus a)))

The NNat 27.

n28 : NNat (N N28 Is (Difference a To (N28Plus a)))

The NNat 28.

n29 : NNat (N N29 Is (Difference a To (N29Plus a)))

The NNat 29.

n3 : NNat (N N3 Is (Difference a To (N3Plus a)))

The NNat 3.

n30 : NNat (N N30 Is (Difference a To (N30Plus a)))

The NNat 30.

n31 : NNat (N N31 Is (Difference a To (N31Plus a)))

The NNat 31.

n32 : NNat (N N32 Is (Difference a To (N32Plus a)))

The NNat 32.

n33 : NNat (N N33 Is (Difference a To (N33Plus a)))

The NNat 33.

n34 : NNat (N N34 Is (Difference a To (N34Plus a)))

The NNat 34.

n35 : NNat (N N35 Is (Difference a To (N35Plus a)))

The NNat 35.

n36 : NNat (N N36 Is (Difference a To (N36Plus a)))

The NNat 36.

n37 : NNat (N N37 Is (Difference a To (N37Plus a)))

The NNat 37.

n38 : NNat (N N38 Is (Difference a To (N38Plus a)))

The NNat 38.

n39 : NNat (N N39 Is (Difference a To (N39Plus a)))

The NNat 39.

n4 : NNat (N N4 Is (Difference a To (N4Plus a)))

The NNat 4.

n40 : NNat (N N40 Is (Difference a To (N40Plus a)))

The NNat 40.

n41 : NNat (N N41 Is (Difference a To (N41Plus a)))

The NNat 41.

n42 : NNat (N N42 Is (Difference a To (N42Plus a)))

The NNat 42.

n43 : NNat (N N43 Is (Difference a To (N43Plus a)))

The NNat 43.

n44 : NNat (N N44 Is (Difference a To (N44Plus a)))

The NNat 44.

n45 : NNat (N N45 Is (Difference a To (N45Plus a)))

The NNat 45.

n46 : NNat (N N46 Is (Difference a To (N46Plus a)))

The NNat 46.

n47 : NNat (N N47 Is (Difference a To (N47Plus a)))

The NNat 47.

n48 : NNat (N N48 Is (Difference a To (N48Plus a)))

The NNat 48.

n49 : NNat (N N49 Is (Difference a To (N49Plus a)))

The NNat 49.

n5 : NNat (N N5 Is (Difference a To (N5Plus a)))

The NNat 5.

n50 : NNat (N N50 Is (Difference a To (N50Plus a)))

The NNat 50.

n51 : NNat (N N51 Is (Difference a To (N51Plus a)))

The NNat 51.

n52 : NNat (N N52 Is (Difference a To (N52Plus a)))

The NNat 52.

n53 : NNat (N N53 Is (Difference a To (N53Plus a)))

The NNat 53.

n54 : NNat (N N54 Is (Difference a To (N54Plus a)))

The NNat 54.

n55 : NNat (N N55 Is (Difference a To (N55Plus a)))

The NNat 55.

n56 : NNat (N N56 Is (Difference a To (N56Plus a)))

The NNat 56.

n57 : NNat (N N57 Is (Difference a To (N57Plus a)))

The NNat 57.

n58 : NNat (N N58 Is (Difference a To (N58Plus a)))

The NNat 58.

n59 : NNat (N N59 Is (Difference a To (N59Plus a)))

The NNat 59.

n6 : NNat (N N6 Is (Difference a To (N6Plus a)))

The NNat 6.

n60 : NNat (N N60 Is (Difference a To (N60Plus a)))

The NNat 60.

n61 : NNat (N N61 Is (Difference a To (N61Plus a)))

The NNat 61.

n62 : NNat (N N62 Is (Difference a To (N62Plus a)))

The NNat 62.

n63 : NNat (N N63 Is (Difference a To (N63Plus a)))

The NNat 63.

n64 : NNat (N N64 Is (Difference a To (N64Plus a)))

The NNat 64.

n65 : NNat (N N65 Is (Difference a To (N65Plus a)))

The NNat 65.

n66 : NNat (N N66 Is (Difference a To (N66Plus a)))

The NNat 66.

n67 : NNat (N N67 Is (Difference a To (N67Plus a)))

The NNat 67.

n68 : NNat (N N68 Is (Difference a To (N68Plus a)))

The NNat 68.

n69 : NNat (N N69 Is (Difference a To (N69Plus a)))

The NNat 69.

n7 : NNat (N N7 Is (Difference a To (N7Plus a)))

The NNat 7.

n70 : NNat (N N70 Is (Difference a To (N70Plus a)))

The NNat 70.

n71 : NNat (N N71 Is (Difference a To (N71Plus a)))

The NNat 71.

n72 : NNat (N N72 Is (Difference a To (N72Plus a)))

The NNat 72.

n73 : NNat (N N73 Is (Difference a To (N73Plus a)))

The NNat 73.

n74 : NNat (N N74 Is (Difference a To (N74Plus a)))

The NNat 74.

n75 : NNat (N N75 Is (Difference a To (N75Plus a)))

The NNat 75.

n76 : NNat (N N76 Is (Difference a To (N76Plus a)))

The NNat 76.

n77 : NNat (N N77 Is (Difference a To (N77Plus a)))

The NNat 77.

n78 : NNat (N N78 Is (Difference a To (N78Plus a)))

The NNat 78.

n79 : NNat (N N79 Is (Difference a To (N79Plus a)))

The NNat 79.

n8 : NNat (N N8 Is (Difference a To (N8Plus a)))

The NNat 8.

n80 : NNat (N N80 Is (Difference a To (N80Plus a)))

The NNat 80.

n81 : NNat (N N81 Is (Difference a To (N81Plus a)))

The NNat 81.

n82 : NNat (N N82 Is (Difference a To (N82Plus a)))

The NNat 82.

n83 : NNat (N N83 Is (Difference a To (N83Plus a)))

The NNat 83.

n84 : NNat (N N84 Is (Difference a To (N84Plus a)))

The NNat 84.

n85 : NNat (N N85 Is (Difference a To (N85Plus a)))

The NNat 85.

n86 : NNat (N N86 Is (Difference a To (N86Plus a)))

The NNat 86.

n87 : NNat (N N87 Is (Difference a To (N87Plus a)))

The NNat 87.

n88 : NNat (N N88 Is (Difference a To (N88Plus a)))

The NNat 88.

n89 : NNat (N N89 Is (Difference a To (N89Plus a)))

The NNat 89.

n9 : NNat (N N9 Is (Difference a To (N9Plus a)))

The NNat 9.

n90 : NNat (N N90 Is (Difference a To (N90Plus a)))

The NNat 90.

n91 : NNat (N N91 Is (Difference a To (N91Plus a)))

The NNat 91.

n92 : NNat (N N92 Is (Difference a To (N92Plus a)))

The NNat 92.

n93 : NNat (N N93 Is (Difference a To (N93Plus a)))

The NNat 93.

n94 : NNat (N N94 Is (Difference a To (N94Plus a)))

The NNat 94.

n95 : NNat (N N95 Is (Difference a To (N95Plus a)))

The NNat 95.

n96 : NNat (N N96 Is (Difference a To (N96Plus a)))

The NNat 96.

n97 : NNat (N N97 Is (Difference a To (N97Plus a)))

The NNat 97.

n98 : NNat (N N98 Is (Difference a To (N98Plus a)))

The NNat 98.

n99 : NNat (N N99 Is (Difference a To (N99Plus a)))

The NNat 99.

add

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N1Plus n) Is (Difference a To (N1Plus nPlusA)))

The NNat plus 1.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N10Plus n) Is (Difference a To (N10Plus nPlusA)))

The NNat plus 10.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N100Plus n) Is (Difference a To (N100Plus nPlusA)))

The NNat plus 100.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N101Plus n) Is (Difference a To (N101Plus nPlusA)))

The NNat plus 101.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N102Plus n) Is (Difference a To (N102Plus nPlusA)))

The NNat plus 102.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N103Plus n) Is (Difference a To (N103Plus nPlusA)))

The NNat plus 103.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N104Plus n) Is (Difference a To (N104Plus nPlusA)))

The NNat plus 104.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N105Plus n) Is (Difference a To (N105Plus nPlusA)))

The NNat plus 105.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N106Plus n) Is (Difference a To (N106Plus nPlusA)))

The NNat plus 106.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N107Plus n) Is (Difference a To (N107Plus nPlusA)))

The NNat plus 107.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N108Plus n) Is (Difference a To (N108Plus nPlusA)))

The NNat plus 108.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N109Plus n) Is (Difference a To (N109Plus nPlusA)))

The NNat plus 109.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N11Plus n) Is (Difference a To (N11Plus nPlusA)))

The NNat plus 11.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N110Plus n) Is (Difference a To (N110Plus nPlusA)))

The NNat plus 110.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N111Plus n) Is (Difference a To (N111Plus nPlusA)))

The NNat plus 111.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N112Plus n) Is (Difference a To (N112Plus nPlusA)))

The NNat plus 112.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N113Plus n) Is (Difference a To (N113Plus nPlusA)))

The NNat plus 113.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N114Plus n) Is (Difference a To (N114Plus nPlusA)))

The NNat plus 114.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N115Plus n) Is (Difference a To (N115Plus nPlusA)))

The NNat plus 115.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N116Plus n) Is (Difference a To (N116Plus nPlusA)))

The NNat plus 116.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N117Plus n) Is (Difference a To (N117Plus nPlusA)))

The NNat plus 117.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N118Plus n) Is (Difference a To (N118Plus nPlusA)))

The NNat plus 118.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N119Plus n) Is (Difference a To (N119Plus nPlusA)))

The NNat plus 119.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N12Plus n) Is (Difference a To (N12Plus nPlusA)))

The NNat plus 12.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N120Plus n) Is (Difference a To (N120Plus nPlusA)))

The NNat plus 120.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N121Plus n) Is (Difference a To (N121Plus nPlusA)))

The NNat plus 121.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N122Plus n) Is (Difference a To (N122Plus nPlusA)))

The NNat plus 122.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N123Plus n) Is (Difference a To (N123Plus nPlusA)))

The NNat plus 123.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N124Plus n) Is (Difference a To (N124Plus nPlusA)))

The NNat plus 124.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N125Plus n) Is (Difference a To (N125Plus nPlusA)))

The NNat plus 125.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N126Plus n) Is (Difference a To (N126Plus nPlusA)))

The NNat plus 126.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N127Plus n) Is (Difference a To (N127Plus nPlusA)))

The NNat plus 127.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N128Plus n) Is (Difference a To (N128Plus nPlusA)))

The NNat plus 128.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N13Plus n) Is (Difference a To (N13Plus nPlusA)))

The NNat plus 13.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N14Plus n) Is (Difference a To (N14Plus nPlusA)))

The NNat plus 14.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N15Plus n) Is (Difference a To (N15Plus nPlusA)))

The NNat plus 15.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N16Plus n) Is (Difference a To (N16Plus nPlusA)))

The NNat plus 16.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N17Plus n) Is (Difference a To (N17Plus nPlusA)))

The NNat plus 17.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N18Plus n) Is (Difference a To (N18Plus nPlusA)))

The NNat plus 18.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N19Plus n) Is (Difference a To (N19Plus nPlusA)))

The NNat plus 19.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N2Plus n) Is (Difference a To (N2Plus nPlusA)))

The NNat plus 2.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N20Plus n) Is (Difference a To (N20Plus nPlusA)))

The NNat plus 20.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N21Plus n) Is (Difference a To (N21Plus nPlusA)))

The NNat plus 21.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N22Plus n) Is (Difference a To (N22Plus nPlusA)))

The NNat plus 22.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N23Plus n) Is (Difference a To (N23Plus nPlusA)))

The NNat plus 23.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N24Plus n) Is (Difference a To (N24Plus nPlusA)))

The NNat plus 24.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N25Plus n) Is (Difference a To (N25Plus nPlusA)))

The NNat plus 25.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N26Plus n) Is (Difference a To (N26Plus nPlusA)))

The NNat plus 26.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N27Plus n) Is (Difference a To (N27Plus nPlusA)))

The NNat plus 27.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N28Plus n) Is (Difference a To (N28Plus nPlusA)))

The NNat plus 28.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N29Plus n) Is (Difference a To (N29Plus nPlusA)))

The NNat plus 29.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N3Plus n) Is (Difference a To (N3Plus nPlusA)))

The NNat plus 3.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N30Plus n) Is (Difference a To (N30Plus nPlusA)))

The NNat plus 30.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N31Plus n) Is (Difference a To (N31Plus nPlusA)))

The NNat plus 31.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N32Plus n) Is (Difference a To (N32Plus nPlusA)))

The NNat plus 32.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N33Plus n) Is (Difference a To (N33Plus nPlusA)))

The NNat plus 33.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N34Plus n) Is (Difference a To (N34Plus nPlusA)))

The NNat plus 34.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N35Plus n) Is (Difference a To (N35Plus nPlusA)))

The NNat plus 35.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N36Plus n) Is (Difference a To (N36Plus nPlusA)))

The NNat plus 36.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N37Plus n) Is (Difference a To (N37Plus nPlusA)))

The NNat plus 37.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N38Plus n) Is (Difference a To (N38Plus nPlusA)))

The NNat plus 38.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N39Plus n) Is (Difference a To (N39Plus nPlusA)))

The NNat plus 39.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N4Plus n) Is (Difference a To (N4Plus nPlusA)))

The NNat plus 4.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N40Plus n) Is (Difference a To (N40Plus nPlusA)))

The NNat plus 40.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N41Plus n) Is (Difference a To (N41Plus nPlusA)))

The NNat plus 41.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N42Plus n) Is (Difference a To (N42Plus nPlusA)))

The NNat plus 42.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N43Plus n) Is (Difference a To (N43Plus nPlusA)))

The NNat plus 43.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N44Plus n) Is (Difference a To (N44Plus nPlusA)))

The NNat plus 44.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N45Plus n) Is (Difference a To (N45Plus nPlusA)))

The NNat plus 45.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N46Plus n) Is (Difference a To (N46Plus nPlusA)))

The NNat plus 46.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N47Plus n) Is (Difference a To (N47Plus nPlusA)))

The NNat plus 47.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N48Plus n) Is (Difference a To (N48Plus nPlusA)))

The NNat plus 48.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N49Plus n) Is (Difference a To (N49Plus nPlusA)))

The NNat plus 49.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N5Plus n) Is (Difference a To (N5Plus nPlusA)))

The NNat plus 5.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N50Plus n) Is (Difference a To (N50Plus nPlusA)))

The NNat plus 50.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N51Plus n) Is (Difference a To (N51Plus nPlusA)))

The NNat plus 51.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N52Plus n) Is (Difference a To (N52Plus nPlusA)))

The NNat plus 52.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N53Plus n) Is (Difference a To (N53Plus nPlusA)))

The NNat plus 53.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N54Plus n) Is (Difference a To (N54Plus nPlusA)))

The NNat plus 54.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N55Plus n) Is (Difference a To (N55Plus nPlusA)))

The NNat plus 55.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N56Plus n) Is (Difference a To (N56Plus nPlusA)))

The NNat plus 56.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N57Plus n) Is (Difference a To (N57Plus nPlusA)))

The NNat plus 57.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N58Plus n) Is (Difference a To (N58Plus nPlusA)))

The NNat plus 58.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N59Plus n) Is (Difference a To (N59Plus nPlusA)))

The NNat plus 59.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N6Plus n) Is (Difference a To (N6Plus nPlusA)))

The NNat plus 6.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N60Plus n) Is (Difference a To (N60Plus nPlusA)))

The NNat plus 60.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N61Plus n) Is (Difference a To (N61Plus nPlusA)))

The NNat plus 61.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N62Plus n) Is (Difference a To (N62Plus nPlusA)))

The NNat plus 62.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N63Plus n) Is (Difference a To (N63Plus nPlusA)))

The NNat plus 63.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N64Plus n) Is (Difference a To (N64Plus nPlusA)))

The NNat plus 64.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N65Plus n) Is (Difference a To (N65Plus nPlusA)))

The NNat plus 65.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N66Plus n) Is (Difference a To (N66Plus nPlusA)))

The NNat plus 66.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N67Plus n) Is (Difference a To (N67Plus nPlusA)))

The NNat plus 67.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N68Plus n) Is (Difference a To (N68Plus nPlusA)))

The NNat plus 68.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N69Plus n) Is (Difference a To (N69Plus nPlusA)))

The NNat plus 69.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N7Plus n) Is (Difference a To (N7Plus nPlusA)))

The NNat plus 7.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N70Plus n) Is (Difference a To (N70Plus nPlusA)))

The NNat plus 70.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N71Plus n) Is (Difference a To (N71Plus nPlusA)))

The NNat plus 71.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N72Plus n) Is (Difference a To (N72Plus nPlusA)))

The NNat plus 72.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N73Plus n) Is (Difference a To (N73Plus nPlusA)))

The NNat plus 73.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N74Plus n) Is (Difference a To (N74Plus nPlusA)))

The NNat plus 74.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N75Plus n) Is (Difference a To (N75Plus nPlusA)))

The NNat plus 75.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N76Plus n) Is (Difference a To (N76Plus nPlusA)))

The NNat plus 76.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N77Plus n) Is (Difference a To (N77Plus nPlusA)))

The NNat plus 77.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N78Plus n) Is (Difference a To (N78Plus nPlusA)))

The NNat plus 78.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N79Plus n) Is (Difference a To (N79Plus nPlusA)))

The NNat plus 79.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N8Plus n) Is (Difference a To (N8Plus nPlusA)))

The NNat plus 8.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N80Plus n) Is (Difference a To (N80Plus nPlusA)))

The NNat plus 80.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N81Plus n) Is (Difference a To (N81Plus nPlusA)))

The NNat plus 81.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N82Plus n) Is (Difference a To (N82Plus nPlusA)))

The NNat plus 82.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N83Plus n) Is (Difference a To (N83Plus nPlusA)))

The NNat plus 83.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N84Plus n) Is (Difference a To (N84Plus nPlusA)))

The NNat plus 84.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N85Plus n) Is (Difference a To (N85Plus nPlusA)))

The NNat plus 85.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N86Plus n) Is (Difference a To (N86Plus nPlusA)))

The NNat plus 86.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N87Plus n) Is (Difference a To (N87Plus nPlusA)))

The NNat plus 87.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N88Plus n) Is (Difference a To (N88Plus nPlusA)))

The NNat plus 88.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N89Plus n) Is (Difference a To (N89Plus nPlusA)))

The NNat plus 89.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N9Plus n) Is (Difference a To (N9Plus nPlusA)))

The NNat plus 9.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N90Plus n) Is (Difference a To (N90Plus nPlusA)))

The NNat plus 90.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N91Plus n) Is (Difference a To (N91Plus nPlusA)))

The NNat plus 91.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N92Plus n) Is (Difference a To (N92Plus nPlusA)))

The NNat plus 92.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N93Plus n) Is (Difference a To (N93Plus nPlusA)))

The NNat plus 93.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N94Plus n) Is (Difference a To (N94Plus nPlusA)))

The NNat plus 94.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N95Plus n) Is (Difference a To (N95Plus nPlusA)))

The NNat plus 95.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N96Plus n) Is (Difference a To (N96Plus nPlusA)))

The NNat plus 96.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N97Plus n) Is (Difference a To (N97Plus nPlusA)))

The NNat plus 97.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N98Plus n) Is (Difference a To (N98Plus nPlusA)))

The NNat plus 98.

NNat (N n Is (Difference a To nPlusA))
-> NNat (N (N99Plus n) Is (Difference a To (N99Plus nPlusA)))

The NNat plus 99.

at least

NNat
(N (N1Plus nMinus1) Is (Difference a To (N1Plus nPlusAMinus1)))
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 1.

NNat
(N
(N10Plus nMinus1)
Is
(Difference a To (N10Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 10.

NNat
(N
(N100Plus nMinus1)
Is
(Difference a To (N100Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 100.

NNat
(N
(N101Plus nMinus1)
Is
(Difference a To (N101Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 101.

NNat
(N
(N102Plus nMinus1)
Is
(Difference a To (N102Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 102.

NNat
(N
(N103Plus nMinus1)
Is
(Difference a To (N103Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 103.

NNat
(N
(N104Plus nMinus1)
Is
(Difference a To (N104Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 104.

NNat
(N
(N105Plus nMinus1)
Is
(Difference a To (N105Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 105.

NNat
(N
(N106Plus nMinus1)
Is
(Difference a To (N106Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 106.

NNat
(N
(N107Plus nMinus1)
Is
(Difference a To (N107Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 107.

NNat
(N
(N108Plus nMinus1)
Is
(Difference a To (N108Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 108.

NNat
(N
(N109Plus nMinus1)
Is
(Difference a To (N109Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 109.

NNat
(N
(N11Plus nMinus1)
Is
(Difference a To (N11Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 11.

NNat
(N
(N110Plus nMinus1)
Is
(Difference a To (N110Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 110.

NNat
(N
(N111Plus nMinus1)
Is
(Difference a To (N111Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 111.

NNat
(N
(N112Plus nMinus1)
Is
(Difference a To (N112Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 112.

NNat
(N
(N113Plus nMinus1)
Is
(Difference a To (N113Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 113.

NNat
(N
(N114Plus nMinus1)
Is
(Difference a To (N114Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 114.

NNat
(N
(N115Plus nMinus1)
Is
(Difference a To (N115Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 115.

NNat
(N
(N116Plus nMinus1)
Is
(Difference a To (N116Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 116.

NNat
(N
(N117Plus nMinus1)
Is
(Difference a To (N117Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 117.

NNat
(N
(N118Plus nMinus1)
Is
(Difference a To (N118Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 118.

NNat
(N
(N119Plus nMinus1)
Is
(Difference a To (N119Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 119.

NNat
(N
(N12Plus nMinus1)
Is
(Difference a To (N12Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 12.

NNat
(N
(N120Plus nMinus1)
Is
(Difference a To (N120Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 120.

NNat
(N
(N121Plus nMinus1)
Is
(Difference a To (N121Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 121.

NNat
(N
(N122Plus nMinus1)
Is
(Difference a To (N122Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 122.

NNat
(N
(N123Plus nMinus1)
Is
(Difference a To (N123Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 123.

NNat
(N
(N124Plus nMinus1)
Is
(Difference a To (N124Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 124.

NNat
(N
(N125Plus nMinus1)
Is
(Difference a To (N125Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 125.

NNat
(N
(N126Plus nMinus1)
Is
(Difference a To (N126Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 126.

NNat
(N
(N127Plus nMinus1)
Is
(Difference a To (N127Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 127.

NNat
(N
(N128Plus nMinus1)
Is
(Difference a To (N128Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 128.

NNat
(N
(N13Plus nMinus1)
Is
(Difference a To (N13Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 13.

NNat
(N
(N14Plus nMinus1)
Is
(Difference a To (N14Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 14.

NNat
(N
(N15Plus nMinus1)
Is
(Difference a To (N15Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 15.

NNat
(N
(N16Plus nMinus1)
Is
(Difference a To (N16Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 16.

NNat
(N
(N17Plus nMinus1)
Is
(Difference a To (N17Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 17.

NNat
(N
(N18Plus nMinus1)
Is
(Difference a To (N18Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 18.

NNat
(N
(N19Plus nMinus1)
Is
(Difference a To (N19Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 19.

NNat
(N (N2Plus nMinus1) Is (Difference a To (N2Plus nPlusAMinus1)))
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 2.

NNat
(N
(N20Plus nMinus1)
Is
(Difference a To (N20Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 20.

NNat
(N
(N21Plus nMinus1)
Is
(Difference a To (N21Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 21.

NNat
(N
(N22Plus nMinus1)
Is
(Difference a To (N22Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 22.

NNat
(N
(N23Plus nMinus1)
Is
(Difference a To (N23Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 23.

NNat
(N
(N24Plus nMinus1)
Is
(Difference a To (N24Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 24.

NNat
(N
(N25Plus nMinus1)
Is
(Difference a To (N25Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 25.

NNat
(N
(N26Plus nMinus1)
Is
(Difference a To (N26Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 26.

NNat
(N
(N27Plus nMinus1)
Is
(Difference a To (N27Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 27.

NNat
(N
(N28Plus nMinus1)
Is
(Difference a To (N28Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 28.

NNat
(N
(N29Plus nMinus1)
Is
(Difference a To (N29Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 29.

NNat
(N (N3Plus nMinus1) Is (Difference a To (N3Plus nPlusAMinus1)))
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 3.

NNat
(N
(N30Plus nMinus1)
Is
(Difference a To (N30Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 30.

NNat
(N
(N31Plus nMinus1)
Is
(Difference a To (N31Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 31.

NNat
(N
(N32Plus nMinus1)
Is
(Difference a To (N32Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 32.

NNat
(N
(N33Plus nMinus1)
Is
(Difference a To (N33Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 33.

NNat
(N
(N34Plus nMinus1)
Is
(Difference a To (N34Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 34.

NNat
(N
(N35Plus nMinus1)
Is
(Difference a To (N35Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 35.

NNat
(N
(N36Plus nMinus1)
Is
(Difference a To (N36Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 36.

NNat
(N
(N37Plus nMinus1)
Is
(Difference a To (N37Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 37.

NNat
(N
(N38Plus nMinus1)
Is
(Difference a To (N38Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 38.

NNat
(N
(N39Plus nMinus1)
Is
(Difference a To (N39Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 39.

NNat
(N (N4Plus nMinus1) Is (Difference a To (N4Plus nPlusAMinus1)))
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 4.

NNat
(N
(N40Plus nMinus1)
Is
(Difference a To (N40Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 40.

NNat
(N
(N41Plus nMinus1)
Is
(Difference a To (N41Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 41.

NNat
(N
(N42Plus nMinus1)
Is
(Difference a To (N42Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 42.

NNat
(N
(N43Plus nMinus1)
Is
(Difference a To (N43Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 43.

NNat
(N
(N44Plus nMinus1)
Is
(Difference a To (N44Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 44.

NNat
(N
(N45Plus nMinus1)
Is
(Difference a To (N45Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 45.

NNat
(N
(N46Plus nMinus1)
Is
(Difference a To (N46Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 46.

NNat
(N
(N47Plus nMinus1)
Is
(Difference a To (N47Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 47.

NNat
(N
(N48Plus nMinus1)
Is
(Difference a To (N48Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 48.

NNat
(N
(N49Plus nMinus1)
Is
(Difference a To (N49Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 49.

NNat
(N (N5Plus nMinus1) Is (Difference a To (N5Plus nPlusAMinus1)))
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 5.

NNat
(N
(N50Plus nMinus1)
Is
(Difference a To (N50Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 50.

NNat
(N
(N51Plus nMinus1)
Is
(Difference a To (N51Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 51.

NNat
(N
(N52Plus nMinus1)
Is
(Difference a To (N52Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 52.

NNat
(N
(N53Plus nMinus1)
Is
(Difference a To (N53Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 53.

NNat
(N
(N54Plus nMinus1)
Is
(Difference a To (N54Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 54.

NNat
(N
(N55Plus nMinus1)
Is
(Difference a To (N55Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 55.

NNat
(N
(N56Plus nMinus1)
Is
(Difference a To (N56Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 56.

NNat
(N
(N57Plus nMinus1)
Is
(Difference a To (N57Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 57.

NNat
(N
(N58Plus nMinus1)
Is
(Difference a To (N58Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 58.

NNat
(N
(N59Plus nMinus1)
Is
(Difference a To (N59Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 59.

NNat
(N (N6Plus nMinus1) Is (Difference a To (N6Plus nPlusAMinus1)))
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 6.

NNat
(N
(N60Plus nMinus1)
Is
(Difference a To (N60Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 60.

NNat
(N
(N61Plus nMinus1)
Is
(Difference a To (N61Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 61.

NNat
(N
(N62Plus nMinus1)
Is
(Difference a To (N62Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 62.

NNat
(N
(N63Plus nMinus1)
Is
(Difference a To (N63Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 63.

NNat
(N
(N64Plus nMinus1)
Is
(Difference a To (N64Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 64.

NNat
(N
(N65Plus nMinus1)
Is
(Difference a To (N65Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 65.

NNat
(N
(N66Plus nMinus1)
Is
(Difference a To (N66Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 66.

NNat
(N
(N67Plus nMinus1)
Is
(Difference a To (N67Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 67.

NNat
(N
(N68Plus nMinus1)
Is
(Difference a To (N68Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 68.

NNat
(N
(N69Plus nMinus1)
Is
(Difference a To (N69Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 69.

NNat
(N (N7Plus nMinus1) Is (Difference a To (N7Plus nPlusAMinus1)))
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 7.

NNat
(N
(N70Plus nMinus1)
Is
(Difference a To (N70Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 70.

NNat
(N
(N71Plus nMinus1)
Is
(Difference a To (N71Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 71.

NNat
(N
(N72Plus nMinus1)
Is
(Difference a To (N72Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 72.

NNat
(N
(N73Plus nMinus1)
Is
(Difference a To (N73Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 73.

NNat
(N
(N74Plus nMinus1)
Is
(Difference a To (N74Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 74.

NNat
(N
(N75Plus nMinus1)
Is
(Difference a To (N75Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 75.

NNat
(N
(N76Plus nMinus1)
Is
(Difference a To (N76Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 76.

NNat
(N
(N77Plus nMinus1)
Is
(Difference a To (N77Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 77.

NNat
(N
(N78Plus nMinus1)
Is
(Difference a To (N78Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 78.

NNat
(N
(N79Plus nMinus1)
Is
(Difference a To (N79Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 79.

NNat
(N (N8Plus nMinus1) Is (Difference a To (N8Plus nPlusAMinus1)))
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 8.

NNat
(N
(N80Plus nMinus1)
Is
(Difference a To (N80Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 80.

NNat
(N
(N81Plus nMinus1)
Is
(Difference a To (N81Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 81.

NNat
(N
(N82Plus nMinus1)
Is
(Difference a To (N82Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 82.

NNat
(N
(N83Plus nMinus1)
Is
(Difference a To (N83Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 83.

NNat
(N
(N84Plus nMinus1)
Is
(Difference a To (N84Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 84.

NNat
(N
(N85Plus nMinus1)
Is
(Difference a To (N85Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 85.

NNat
(N
(N86Plus nMinus1)
Is
(Difference a To (N86Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 86.

NNat
(N
(N87Plus nMinus1)
Is
(Difference a To (N87Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 87.

NNat
(N
(N88Plus nMinus1)
Is
(Difference a To (N88Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 88.

NNat
(N
(N89Plus nMinus1)
Is
(Difference a To (N89Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 89.

NNat
(N (N9Plus nMinus1) Is (Difference a To (N9Plus nPlusAMinus1)))
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 9.

NNat
(N
(N90Plus nMinus1)
Is
(Difference a To (N90Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 90.

NNat
(N
(N91Plus nMinus1)
Is
(Difference a To (N91Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 91.

NNat
(N
(N92Plus nMinus1)
Is
(Difference a To (N92Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 92.

NNat
(N
(N93Plus nMinus1)
Is
(Difference a To (N93Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 93.

NNat
(N
(N94Plus nMinus1)
Is
(Difference a To (N94Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 94.

NNat
(N
(N95Plus nMinus1)
Is
(Difference a To (N95Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 95.

NNat
(N
(N96Plus nMinus1)
Is
(Difference a To (N96Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 96.

NNat
(N
(N97Plus nMinus1)
Is
(Difference a To (N97Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 97.

NNat
(N
(N98Plus nMinus1)
Is
(Difference a To (N98Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 98.

NNat
(N
(N99Plus nMinus1)
Is
(Difference a To (N99Plus nPlusAMinus1))
)
-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 99.