indique/elm-bounded-nat/9.1.1

NOTE: the latest version is 13.0.0

NNats

Nat (N Nat0 ...) to Nat (N Nat192 ...).

See Nat.Bound.N & Nat.N for an explanation.

nat0 : Nat (N Nat0 (Is a To a) (Is b To b))

The Nat 0.

nat1 : Nat (N Nat1 (Is a To (Nat1Plus a)) (Is b To (Nat1Plus b)))

The Nat 1.

nat10 : Nat (N Nat10 (Is a To (Nat10Plus a)) (Is b To (Nat10Plus b)))

The Nat 10.

Nat
(N Nat100 (Is a To (Nat100Plus a)) (Is b To (Nat100Plus b)))

The Nat 100.

Nat
(N Nat101 (Is a To (Nat101Plus a)) (Is b To (Nat101Plus b)))

The Nat 101.

Nat
(N Nat102 (Is a To (Nat102Plus a)) (Is b To (Nat102Plus b)))

The Nat 102.

Nat
(N Nat103 (Is a To (Nat103Plus a)) (Is b To (Nat103Plus b)))

The Nat 103.

Nat
(N Nat104 (Is a To (Nat104Plus a)) (Is b To (Nat104Plus b)))

The Nat 104.

Nat
(N Nat105 (Is a To (Nat105Plus a)) (Is b To (Nat105Plus b)))

The Nat 105.

Nat
(N Nat106 (Is a To (Nat106Plus a)) (Is b To (Nat106Plus b)))

The Nat 106.

Nat
(N Nat107 (Is a To (Nat107Plus a)) (Is b To (Nat107Plus b)))

The Nat 107.

Nat
(N Nat108 (Is a To (Nat108Plus a)) (Is b To (Nat108Plus b)))

The Nat 108.

Nat
(N Nat109 (Is a To (Nat109Plus a)) (Is b To (Nat109Plus b)))

The Nat 109.

nat11 : Nat (N Nat11 (Is a To (Nat11Plus a)) (Is b To (Nat11Plus b)))

The Nat 11.

Nat
(N Nat110 (Is a To (Nat110Plus a)) (Is b To (Nat110Plus b)))

The Nat 110.

Nat
(N Nat111 (Is a To (Nat111Plus a)) (Is b To (Nat111Plus b)))

The Nat 111.

Nat
(N Nat112 (Is a To (Nat112Plus a)) (Is b To (Nat112Plus b)))

The Nat 112.

Nat
(N Nat113 (Is a To (Nat113Plus a)) (Is b To (Nat113Plus b)))

The Nat 113.

Nat
(N Nat114 (Is a To (Nat114Plus a)) (Is b To (Nat114Plus b)))

The Nat 114.

Nat
(N Nat115 (Is a To (Nat115Plus a)) (Is b To (Nat115Plus b)))

The Nat 115.

Nat
(N Nat116 (Is a To (Nat116Plus a)) (Is b To (Nat116Plus b)))

The Nat 116.

Nat
(N Nat117 (Is a To (Nat117Plus a)) (Is b To (Nat117Plus b)))

The Nat 117.

Nat
(N Nat118 (Is a To (Nat118Plus a)) (Is b To (Nat118Plus b)))

The Nat 118.

Nat
(N Nat119 (Is a To (Nat119Plus a)) (Is b To (Nat119Plus b)))

The Nat 119.

nat12 : Nat (N Nat12 (Is a To (Nat12Plus a)) (Is b To (Nat12Plus b)))

The Nat 12.

Nat
(N Nat120 (Is a To (Nat120Plus a)) (Is b To (Nat120Plus b)))

The Nat 120.

Nat
(N Nat121 (Is a To (Nat121Plus a)) (Is b To (Nat121Plus b)))

The Nat 121.

Nat
(N Nat122 (Is a To (Nat122Plus a)) (Is b To (Nat122Plus b)))

The Nat 122.

Nat
(N Nat123 (Is a To (Nat123Plus a)) (Is b To (Nat123Plus b)))

The Nat 123.

Nat
(N Nat124 (Is a To (Nat124Plus a)) (Is b To (Nat124Plus b)))

The Nat 124.

Nat
(N Nat125 (Is a To (Nat125Plus a)) (Is b To (Nat125Plus b)))

The Nat 125.

Nat
(N Nat126 (Is a To (Nat126Plus a)) (Is b To (Nat126Plus b)))

