lue-bird/elm-bounded-nat/11.0.0

NOTE: the latest version is 35.0.0

NNats

Nat (ArgN Nat0 ...) to Nat (ArgN 160 ...).

Bigger Nat (ArgN ...) s start to slow down compilation, so they are avoided.

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

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

The exact Nat 0.

Nat
(N
Nat1
(Nat1Plus orMore)
(Is a To (Nat1Plus a))
(Is b To (Nat1Plus b))
)

The exact Nat 1.

Nat
(N
Nat10
(Nat10Plus orMore)
(Is a To (Nat10Plus a))
(Is b To (Nat10Plus b))
)

The exact Nat 10.

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

The exact Nat 100.

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

The exact Nat 101.

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

The exact Nat 102.

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

The exact Nat 103.

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

The exact Nat 104.

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

The exact Nat 105.

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

The exact Nat 106.

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

The exact Nat 107.

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

The exact Nat 108.

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

The exact Nat 109.

Nat
(N
Nat11
(Nat11Plus orMore)
(Is a To (Nat11Plus a))
(Is b To (Nat11Plus b))
)

The exact Nat 11.

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

The exact Nat 110.

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

The exact Nat 111.

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

The exact Nat 112.

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

The exact Nat 113.

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

The exact Nat 114.

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

The exact Nat 115.

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

The exact Nat 116.

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

The exact Nat 117.

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

The exact Nat 118.

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

The exact Nat 119.

Nat
(N
Nat12
(Nat12Plus orMore)
(Is a To (Nat12Plus a))
(Is b To (Nat12Plus b))
)

The exact Nat 12.

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

The exact Nat 120.

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

The exact Nat 121.

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

The exact Nat 122.

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

The exact Nat 123.

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

The exact Nat 124.

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

The exact Nat 125.

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

The exact Nat 126.

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

The exact Nat 127.

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

The exact Nat 128.

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

The exact Nat 129.

Nat
(N
Nat13
(Nat13Plus orMore)
(Is a To (Nat13Plus a))
(Is b To (Nat13Plus b))
)

The exact Nat 13.

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

The exact Nat 130.

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

The exact Nat 131.

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

The exact Nat 132.

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

The exact Nat 133.

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

The exact Nat 134.

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

The exact Nat 135.

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

The exact Nat 136.

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

The exact Nat 137.

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

The exact Nat 138.

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

The exact Nat 139.

Nat
(N
Nat14
(Nat14Plus orMore)
(Is a To (Nat14Plus a))
(Is b To (Nat14Plus b))
)

The exact Nat 14.

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

The exact Nat 140.

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

The exact Nat 141.

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

The exact Nat 142.

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

The exact Nat 143.

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

The exact Nat 144.

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

The exact Nat 145.

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

The exact Nat 146.

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

The exact Nat 147.

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

The exact Nat 148.

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

The exact Nat 149.

Nat
(N
Nat15
(Nat15Plus orMore)
(Is a To (Nat15Plus a))
(Is b To (Nat15Plus b))
)

The exact Nat 15.

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

The exact Nat 150.

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

The exact Nat 151.

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

The exact Nat 152.

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

The exact Nat 153.

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

The exact Nat 154.

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

The exact Nat 155.

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

The exact Nat 156.

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

The exact Nat 157.

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

The exact Nat 158.

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

The exact Nat 159.

Nat
(N
Nat16
(Nat16Plus orMore)
(Is a To (Nat16Plus a))
(Is b To (Nat16Plus b))
)

The exact Nat 16.

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

The exact Nat 160.

Nat
(N
Nat17
(Nat17Plus orMore)
(Is a To (Nat17Plus a))
(Is b To (Nat17Plus b))
)

The exact Nat 17.

Nat
(N
Nat18
(Nat18Plus orMore)
(Is a To (Nat18Plus a))
(Is b To (Nat18Plus b))
)