The Nat 126.

Nat
(N Nat127 (Is a To (Nat127Plus a)) (Is b To (Nat127Plus b)))

The Nat 127.

Nat
(N Nat128 (Is a To (Nat128Plus a)) (Is b To (Nat128Plus b)))

The Nat 128.

Nat
(N Nat129 (Is a To (Nat129Plus a)) (Is b To (Nat129Plus b)))

The Nat 129.

nat13 : Nat (N Nat13 (Is a To (Nat13Plus a)) (Is b To (Nat13Plus b)))

The Nat 13.

Nat
(N Nat130 (Is a To (Nat130Plus a)) (Is b To (Nat130Plus b)))

The Nat 130.

Nat
(N Nat131 (Is a To (Nat131Plus a)) (Is b To (Nat131Plus b)))

The Nat 131.

Nat
(N Nat132 (Is a To (Nat132Plus a)) (Is b To (Nat132Plus b)))

The Nat 132.

Nat
(N Nat133 (Is a To (Nat133Plus a)) (Is b To (Nat133Plus b)))

The Nat 133.

Nat
(N Nat134 (Is a To (Nat134Plus a)) (Is b To (Nat134Plus b)))

The Nat 134.

Nat
(N Nat135 (Is a To (Nat135Plus a)) (Is b To (Nat135Plus b)))

The Nat 135.

Nat
(N Nat136 (Is a To (Nat136Plus a)) (Is b To (Nat136Plus b)))

The Nat 136.

Nat
(N Nat137 (Is a To (Nat137Plus a)) (Is b To (Nat137Plus b)))

The Nat 137.

Nat
(N Nat138 (Is a To (Nat138Plus a)) (Is b To (Nat138Plus b)))

The Nat 138.

Nat
(N Nat139 (Is a To (Nat139Plus a)) (Is b To (Nat139Plus b)))

The Nat 139.

nat14 : Nat (N Nat14 (Is a To (Nat14Plus a)) (Is b To (Nat14Plus b)))

The Nat 14.

Nat
(N Nat140 (Is a To (Nat140Plus a)) (Is b To (Nat140Plus b)))

The Nat 140.

Nat
(N Nat141 (Is a To (Nat141Plus a)) (Is b To (Nat141Plus b)))

The Nat 141.

Nat
(N Nat142 (Is a To (Nat142Plus a)) (Is b To (Nat142Plus b)))

The Nat 142.

Nat
(N Nat143 (Is a To (Nat143Plus a)) (Is b To (Nat143Plus b)))

The Nat 143.

Nat
(N Nat144 (Is a To (Nat144Plus a)) (Is b To (Nat144Plus b)))

The Nat 144.

Nat
(N Nat145 (Is a To (Nat145Plus a)) (Is b To (Nat145Plus b)))

The Nat 145.

Nat
(N Nat146 (Is a To (Nat146Plus a)) (Is b To (Nat146Plus b)))

The Nat 146.

Nat
(N Nat147 (Is a To (Nat147Plus a)) (Is b To (Nat147Plus b)))

The Nat 147.

Nat
(N Nat148 (Is a To (Nat148Plus a)) (Is b To (Nat148Plus b)))

The Nat 148.

Nat
(N Nat149 (Is a To (Nat149Plus a)) (Is b To (Nat149Plus b)))

The Nat 149.

nat15 : Nat (N Nat15 (Is a To (Nat15Plus a)) (Is b To (Nat15Plus b)))

The Nat 15.

Nat
(N Nat150 (Is a To (Nat150Plus a)) (Is b To (Nat150Plus b)))

The Nat 150.

Nat
(N Nat151 (Is a To (Nat151Plus a)) (Is b To (Nat151Plus b)))

The Nat 151.

Nat
(N Nat152 (Is a To (Nat152Plus a)) (Is b To (Nat152Plus b)))

The Nat 152.

Nat
(N Nat153 (Is a To (Nat153Plus a)) (Is b To (Nat153Plus b)))

The Nat 153.

Nat
(N Nat154 (Is a To (Nat154Plus a)) (Is b To (Nat154Plus b)))

The Nat 154.

Nat
(N Nat155 (Is a To (Nat155Plus a)) (Is b To (Nat155Plus b)))

The Nat 155.

Nat
(N Nat156 (Is a To (Nat156Plus a)) (Is b To (Nat156Plus b)))

The Nat 156.

Nat
(N Nat157 (Is a To (Nat157Plus a)) (Is b To (Nat157Plus b)))

The Nat 157.

Nat
(N Nat158 (Is a To (Nat158Plus a)) (Is b To (Nat158Plus b)))

The Nat 158.

Nat
(N Nat159 (Is a To (Nat159Plus a)) (Is b To (Nat159Plus b)))

The Nat 159.

nat16 : Nat (N Nat16 (Is a To (Nat16Plus a)) (Is b To (Nat16Plus b)))

The Nat 16.

Nat
(N Nat160 (Is a To (Nat160Plus a)) (Is b To (Nat160Plus b)))

The Nat 160.

Nat
(N Nat161 (Is a To (Nat161Plus a)) (Is b To (Nat161Plus b)))

The Nat 161.

Nat
(N Nat162 (Is a To (Nat162Plus a)) (Is b To (Nat162Plus b)))

The Nat 162.

Nat
(N Nat163 (Is a To (Nat163Plus a)) (Is b To (Nat163Plus b)))

The Nat 163.

Nat
(N Nat164 (Is a To (Nat164Plus a)) (Is b To (Nat164Plus b)))

The Nat 164.

Nat
(N Nat165 (Is a To (Nat165Plus a)) (Is b To (Nat165Plus b)))

The Nat 165.

Nat
(N Nat166 (Is a To (Nat166Plus a)) (Is b To (Nat166Plus b)))

The Nat 166.

Nat
(N Nat167 (Is a To (Nat167Plus a)) (Is b To (Nat167Plus b)))

The Nat 167.

Nat
(N Nat168 (Is a To (Nat168Plus a)) (Is b To (Nat168Plus b)))

The Nat 168.

Nat
(N Nat169 (Is a To (Nat169Plus a)) (Is b To (Nat169Plus b)))

The Nat 169.

nat17 : Nat (N Nat17 (Is a To (Nat17Plus a)) (Is b To (Nat17Plus b)))

The Nat 17.

Nat
(N Nat170 (Is a To (Nat170Plus a)) (Is b To (Nat170Plus b)))

The Nat 170.

Nat
(N Nat171 (Is a To (Nat171Plus a)) (Is b To (Nat171Plus b)))

The Nat 171.

Nat
(N Nat172 (Is a To (Nat172Plus a)) (Is b To (Nat172Plus b)))

The Nat 172.

Nat
(N Nat173 (Is a To (Nat173Plus a)) (Is b To (Nat173Plus b)))

The Nat 173.

Nat
(N Nat174 (Is a To (Nat174Plus a)) (Is b To (Nat174Plus b)))

The Nat 174.

Nat
(N Nat175 (Is a To (Nat175Plus a)) (Is b To (Nat175Plus b)))

The Nat 175.

Nat
(N Nat176 (Is a To (Nat176Plus a)) (Is b To (Nat176Plus b)))

The Nat 176.

Nat
(N Nat177 (Is a To (Nat177Plus a)) (Is b To (Nat177Plus b)))

The Nat 177.

Nat
(N Nat178 (Is a To (Nat178Plus a)) (Is b To (Nat178Plus b)))

The Nat 178.

Nat
(N Nat179 (Is a To (Nat179Plus a)) (Is b To (Nat179Plus b)))

The Nat 179.

nat18 : Nat (N Nat18 (Is a To (Nat18Plus a)) (Is b To (Nat18Plus b)))

The Nat 18.

Nat
(N Nat180 (Is a To (Nat180Plus a)) (Is b To (Nat180Plus b)))

The Nat 180.

Nat
(N Nat181 (Is a To (Nat181Plus a)) (Is b To (Nat181Plus b)))

The Nat 181.

Nat
(N Nat182 (Is a To (Nat182Plus a)) (Is b To (Nat182Plus b)))

The Nat 182.

Nat
(N Nat183 (Is a To (Nat183Plus a)) (Is b To (Nat183Plus b)))

The Nat 183.

Nat
(N Nat184 (Is a To (Nat184Plus a)) (Is b To (Nat184Plus b)))

The Nat 184.

Nat
(N Nat185 (Is a To (Nat185Plus a)) (Is b To (Nat185Plus b)))

The Nat 185.

Nat
(N Nat186 (Is a To (Nat186Plus a)) (Is b To (Nat186Plus b)))

The Nat 186.

Nat
(N Nat187 (Is a To (Nat187Plus a)) (Is b To (Nat187Plus b)))