The exact Nat 18.

Nat
(N
Nat19
(Nat19Plus orMore)
(Is a To (Nat19Plus a))
(Is b To (Nat19Plus b))
)

The exact Nat 19.

Nat
(N
Nat2
(Nat2Plus orMore)
(Is a To (Nat2Plus a))
(Is b To (Nat2Plus b))
)

The exact Nat 2.

Nat
(N
Nat20
(Nat20Plus orMore)
(Is a To (Nat20Plus a))
(Is b To (Nat20Plus b))
)

The exact Nat 20.

Nat
(N
Nat21
(Nat21Plus orMore)
(Is a To (Nat21Plus a))
(Is b To (Nat21Plus b))
)

The exact Nat 21.

Nat
(N
Nat22
(Nat22Plus orMore)
(Is a To (Nat22Plus a))
(Is b To (Nat22Plus b))
)

The exact Nat 22.

Nat
(N
Nat23
(Nat23Plus orMore)
(Is a To (Nat23Plus a))
(Is b To (Nat23Plus b))
)

The exact Nat 23.

Nat
(N
Nat24
(Nat24Plus orMore)
(Is a To (Nat24Plus a))
(Is b To (Nat24Plus b))
)

The exact Nat 24.

Nat
(N
Nat25
(Nat25Plus orMore)
(Is a To (Nat25Plus a))
(Is b To (Nat25Plus b))
)

The exact Nat 25.

Nat
(N
Nat26
(Nat26Plus orMore)
(Is a To (Nat26Plus a))
(Is b To (Nat26Plus b))
)

The exact Nat 26.

Nat
(N
Nat27
(Nat27Plus orMore)
(Is a To (Nat27Plus a))
(Is b To (Nat27Plus b))
)

The exact Nat 27.

Nat
(N
Nat28
(Nat28Plus orMore)
(Is a To (Nat28Plus a))
(Is b To (Nat28Plus b))
)

The exact Nat 28.

Nat
(N
Nat29
(Nat29Plus orMore)
(Is a To (Nat29Plus a))
(Is b To (Nat29Plus b))
)

The exact Nat 29.

Nat
(N
Nat3
(Nat3Plus orMore)
(Is a To (Nat3Plus a))
(Is b To (Nat3Plus b))
)

The exact Nat 3.

Nat
(N
Nat30
(Nat30Plus orMore)
(Is a To (Nat30Plus a))
(Is b To (Nat30Plus b))
)

The exact Nat 30.

Nat
(N
Nat31
(Nat31Plus orMore)
(Is a To (Nat31Plus a))
(Is b To (Nat31Plus b))
)

The exact Nat 31.

Nat
(N
Nat32
(Nat32Plus orMore)
(Is a To (Nat32Plus a))
(Is b To (Nat32Plus b))
)

The exact Nat 32.

Nat
(N
Nat33
(Nat33Plus orMore)
(Is a To (Nat33Plus a))
(Is b To (Nat33Plus b))
)

The exact Nat 33.

Nat
(N
Nat34
(Nat34Plus orMore)
(Is a To (Nat34Plus a))
(Is b To (Nat34Plus b))
)

The exact Nat 34.

Nat
(N
Nat35
(Nat35Plus orMore)
(Is a To (Nat35Plus a))
(Is b To (Nat35Plus b))
)

The exact Nat 35.

Nat
(N
Nat36
(Nat36Plus orMore)
(Is a To (Nat36Plus a))
(Is b To (Nat36Plus b))
)

The exact Nat 36.

Nat
(N
Nat37
(Nat37Plus orMore)
(Is a To (Nat37Plus a))
(Is b To (Nat37Plus b))
)

The exact Nat 37.

Nat
(N
Nat38
(Nat38Plus orMore)
(Is a To (Nat38Plus a))
(Is b To (Nat38Plus b))
)

The exact Nat 38.