The Nat 187.

Nat
(N Nat188 (Is a To (Nat188Plus a)) (Is b To (Nat188Plus b)))

The Nat 188.

Nat
(N Nat189 (Is a To (Nat189Plus a)) (Is b To (Nat189Plus b)))

The Nat 189.

nat19 : Nat (N Nat19 (Is a To (Nat19Plus a)) (Is b To (Nat19Plus b)))

The Nat 19.

Nat
(N Nat190 (Is a To (Nat190Plus a)) (Is b To (Nat190Plus b)))

The Nat 190.

Nat
(N Nat191 (Is a To (Nat191Plus a)) (Is b To (Nat191Plus b)))

The Nat 191.

Nat
(N Nat192 (Is a To (Nat192Plus a)) (Is b To (Nat192Plus b)))

The Nat 192.

nat2 : Nat (N Nat2 (Is a To (Nat2Plus a)) (Is b To (Nat2Plus b)))

The Nat 2.

nat20 : Nat (N Nat20 (Is a To (Nat20Plus a)) (Is b To (Nat20Plus b)))

The Nat 20.

nat21 : Nat (N Nat21 (Is a To (Nat21Plus a)) (Is b To (Nat21Plus b)))

The Nat 21.

nat22 : Nat (N Nat22 (Is a To (Nat22Plus a)) (Is b To (Nat22Plus b)))

The Nat 22.

nat23 : Nat (N Nat23 (Is a To (Nat23Plus a)) (Is b To (Nat23Plus b)))

The Nat 23.

nat24 : Nat (N Nat24 (Is a To (Nat24Plus a)) (Is b To (Nat24Plus b)))

The Nat 24.

nat25 : Nat (N Nat25 (Is a To (Nat25Plus a)) (Is b To (Nat25Plus b)))

The Nat 25.

nat26 : Nat (N Nat26 (Is a To (Nat26Plus a)) (Is b To (Nat26Plus b)))

The Nat 26.

nat27 : Nat (N Nat27 (Is a To (Nat27Plus a)) (Is b To (Nat27Plus b)))

The Nat 27.

nat28 : Nat (N Nat28 (Is a To (Nat28Plus a)) (Is b To (Nat28Plus b)))

The Nat 28.

nat29 : Nat (N Nat29 (Is a To (Nat29Plus a)) (Is b To (Nat29Plus b)))

The Nat 29.

nat3 : Nat (N Nat3 (Is a To (Nat3Plus a)) (Is b To (Nat3Plus b)))

The Nat 3.

nat30 : Nat (N Nat30 (Is a To (Nat30Plus a)) (Is b To (Nat30Plus b)))

The Nat 30.

nat31 : Nat (N Nat31 (Is a To (Nat31Plus a)) (Is b To (Nat31Plus b)))

The Nat 31.

nat32 : Nat (N Nat32 (Is a To (Nat32Plus a)) (Is b To (Nat32Plus b)))

The Nat 32.

nat33 : Nat (N Nat33 (Is a To (Nat33Plus a)) (Is b To (Nat33Plus b)))

The Nat 33.

nat34 : Nat (N Nat34 (Is a To (Nat34Plus a)) (Is b To (Nat34Plus b)))

The Nat 34.

nat35 : Nat (N Nat35 (Is a To (Nat35Plus a)) (Is b To (Nat35Plus b)))

The Nat 35.

nat36 : Nat (N Nat36 (Is a To (Nat36Plus a)) (Is b To (Nat36Plus b)))

The Nat 36.

nat37 : Nat (N Nat37 (Is a To (Nat37Plus a)) (Is b To (Nat37Plus b)))

The Nat 37.

nat38 : Nat (N Nat38 (Is a To (Nat38Plus a)) (Is b To (Nat38Plus b)))

The Nat 38.

nat39 : Nat (N Nat39 (Is a To (Nat39Plus a)) (Is b To (Nat39Plus b)))

The Nat 39.

nat4 : Nat (N Nat4 (Is a To (Nat4Plus a)) (Is b To (Nat4Plus b)))

The Nat 4.

nat40 : Nat (N Nat40 (Is a To (Nat40Plus a)) (Is b To (Nat40Plus b)))

The Nat 40.

nat41 : Nat (N Nat41 (Is a To (Nat41Plus a)) (Is b To (Nat41Plus b)))

The Nat 41.

nat42 : Nat (N Nat42 (Is a To (Nat42Plus a)) (Is b To (Nat42Plus b)))