Nat
(N
Nat39
(Nat39Plus orMore)
(Is a To (Nat39Plus a))
(Is b To (Nat39Plus b))
)

The exact Nat 39.

Nat
(N
Nat4
(Nat4Plus orMore)
(Is a To (Nat4Plus a))
(Is b To (Nat4Plus b))
)

The exact Nat 4.

Nat
(N
Nat40
(Nat40Plus orMore)
(Is a To (Nat40Plus a))
(Is b To (Nat40Plus b))
)

The exact Nat 40.

Nat
(N
Nat41
(Nat41Plus orMore)
(Is a To (Nat41Plus a))
(Is b To (Nat41Plus b))
)

The exact Nat 41.

Nat
(N
Nat42
(Nat42Plus orMore)
(Is a To (Nat42Plus a))
(Is b To (Nat42Plus b))
)

The exact Nat 42.

Nat
(N
Nat43
(Nat43Plus orMore)
(Is a To (Nat43Plus a))
(Is b To (Nat43Plus b))
)

The exact Nat 43.

Nat
(N
Nat44
(Nat44Plus orMore)
(Is a To (Nat44Plus a))
(Is b To (Nat44Plus b))
)

The exact Nat 44.

Nat
(N
Nat45
(Nat45Plus orMore)
(Is a To (Nat45Plus a))
(Is b To (Nat45Plus b))
)

The exact Nat 45.

Nat
(N
Nat46
(Nat46Plus orMore)
(Is a To (Nat46Plus a))
(Is b To (Nat46Plus b))
)

The exact Nat 46.

Nat
(N
Nat47
(Nat47Plus orMore)
(Is a To (Nat47Plus a))
(Is b To (Nat47Plus b))
)

The exact Nat 47.

Nat
(N
Nat48
(Nat48Plus orMore)
(Is a To (Nat48Plus a))
(Is b To (Nat48Plus b))
)

The exact Nat 48.

Nat
(N
Nat49
(Nat49Plus orMore)
(Is a To (Nat49Plus a))
(Is b To (Nat49Plus b))
)

The exact Nat 49.

Nat
(N
Nat5
(Nat5Plus orMore)
(Is a To (Nat5Plus a))
(Is b To (Nat5Plus b))
)

The exact Nat 5.

Nat
(N
Nat50
(Nat50Plus orMore)
(Is a To (Nat50Plus a))
(Is b To (Nat50Plus b))
)

The exact Nat 50.

Nat
(N
Nat51
(Nat51Plus orMore)
(Is a To (Nat51Plus a))
(Is b To (Nat51Plus b))
)

The exact Nat 51.

Nat
(N
Nat52
(Nat52Plus orMore)
(Is a To (Nat52Plus a))
(Is b To (Nat52Plus b))
)

The exact Nat 52.

Nat
(N
Nat53
(Nat53Plus orMore)
(Is a To (Nat53Plus a))
(Is b To (Nat53Plus b))
)

The exact Nat 53.

Nat
(N
Nat54
(Nat54Plus orMore)
(Is a To (Nat54Plus a))
(Is b To (Nat54Plus b))
)

The exact Nat 54.

Nat
(N
Nat55
(Nat55Plus orMore)
(Is a To (Nat55Plus a))
(Is b To (Nat55Plus b))
)

The exact Nat 55.

Nat
(N
Nat56
(Nat56Plus orMore)
(Is a To (Nat56Plus a))
(Is b To (Nat56Plus b))
)

The exact Nat 56.

Nat
(N
Nat57
(Nat57Plus orMore)
(Is a To (Nat57Plus a))
(Is b To (Nat57Plus b))
)

The exact Nat 57.

Nat
(N
Nat58
(Nat58Plus orMore)
(Is a To (Nat58Plus a))
(Is b To (Nat58Plus b))
)

The exact Nat 58.

Nat
(N
Nat59
(Nat59Plus orMore)
(Is a To (Nat59Plus a))
(Is b To (Nat59Plus b))
)

The exact Nat 59.

Nat
(N
Nat6
(Nat6Plus orMore)
(Is a To (Nat6Plus a))
(Is b To (Nat6Plus b))
)

The exact Nat 6.

Nat
(N
Nat60
(Nat60Plus orMore)
(Is a To (Nat60Plus a))
(Is b To (Nat60Plus b))
)

The exact Nat 60.

Nat
(N
Nat61
(Nat61Plus orMore)
(Is a To (Nat61Plus a))
(Is b To (Nat61Plus b))
)

The exact Nat 61.

Nat
(N
Nat62
(Nat62Plus orMore)
(Is a To (Nat62Plus a))
(Is b To (Nat62Plus b))
)

The exact Nat 62.

Nat
(N
Nat63
(Nat63Plus orMore)
(Is a To (Nat63Plus a))
(Is b To (Nat63Plus b))
)

The exact Nat 63.

Nat
(N
Nat64
(Nat64Plus orMore)
(Is a To (Nat64Plus a))
(Is b To (Nat64Plus b))
)

The exact Nat 64.

Nat
(N
Nat65
(Nat65Plus orMore)
(Is a To (Nat65Plus a))
(Is b To (Nat65Plus b))
)

The exact Nat 65.

Nat
(N
Nat66
(Nat66Plus orMore)
(Is a To (Nat66Plus a))
(Is b To (Nat66Plus b))
)

The exact Nat 66.

Nat
(N
Nat67
(Nat67Plus orMore)
(Is a To (Nat67Plus a))
(Is b To (Nat67Plus b))
)

The exact Nat 67.

Nat
(N
Nat68
(Nat68Plus orMore)
(Is a To (Nat68Plus a))
(Is b To (Nat68Plus b))
)

The exact Nat 68.

Nat
(N
Nat69
(Nat69Plus orMore)
(Is a To (Nat69Plus a))
(Is b To (Nat69Plus b))
)

The exact Nat 69.

Nat
(N
Nat7
(Nat7Plus orMore)
(Is a To (Nat7Plus a))
(Is b To (Nat7Plus b))
)

The exact Nat 7.

Nat
(N
Nat70
(Nat70Plus orMore)
(Is a To (Nat70Plus a))
(Is b To (Nat70Plus b))
)

The exact Nat 70.

Nat
(N
Nat71
(Nat71Plus orMore)
(Is a To (Nat71Plus a))
(Is b To (Nat71Plus b))
)

The exact Nat 71.

Nat
(N
Nat72
(Nat72Plus orMore)
(Is a To (Nat72Plus a))
(Is b To (Nat72Plus b))
)

The exact Nat 72.

Nat
(N
Nat73
(Nat73Plus orMore)
(Is a To (Nat73Plus a))
(Is b To (Nat73Plus b))
)

The exact Nat 73.

Nat
(N
Nat74
(Nat74Plus orMore)
(Is a To (Nat74Plus a))
(Is b To (Nat74Plus b))
)

The exact Nat 74.

Nat
(N
Nat75
(Nat75Plus orMore)
(Is a To (Nat75Plus a))
(Is b To (Nat75Plus b))
)

The exact Nat 75.

Nat
(N
Nat76
(Nat76Plus orMore)
(Is a To (Nat76Plus a))
(Is b To (Nat76Plus b))
)

The exact Nat 76.

Nat
(N
Nat77
(Nat77Plus orMore)
(Is a To (Nat77Plus a))
(Is b To (Nat77Plus b))
)

The exact Nat 77.

Nat
(N
Nat78
(Nat78Plus orMore)
(Is a To (Nat78Plus a))
(Is b To (Nat78Plus b))
)

The exact Nat 78.

Nat
(N
Nat79
(Nat79Plus orMore)
(Is a To (Nat79Plus a))
(Is b To (Nat79Plus b))
)