The Nat 42.

nat43 : Nat (N Nat43 (Is a To (Nat43Plus a)) (Is b To (Nat43Plus b)))

The Nat 43.

nat44 : Nat (N Nat44 (Is a To (Nat44Plus a)) (Is b To (Nat44Plus b)))

The Nat 44.

nat45 : Nat (N Nat45 (Is a To (Nat45Plus a)) (Is b To (Nat45Plus b)))

The Nat 45.

nat46 : Nat (N Nat46 (Is a To (Nat46Plus a)) (Is b To (Nat46Plus b)))

The Nat 46.

nat47 : Nat (N Nat47 (Is a To (Nat47Plus a)) (Is b To (Nat47Plus b)))

The Nat 47.

nat48 : Nat (N Nat48 (Is a To (Nat48Plus a)) (Is b To (Nat48Plus b)))

The Nat 48.

nat49 : Nat (N Nat49 (Is a To (Nat49Plus a)) (Is b To (Nat49Plus b)))

The Nat 49.

nat5 : Nat (N Nat5 (Is a To (Nat5Plus a)) (Is b To (Nat5Plus b)))

The Nat 5.

nat50 : Nat (N Nat50 (Is a To (Nat50Plus a)) (Is b To (Nat50Plus b)))

The Nat 50.

nat51 : Nat (N Nat51 (Is a To (Nat51Plus a)) (Is b To (Nat51Plus b)))

The Nat 51.

nat52 : Nat (N Nat52 (Is a To (Nat52Plus a)) (Is b To (Nat52Plus b)))

The Nat 52.

nat53 : Nat (N Nat53 (Is a To (Nat53Plus a)) (Is b To (Nat53Plus b)))

The Nat 53.

nat54 : Nat (N Nat54 (Is a To (Nat54Plus a)) (Is b To (Nat54Plus b)))

The Nat 54.

nat55 : Nat (N Nat55 (Is a To (Nat55Plus a)) (Is b To (Nat55Plus b)))

The Nat 55.

nat56 : Nat (N Nat56 (Is a To (Nat56Plus a)) (Is b To (Nat56Plus b)))

The Nat 56.

nat57 : Nat (N Nat57 (Is a To (Nat57Plus a)) (Is b To (Nat57Plus b)))

The Nat 57.

nat58 : Nat (N Nat58 (Is a To (Nat58Plus a)) (Is b To (Nat58Plus b)))

The Nat 58.

nat59 : Nat (N Nat59 (Is a To (Nat59Plus a)) (Is b To (Nat59Plus b)))

The Nat 59.

nat6 : Nat (N Nat6 (Is a To (Nat6Plus a)) (Is b To (Nat6Plus b)))

The Nat 6.

nat60 : Nat (N Nat60 (Is a To (Nat60Plus a)) (Is b To (Nat60Plus b)))

The Nat 60.

nat61 : Nat (N Nat61 (Is a To (Nat61Plus a)) (Is b To (Nat61Plus b)))

The Nat 61.

nat62 : Nat (N Nat62 (Is a To (Nat62Plus a)) (Is b To (Nat62Plus b)))

The Nat 62.

nat63 : Nat (N Nat63 (Is a To (Nat63Plus a)) (Is b To (Nat63Plus b)))

The Nat 63.

nat64 : Nat (N Nat64 (Is a To (Nat64Plus a)) (Is b To (Nat64Plus b)))

The Nat 64.

nat65 : Nat (N Nat65 (Is a To (Nat65Plus a)) (Is b To (Nat65Plus b)))

The Nat 65.

nat66 : Nat (N Nat66 (Is a To (Nat66Plus a)) (Is b To (Nat66Plus b)))

The Nat 66.

nat67 : Nat (N Nat67 (Is a To (Nat67Plus a)) (Is b To (Nat67Plus b)))

The Nat 67.

nat68 : Nat (N Nat68 (Is a To (Nat68Plus a)) (Is b To (Nat68Plus b)))

The Nat 68.

nat69 : Nat (N Nat69 (Is a To (Nat69Plus a)) (Is b To (Nat69Plus b)))

The Nat 69.

nat7 : Nat (N Nat7 (Is a To (Nat7Plus a)) (Is b To (Nat7Plus b)))

The Nat 7.

nat70 : Nat (N Nat70 (Is a To (Nat70Plus a)) (Is b To (Nat70Plus b)))

The Nat 70.

nat71 : Nat (N Nat71 (Is a To (Nat71Plus a)) (Is b To (Nat71Plus b)))

The Nat 71.

nat72 : Nat (N Nat72 (Is a To (Nat72Plus a)) (Is b To (Nat72Plus b)))

The Nat 72.

nat73 : Nat (N Nat73 (Is a To (Nat73Plus a)) (Is b To (Nat73Plus b)))

The Nat 73.

nat74 : Nat (N Nat74 (Is a To (Nat74Plus a)) (Is b To (Nat74Plus b)))

The Nat 74.

nat75 : Nat (N Nat75 (Is a To (Nat75Plus a)) (Is b To (Nat75Plus b)))

The Nat 75.

nat76 : Nat (N Nat76 (Is a To (Nat76Plus a)) (Is b To (Nat76Plus b)))

The Nat 76.

nat77 : Nat (N Nat77 (Is a To (Nat77Plus a)) (Is b To (Nat77Plus b)))

The Nat 77.

nat78 : Nat (N Nat78 (Is a To (Nat78Plus a)) (Is b To (Nat78Plus b)))

The Nat 78.

nat79 : Nat (N Nat79 (Is a To (Nat79Plus a)) (Is b To (Nat79Plus b)))

The Nat 79.

nat8 : Nat (N Nat8 (Is a To (Nat8Plus a)) (Is b To (Nat8Plus b)))

The Nat 8.

nat80 : Nat (N Nat80 (Is a To (Nat80Plus a)) (Is b To (Nat80Plus b)))

The Nat 80.

nat81 : Nat (N Nat81 (Is a To (Nat81Plus a)) (Is b To (Nat81Plus b)))

The Nat 81.

nat82 : Nat (N Nat82 (Is a To (Nat82Plus a)) (Is b To (Nat82Plus b)))

The Nat 82.

nat83 : Nat (N Nat83 (Is a To (Nat83Plus a)) (Is b To (Nat83Plus b)))

The Nat 83.

nat84 : Nat (N Nat84 (Is a To (Nat84Plus a)) (Is b To (Nat84Plus b)))

The Nat 84.

nat85 : Nat (N Nat85 (Is a To (Nat85Plus a)) (Is b To (Nat85Plus b)))

The Nat 85.

nat86 : Nat (N Nat86 (Is a To (Nat86Plus a)) (Is b To (Nat86Plus b)))

The Nat 86.

nat87 : Nat (N Nat87 (Is a To (Nat87Plus a)) (Is b To (Nat87Plus b)))

The Nat 87.

nat88 : Nat (N Nat88 (Is a To (Nat88Plus a)) (Is b To (Nat88Plus b)))

The Nat 88.

nat89 : Nat (N Nat89 (Is a To (Nat89Plus a)) (Is b To (Nat89Plus b)))

The Nat 89.

nat9 : Nat (N Nat9 (Is a To (Nat9Plus a)) (Is b To (Nat9Plus b)))

The Nat 9.

nat90 : Nat (N Nat90 (Is a To (Nat90Plus a)) (Is b To (Nat90Plus b)))

The Nat 90.

nat91 : Nat (N Nat91 (Is a To (Nat91Plus a)) (Is b To (Nat91Plus b)))

The Nat 91.

nat92 : Nat (N Nat92 (Is a To (Nat92Plus a)) (Is b To (Nat92Plus b)))

The Nat 92.

nat93 : Nat (N Nat93 (Is a To (Nat93Plus a)) (Is b To (Nat93Plus b)))

The Nat 93.

nat94 : Nat (N Nat94 (Is a To (Nat94Plus a)) (Is b To (Nat94Plus b)))

The Nat 94.

nat95 : Nat (N Nat95 (Is a To (Nat95Plus a)) (Is b To (Nat95Plus b)))

The Nat 95.

nat96 : Nat (N Nat96 (Is a To (Nat96Plus a)) (Is b To (Nat96Plus b)))

The Nat 96.

nat97 : Nat (N Nat97 (Is a To (Nat97Plus a)) (Is b To (Nat97Plus b)))

The Nat 97.

nat98 : Nat (N Nat98 (Is a To (Nat98Plus a)) (Is b To (Nat98Plus b)))

The Nat 98.

nat99 : Nat (N Nat99 (Is a To (Nat99Plus a)) (Is b To (Nat99Plus b)))

The Nat 99.