The exact Nat 79.

Nat
(N
Nat8
(Nat8Plus orMore)
(Is a To (Nat8Plus a))
(Is b To (Nat8Plus b))
)

The exact Nat 8.

Nat
(N
Nat80
(Nat80Plus orMore)
(Is a To (Nat80Plus a))
(Is b To (Nat80Plus b))
)

The exact Nat 80.

Nat
(N
Nat81
(Nat81Plus orMore)
(Is a To (Nat81Plus a))
(Is b To (Nat81Plus b))
)

The exact Nat 81.

Nat
(N
Nat82
(Nat82Plus orMore)
(Is a To (Nat82Plus a))
(Is b To (Nat82Plus b))
)

The exact Nat 82.

Nat
(N
Nat83
(Nat83Plus orMore)
(Is a To (Nat83Plus a))
(Is b To (Nat83Plus b))
)

The exact Nat 83.

Nat
(N
Nat84
(Nat84Plus orMore)
(Is a To (Nat84Plus a))
(Is b To (Nat84Plus b))
)

The exact Nat 84.

Nat
(N
Nat85
(Nat85Plus orMore)
(Is a To (Nat85Plus a))
(Is b To (Nat85Plus b))
)

The exact Nat 85.

Nat
(N
Nat86
(Nat86Plus orMore)
(Is a To (Nat86Plus a))
(Is b To (Nat86Plus b))
)

The exact Nat 86.

Nat
(N
Nat87
(Nat87Plus orMore)
(Is a To (Nat87Plus a))
(Is b To (Nat87Plus b))
)

The exact Nat 87.

Nat
(N
Nat88
(Nat88Plus orMore)
(Is a To (Nat88Plus a))
(Is b To (Nat88Plus b))
)

The exact Nat 88.

Nat
(N
Nat89
(Nat89Plus orMore)
(Is a To (Nat89Plus a))
(Is b To (Nat89Plus b))
)

The exact Nat 89.

Nat
(N
Nat9
(Nat9Plus orMore)
(Is a To (Nat9Plus a))
(Is b To (Nat9Plus b))
)

The exact Nat 9.

Nat
(N
Nat90
(Nat90Plus orMore)
(Is a To (Nat90Plus a))
(Is b To (Nat90Plus b))
)

The exact Nat 90.

Nat
(N
Nat91
(Nat91Plus orMore)
(Is a To (Nat91Plus a))
(Is b To (Nat91Plus b))
)

The exact Nat 91.

Nat
(N
Nat92
(Nat92Plus orMore)
(Is a To (Nat92Plus a))
(Is b To (Nat92Plus b))
)

The exact Nat 92.

Nat
(N
Nat93
(Nat93Plus orMore)
(Is a To (Nat93Plus a))
(Is b To (Nat93Plus b))
)

The exact Nat 93.

Nat
(N
Nat94
(Nat94Plus orMore)
(Is a To (Nat94Plus a))
(Is b To (Nat94Plus b))
)

The exact Nat 94.

Nat
(N
Nat95
(Nat95Plus orMore)
(Is a To (Nat95Plus a))
(Is b To (Nat95Plus b))
)

The exact Nat 95.

Nat
(N
Nat96
(Nat96Plus orMore)
(Is a To (Nat96Plus a))
(Is b To (Nat96Plus b))
)

The exact Nat 96.

Nat
(N
Nat97
(Nat97Plus orMore)
(Is a To (Nat97Plus a))
(Is b To (Nat97Plus b))
)

The exact Nat 97.

Nat
(N
Nat98
(Nat98Plus orMore)
(Is a To (Nat98Plus a))
(Is b To (Nat98Plus b))
)

The exact Nat 98.

Nat
(N
Nat99
(Nat99Plus orMore)
(Is a To (Nat99Plus a))
(Is b To (Nat99Plus b))
)

The exact Nat 99.