Library MetaRocq.Utils.ByteCompare
From Stdlib Require Import Strings.Byte NArith.BinNat.
Module ByteN.
Definition N0 := 0%N.
Definition N1 := 1%N.
Definition N2 := 2%N.
Definition N3 := 3%N.
Definition N4 := 4%N.
Definition N5 := 5%N.
Definition N6 := 6%N.
Definition N7 := 7%N.
Definition N8 := 8%N.
Definition N9 := 9%N.
Definition N10 := 10%N.
Definition N11 := 11%N.
Definition N12 := 12%N.
Definition N13 := 13%N.
Definition N14 := 14%N.
Definition N15 := 15%N.
Definition N16 := 16%N.
Definition N17 := 17%N.
Definition N18 := 18%N.
Definition N19 := 19%N.
Definition N20 := 20%N.
Definition N21 := 21%N.
Definition N22 := 22%N.
Definition N23 := 23%N.
Definition N24 := 24%N.
Definition N25 := 25%N.
Definition N26 := 26%N.
Definition N27 := 27%N.
Definition N28 := 28%N.
Definition N29 := 29%N.
Definition N30 := 30%N.
Definition N31 := 31%N.
Definition N32 := 32%N.
Definition N33 := 33%N.
Definition N34 := 34%N.
Definition N35 := 35%N.
Definition N36 := 36%N.
Definition N37 := 37%N.
Definition N38 := 38%N.
Definition N39 := 39%N.
Definition N40 := 40%N.
Definition N41 := 41%N.
Definition N42 := 42%N.
Definition N43 := 43%N.
Definition N44 := 44%N.
Definition N45 := 45%N.
Definition N46 := 46%N.
Definition N47 := 47%N.
Definition N48 := 48%N.
Definition N49 := 49%N.
Definition N50 := 50%N.
Definition N51 := 51%N.
Definition N52 := 52%N.
Definition N53 := 53%N.
Definition N54 := 54%N.
Definition N55 := 55%N.
Definition N56 := 56%N.
Definition N57 := 57%N.
Definition N58 := 58%N.
Definition N59 := 59%N.
Definition N60 := 60%N.
Definition N61 := 61%N.
Definition N62 := 62%N.
Definition N63 := 63%N.
Definition N64 := 64%N.
Definition N65 := 65%N.
Definition N66 := 66%N.
Definition N67 := 67%N.
Definition N68 := 68%N.
Definition N69 := 69%N.
Definition N70 := 70%N.
Definition N71 := 71%N.
Definition N72 := 72%N.
Definition N73 := 73%N.
Definition N74 := 74%N.
Definition N75 := 75%N.
Definition N76 := 76%N.
Definition N77 := 77%N.
Definition N78 := 78%N.
Definition N79 := 79%N.
Definition N80 := 80%N.
Definition N81 := 81%N.
Definition N82 := 82%N.
Definition N83 := 83%N.
Definition N84 := 84%N.
Definition N85 := 85%N.
Definition N86 := 86%N.
Definition N87 := 87%N.
Definition N88 := 88%N.
Definition N89 := 89%N.
Definition N90 := 90%N.
Definition N91 := 91%N.
Definition N92 := 92%N.
Definition N93 := 93%N.
Definition N94 := 94%N.
Definition N95 := 95%N.
Definition N96 := 96%N.
Definition N97 := 97%N.
Definition N98 := 98%N.
Definition N99 := 99%N.
Definition N100 := 100%N.
Definition N101 := 101%N.
Definition N102 := 102%N.
Definition N103 := 103%N.
Definition N104 := 104%N.
Definition N105 := 105%N.
Definition N106 := 106%N.
Definition N107 := 107%N.
Definition N108 := 108%N.
Definition N109 := 109%N.
Definition N110 := 110%N.
Definition N111 := 111%N.
Definition N112 := 112%N.
Definition N113 := 113%N.
Definition N114 := 114%N.
Definition N115 := 115%N.
Definition N116 := 116%N.
Definition N117 := 117%N.
Definition N118 := 118%N.
Definition N119 := 119%N.
Definition N120 := 120%N.
Definition N121 := 121%N.
Definition N122 := 122%N.
Definition N123 := 123%N.
Definition N124 := 124%N.
Definition N125 := 125%N.
Definition N126 := 126%N.
Definition N127 := 127%N.
Definition N128 := 128%N.
Definition N129 := 129%N.
Definition N130 := 130%N.
Definition N131 := 131%N.
Definition N132 := 132%N.
Definition N133 := 133%N.
Definition N134 := 134%N.
Definition N135 := 135%N.
Definition N136 := 136%N.
Definition N137 := 137%N.
Definition N138 := 138%N.
Definition N139 := 139%N.
Definition N140 := 140%N.
Definition N141 := 141%N.
Definition N142 := 142%N.
Definition N143 := 143%N.
Definition N144 := 144%N.
Definition N145 := 145%N.
Definition N146 := 146%N.
Definition N147 := 147%N.
Definition N148 := 148%N.
Definition N149 := 149%N.
Definition N150 := 150%N.
Definition N151 := 151%N.
Definition N152 := 152%N.
Definition N153 := 153%N.
Definition N154 := 154%N.
Definition N155 := 155%N.
Definition N156 := 156%N.
Definition N157 := 157%N.
Definition N158 := 158%N.
Definition N159 := 159%N.
Definition N160 := 160%N.
Definition N161 := 161%N.
Definition N162 := 162%N.
Definition N163 := 163%N.
Definition N164 := 164%N.
Definition N165 := 165%N.
Definition N166 := 166%N.
Definition N167 := 167%N.
Definition N168 := 168%N.
Definition N169 := 169%N.
Definition N170 := 170%N.
Definition N171 := 171%N.
Definition N172 := 172%N.
Definition N173 := 173%N.
Definition N174 := 174%N.
Definition N175 := 175%N.
Definition N176 := 176%N.
Definition N177 := 177%N.
Definition N178 := 178%N.
Definition N179 := 179%N.
Definition N180 := 180%N.
Definition N181 := 181%N.
Definition N182 := 182%N.
Definition N183 := 183%N.
Definition N184 := 184%N.
Definition N185 := 185%N.
Definition N186 := 186%N.
Definition N187 := 187%N.
Definition N188 := 188%N.
Definition N189 := 189%N.
Definition N190 := 190%N.
Definition N191 := 191%N.
Definition N192 := 192%N.
Definition N193 := 193%N.
Definition N194 := 194%N.
Definition N195 := 195%N.
Definition N196 := 196%N.
Definition N197 := 197%N.
Definition N198 := 198%N.
Definition N199 := 199%N.
Definition N200 := 200%N.
Definition N201 := 201%N.
Definition N202 := 202%N.
Definition N203 := 203%N.
Definition N204 := 204%N.
Definition N205 := 205%N.
Definition N206 := 206%N.
Definition N207 := 207%N.
Definition N208 := 208%N.
Definition N209 := 209%N.
Definition N210 := 210%N.
Definition N211 := 211%N.
Definition N212 := 212%N.
Definition N213 := 213%N.
Definition N214 := 214%N.
Definition N215 := 215%N.
Definition N216 := 216%N.
Definition N217 := 217%N.
Definition N218 := 218%N.
Definition N219 := 219%N.
Definition N220 := 220%N.
Definition N221 := 221%N.
Definition N222 := 222%N.
Definition N223 := 223%N.
Definition N224 := 224%N.
Definition N225 := 225%N.
Definition N226 := 226%N.
Definition N227 := 227%N.
Definition N228 := 228%N.
Definition N229 := 229%N.
Definition N230 := 230%N.
Definition N231 := 231%N.
Definition N232 := 232%N.
Definition N233 := 233%N.
Definition N234 := 234%N.
Definition N235 := 235%N.
Definition N236 := 236%N.
Definition N237 := 237%N.
Definition N238 := 238%N.
Definition N239 := 239%N.
Definition N240 := 240%N.
Definition N241 := 241%N.
Definition N242 := 242%N.
Definition N243 := 243%N.
Definition N244 := 244%N.
Definition N245 := 245%N.
Definition N246 := 246%N.
Definition N247 := 247%N.
Definition N248 := 248%N.
Definition N249 := 249%N.
Definition N250 := 250%N.
Definition N251 := 251%N.
Definition N252 := 252%N.
Definition N253 := 253%N.
Definition N254 := 254%N.
Definition N255 := 255%N.
Definition to_N (x : byte) :=
match x with
| "000"%byte ⇒ N0
| "001"%byte ⇒ N1
| "002"%byte ⇒ N2
| "003"%byte ⇒ N3
| "004"%byte ⇒ N4
| "005"%byte ⇒ N5
| "006"%byte ⇒ N6
| "007"%byte ⇒ N7
| "008"%byte ⇒ N8
| "009"%byte ⇒ N9
| "010"%byte ⇒ N10
| "011"%byte ⇒ N11
| "012"%byte ⇒ N12
| "013"%byte ⇒ N13
| "014"%byte ⇒ N14
| "015"%byte ⇒ N15
| "016"%byte ⇒ N16
| "017"%byte ⇒ N17
| "018"%byte ⇒ N18
| "019"%byte ⇒ N19
| "020"%byte ⇒ N20
| "021"%byte ⇒ N21
| "022"%byte ⇒ N22
| "023"%byte ⇒ N23
| "024"%byte ⇒ N24
| "025"%byte ⇒ N25
| "026"%byte ⇒ N26
| "027"%byte ⇒ N27
| "028"%byte ⇒ N28
| "029"%byte ⇒ N29
| "030"%byte ⇒ N30
| "031"%byte ⇒ N31
| "032"%byte ⇒ N32
| "033"%byte ⇒ N33
| "034"%byte ⇒ N34
| "035"%byte ⇒ N35
| "036"%byte ⇒ N36
| "037"%byte ⇒ N37
| "038"%byte ⇒ N38
| "039"%byte ⇒ N39
| "040"%byte ⇒ N40
| "041"%byte ⇒ N41
| "042"%byte ⇒ N42
| "043"%byte ⇒ N43
| "044"%byte ⇒ N44
| "045"%byte ⇒ N45
| "046"%byte ⇒ N46
| "047"%byte ⇒ N47
| "048"%byte ⇒ N48
| "049"%byte ⇒ N49
| "050"%byte ⇒ N50
| "051"%byte ⇒ N51
| "052"%byte ⇒ N52
| "053"%byte ⇒ N53
| "054"%byte ⇒ N54
| "055"%byte ⇒ N55
| "056"%byte ⇒ N56
| "057"%byte ⇒ N57
| "058"%byte ⇒ N58
| "059"%byte ⇒ N59
| "060"%byte ⇒ N60
| "061"%byte ⇒ N61
| "062"%byte ⇒ N62
| "063"%byte ⇒ N63
| "064"%byte ⇒ N64
| "065"%byte ⇒ N65
| "066"%byte ⇒ N66
| "067"%byte ⇒ N67
| "068"%byte ⇒ N68
| "069"%byte ⇒ N69
| "070"%byte ⇒ N70
| "071"%byte ⇒ N71
| "072"%byte ⇒ N72
| "073"%byte ⇒ N73
| "074"%byte ⇒ N74
| "075"%byte ⇒ N75
| "076"%byte ⇒ N76
| "077"%byte ⇒ N77
| "078"%byte ⇒ N78
| "079"%byte ⇒ N79
| "080"%byte ⇒ N80
| "081"%byte ⇒ N81
| "082"%byte ⇒ N82
| "083"%byte ⇒ N83
| "084"%byte ⇒ N84
| "085"%byte ⇒ N85
| "086"%byte ⇒ N86
| "087"%byte ⇒ N87
| "088"%byte ⇒ N88
| "089"%byte ⇒ N89
| "090"%byte ⇒ N90
| "091"%byte ⇒ N91
| "092"%byte ⇒ N92
| "093"%byte ⇒ N93
| "094"%byte ⇒ N94
| "095"%byte ⇒ N95
| "096"%byte ⇒ N96
| "097"%byte ⇒ N97
| "098"%byte ⇒ N98
| "099"%byte ⇒ N99
| "100"%byte ⇒ N100
| "101"%byte ⇒ N101
| "102"%byte ⇒ N102
| "103"%byte ⇒ N103
| "104"%byte ⇒ N104
| "105"%byte ⇒ N105
| "106"%byte ⇒ N106
| "107"%byte ⇒ N107
| "108"%byte ⇒ N108
| "109"%byte ⇒ N109
| "110"%byte ⇒ N110
| "111"%byte ⇒ N111
| "112"%byte ⇒ N112
| "113"%byte ⇒ N113
| "114"%byte ⇒ N114
| "115"%byte ⇒ N115
| "116"%byte ⇒ N116
| "117"%byte ⇒ N117
| "118"%byte ⇒ N118
| "119"%byte ⇒ N119
| "120"%byte ⇒ N120
| "121"%byte ⇒ N121
| "122"%byte ⇒ N122
| "123"%byte ⇒ N123
| "124"%byte ⇒ N124
| "125"%byte ⇒ N125
| "126"%byte ⇒ N126
| "127"%byte ⇒ N127
| "128"%byte ⇒ N128
| "129"%byte ⇒ N129
| "130"%byte ⇒ N130
| "131"%byte ⇒ N131
| "132"%byte ⇒ N132
| "133"%byte ⇒ N133
| "134"%byte ⇒ N134
| "135"%byte ⇒ N135
| "136"%byte ⇒ N136
| "137"%byte ⇒ N137
| "138"%byte ⇒ N138
| "139"%byte ⇒ N139
| "140"%byte ⇒ N140
| "141"%byte ⇒ N141
| "142"%byte ⇒ N142
| "143"%byte ⇒ N143
| "144"%byte ⇒ N144
| "145"%byte ⇒ N145
| "146"%byte ⇒ N146
| "147"%byte ⇒ N147
| "148"%byte ⇒ N148
| "149"%byte ⇒ N149
| "150"%byte ⇒ N150
| "151"%byte ⇒ N151
| "152"%byte ⇒ N152
| "153"%byte ⇒ N153
| "154"%byte ⇒ N154
| "155"%byte ⇒ N155
| "156"%byte ⇒ N156
| "157"%byte ⇒ N157
| "158"%byte ⇒ N158
| "159"%byte ⇒ N159
| "160"%byte ⇒ N160
| "161"%byte ⇒ N161
| "162"%byte ⇒ N162
| "163"%byte ⇒ N163
| "164"%byte ⇒ N164
| "165"%byte ⇒ N165
| "166"%byte ⇒ N166
| "167"%byte ⇒ N167
| "168"%byte ⇒ N168
| "169"%byte ⇒ N169
| "170"%byte ⇒ N170
| "171"%byte ⇒ N171
| "172"%byte ⇒ N172
| "173"%byte ⇒ N173
| "174"%byte ⇒ N174
| "175"%byte ⇒ N175
| "176"%byte ⇒ N176
| "177"%byte ⇒ N177
| "178"%byte ⇒ N178
| "179"%byte ⇒ N179
| "180"%byte ⇒ N180
| "181"%byte ⇒ N181
| "182"%byte ⇒ N182
| "183"%byte ⇒ N183
| "184"%byte ⇒ N184
| "185"%byte ⇒ N185
| "186"%byte ⇒ N186
| "187"%byte ⇒ N187
| "188"%byte ⇒ N188
| "189"%byte ⇒ N189
| "190"%byte ⇒ N190
| "191"%byte ⇒ N191
| "192"%byte ⇒ N192
| "193"%byte ⇒ N193
| "194"%byte ⇒ N194
| "195"%byte ⇒ N195
| "196"%byte ⇒ N196
| "197"%byte ⇒ N197
| "198"%byte ⇒ N198
| "199"%byte ⇒ N199
| "200"%byte ⇒ N200
| "201"%byte ⇒ N201
| "202"%byte ⇒ N202
| "203"%byte ⇒ N203
| "204"%byte ⇒ N204
| "205"%byte ⇒ N205
| "206"%byte ⇒ N206
| "207"%byte ⇒ N207
| "208"%byte ⇒ N208
| "209"%byte ⇒ N209
| "210"%byte ⇒ N210
| "211"%byte ⇒ N211
| "212"%byte ⇒ N212
| "213"%byte ⇒ N213
| "214"%byte ⇒ N214
| "215"%byte ⇒ N215
| "216"%byte ⇒ N216
| "217"%byte ⇒ N217
| "218"%byte ⇒ N218
| "219"%byte ⇒ N219
| "220"%byte ⇒ N220
| "221"%byte ⇒ N221
| "222"%byte ⇒ N222
| "223"%byte ⇒ N223
| "224"%byte ⇒ N224
| "225"%byte ⇒ N225
| "226"%byte ⇒ N226
| "227"%byte ⇒ N227
| "228"%byte ⇒ N228
| "229"%byte ⇒ N229
| "230"%byte ⇒ N230
| "231"%byte ⇒ N231
| "232"%byte ⇒ N232
| "233"%byte ⇒ N233
| "234"%byte ⇒ N234
| "235"%byte ⇒ N235
| "236"%byte ⇒ N236
| "237"%byte ⇒ N237
| "238"%byte ⇒ N238
| "239"%byte ⇒ N239
| "240"%byte ⇒ N240
| "241"%byte ⇒ N241
| "242"%byte ⇒ N242
| "243"%byte ⇒ N243
| "244"%byte ⇒ N244
| "245"%byte ⇒ N245
| "246"%byte ⇒ N246
| "247"%byte ⇒ N247
| "248"%byte ⇒ N248
| "249"%byte ⇒ N249
| "250"%byte ⇒ N250
| "251"%byte ⇒ N251
| "252"%byte ⇒ N252
| "253"%byte ⇒ N253
| "254"%byte ⇒ N254
| "255"%byte ⇒ N255
end.
End ByteN.
Definition eqb (x y : byte) :=
N.eqb (ByteN.to_N x) (ByteN.to_N y).
Definition compare (x y : byte) :=
N.compare (ByteN.to_N x) (ByteN.to_N y).
Module ByteN.
Definition N0 := 0%N.
Definition N1 := 1%N.
Definition N2 := 2%N.
Definition N3 := 3%N.
Definition N4 := 4%N.
Definition N5 := 5%N.
Definition N6 := 6%N.
Definition N7 := 7%N.
Definition N8 := 8%N.
Definition N9 := 9%N.
Definition N10 := 10%N.
Definition N11 := 11%N.
Definition N12 := 12%N.
Definition N13 := 13%N.
Definition N14 := 14%N.
Definition N15 := 15%N.
Definition N16 := 16%N.
Definition N17 := 17%N.
Definition N18 := 18%N.
Definition N19 := 19%N.
Definition N20 := 20%N.
Definition N21 := 21%N.
Definition N22 := 22%N.
Definition N23 := 23%N.
Definition N24 := 24%N.
Definition N25 := 25%N.
Definition N26 := 26%N.
Definition N27 := 27%N.
Definition N28 := 28%N.
Definition N29 := 29%N.
Definition N30 := 30%N.
Definition N31 := 31%N.
Definition N32 := 32%N.
Definition N33 := 33%N.
Definition N34 := 34%N.
Definition N35 := 35%N.
Definition N36 := 36%N.
Definition N37 := 37%N.
Definition N38 := 38%N.
Definition N39 := 39%N.
Definition N40 := 40%N.
Definition N41 := 41%N.
Definition N42 := 42%N.
Definition N43 := 43%N.
Definition N44 := 44%N.
Definition N45 := 45%N.
Definition N46 := 46%N.
Definition N47 := 47%N.
Definition N48 := 48%N.
Definition N49 := 49%N.
Definition N50 := 50%N.
Definition N51 := 51%N.
Definition N52 := 52%N.
Definition N53 := 53%N.
Definition N54 := 54%N.
Definition N55 := 55%N.
Definition N56 := 56%N.
Definition N57 := 57%N.
Definition N58 := 58%N.
Definition N59 := 59%N.
Definition N60 := 60%N.
Definition N61 := 61%N.
Definition N62 := 62%N.
Definition N63 := 63%N.
Definition N64 := 64%N.
Definition N65 := 65%N.
Definition N66 := 66%N.
Definition N67 := 67%N.
Definition N68 := 68%N.
Definition N69 := 69%N.
Definition N70 := 70%N.
Definition N71 := 71%N.
Definition N72 := 72%N.
Definition N73 := 73%N.
Definition N74 := 74%N.
Definition N75 := 75%N.
Definition N76 := 76%N.
Definition N77 := 77%N.
Definition N78 := 78%N.
Definition N79 := 79%N.
Definition N80 := 80%N.
Definition N81 := 81%N.
Definition N82 := 82%N.
Definition N83 := 83%N.
Definition N84 := 84%N.
Definition N85 := 85%N.
Definition N86 := 86%N.
Definition N87 := 87%N.
Definition N88 := 88%N.
Definition N89 := 89%N.
Definition N90 := 90%N.
Definition N91 := 91%N.
Definition N92 := 92%N.
Definition N93 := 93%N.
Definition N94 := 94%N.
Definition N95 := 95%N.
Definition N96 := 96%N.
Definition N97 := 97%N.
Definition N98 := 98%N.
Definition N99 := 99%N.
Definition N100 := 100%N.
Definition N101 := 101%N.
Definition N102 := 102%N.
Definition N103 := 103%N.
Definition N104 := 104%N.
Definition N105 := 105%N.
Definition N106 := 106%N.
Definition N107 := 107%N.
Definition N108 := 108%N.
Definition N109 := 109%N.
Definition N110 := 110%N.
Definition N111 := 111%N.
Definition N112 := 112%N.
Definition N113 := 113%N.
Definition N114 := 114%N.
Definition N115 := 115%N.
Definition N116 := 116%N.
Definition N117 := 117%N.
Definition N118 := 118%N.
Definition N119 := 119%N.
Definition N120 := 120%N.
Definition N121 := 121%N.
Definition N122 := 122%N.
Definition N123 := 123%N.
Definition N124 := 124%N.
Definition N125 := 125%N.
Definition N126 := 126%N.
Definition N127 := 127%N.
Definition N128 := 128%N.
Definition N129 := 129%N.
Definition N130 := 130%N.
Definition N131 := 131%N.
Definition N132 := 132%N.
Definition N133 := 133%N.
Definition N134 := 134%N.
Definition N135 := 135%N.
Definition N136 := 136%N.
Definition N137 := 137%N.
Definition N138 := 138%N.
Definition N139 := 139%N.
Definition N140 := 140%N.
Definition N141 := 141%N.
Definition N142 := 142%N.
Definition N143 := 143%N.
Definition N144 := 144%N.
Definition N145 := 145%N.
Definition N146 := 146%N.
Definition N147 := 147%N.
Definition N148 := 148%N.
Definition N149 := 149%N.
Definition N150 := 150%N.
Definition N151 := 151%N.
Definition N152 := 152%N.
Definition N153 := 153%N.
Definition N154 := 154%N.
Definition N155 := 155%N.
Definition N156 := 156%N.
Definition N157 := 157%N.
Definition N158 := 158%N.
Definition N159 := 159%N.
Definition N160 := 160%N.
Definition N161 := 161%N.
Definition N162 := 162%N.
Definition N163 := 163%N.
Definition N164 := 164%N.
Definition N165 := 165%N.
Definition N166 := 166%N.
Definition N167 := 167%N.
Definition N168 := 168%N.
Definition N169 := 169%N.
Definition N170 := 170%N.
Definition N171 := 171%N.
Definition N172 := 172%N.
Definition N173 := 173%N.
Definition N174 := 174%N.
Definition N175 := 175%N.
Definition N176 := 176%N.
Definition N177 := 177%N.
Definition N178 := 178%N.
Definition N179 := 179%N.
Definition N180 := 180%N.
Definition N181 := 181%N.
Definition N182 := 182%N.
Definition N183 := 183%N.
Definition N184 := 184%N.
Definition N185 := 185%N.
Definition N186 := 186%N.
Definition N187 := 187%N.
Definition N188 := 188%N.
Definition N189 := 189%N.
Definition N190 := 190%N.
Definition N191 := 191%N.
Definition N192 := 192%N.
Definition N193 := 193%N.
Definition N194 := 194%N.
Definition N195 := 195%N.
Definition N196 := 196%N.
Definition N197 := 197%N.
Definition N198 := 198%N.
Definition N199 := 199%N.
Definition N200 := 200%N.
Definition N201 := 201%N.
Definition N202 := 202%N.
Definition N203 := 203%N.
Definition N204 := 204%N.
Definition N205 := 205%N.
Definition N206 := 206%N.
Definition N207 := 207%N.
Definition N208 := 208%N.
Definition N209 := 209%N.
Definition N210 := 210%N.
Definition N211 := 211%N.
Definition N212 := 212%N.
Definition N213 := 213%N.
Definition N214 := 214%N.
Definition N215 := 215%N.
Definition N216 := 216%N.
Definition N217 := 217%N.
Definition N218 := 218%N.
Definition N219 := 219%N.
Definition N220 := 220%N.
Definition N221 := 221%N.
Definition N222 := 222%N.
Definition N223 := 223%N.
Definition N224 := 224%N.
Definition N225 := 225%N.
Definition N226 := 226%N.
Definition N227 := 227%N.
Definition N228 := 228%N.
Definition N229 := 229%N.
Definition N230 := 230%N.
Definition N231 := 231%N.
Definition N232 := 232%N.
Definition N233 := 233%N.
Definition N234 := 234%N.
Definition N235 := 235%N.
Definition N236 := 236%N.
Definition N237 := 237%N.
Definition N238 := 238%N.
Definition N239 := 239%N.
Definition N240 := 240%N.
Definition N241 := 241%N.
Definition N242 := 242%N.
Definition N243 := 243%N.
Definition N244 := 244%N.
Definition N245 := 245%N.
Definition N246 := 246%N.
Definition N247 := 247%N.
Definition N248 := 248%N.
Definition N249 := 249%N.
Definition N250 := 250%N.
Definition N251 := 251%N.
Definition N252 := 252%N.
Definition N253 := 253%N.
Definition N254 := 254%N.
Definition N255 := 255%N.
Definition to_N (x : byte) :=
match x with
| "000"%byte ⇒ N0
| "001"%byte ⇒ N1
| "002"%byte ⇒ N2
| "003"%byte ⇒ N3
| "004"%byte ⇒ N4
| "005"%byte ⇒ N5
| "006"%byte ⇒ N6
| "007"%byte ⇒ N7
| "008"%byte ⇒ N8
| "009"%byte ⇒ N9
| "010"%byte ⇒ N10
| "011"%byte ⇒ N11
| "012"%byte ⇒ N12
| "013"%byte ⇒ N13
| "014"%byte ⇒ N14
| "015"%byte ⇒ N15
| "016"%byte ⇒ N16
| "017"%byte ⇒ N17
| "018"%byte ⇒ N18
| "019"%byte ⇒ N19
| "020"%byte ⇒ N20
| "021"%byte ⇒ N21
| "022"%byte ⇒ N22
| "023"%byte ⇒ N23
| "024"%byte ⇒ N24
| "025"%byte ⇒ N25
| "026"%byte ⇒ N26
| "027"%byte ⇒ N27
| "028"%byte ⇒ N28
| "029"%byte ⇒ N29
| "030"%byte ⇒ N30
| "031"%byte ⇒ N31
| "032"%byte ⇒ N32
| "033"%byte ⇒ N33
| "034"%byte ⇒ N34
| "035"%byte ⇒ N35
| "036"%byte ⇒ N36
| "037"%byte ⇒ N37
| "038"%byte ⇒ N38
| "039"%byte ⇒ N39
| "040"%byte ⇒ N40
| "041"%byte ⇒ N41
| "042"%byte ⇒ N42
| "043"%byte ⇒ N43
| "044"%byte ⇒ N44
| "045"%byte ⇒ N45
| "046"%byte ⇒ N46
| "047"%byte ⇒ N47
| "048"%byte ⇒ N48
| "049"%byte ⇒ N49
| "050"%byte ⇒ N50
| "051"%byte ⇒ N51
| "052"%byte ⇒ N52
| "053"%byte ⇒ N53
| "054"%byte ⇒ N54
| "055"%byte ⇒ N55
| "056"%byte ⇒ N56
| "057"%byte ⇒ N57
| "058"%byte ⇒ N58
| "059"%byte ⇒ N59
| "060"%byte ⇒ N60
| "061"%byte ⇒ N61
| "062"%byte ⇒ N62
| "063"%byte ⇒ N63
| "064"%byte ⇒ N64
| "065"%byte ⇒ N65
| "066"%byte ⇒ N66
| "067"%byte ⇒ N67
| "068"%byte ⇒ N68
| "069"%byte ⇒ N69
| "070"%byte ⇒ N70
| "071"%byte ⇒ N71
| "072"%byte ⇒ N72
| "073"%byte ⇒ N73
| "074"%byte ⇒ N74
| "075"%byte ⇒ N75
| "076"%byte ⇒ N76
| "077"%byte ⇒ N77
| "078"%byte ⇒ N78
| "079"%byte ⇒ N79
| "080"%byte ⇒ N80
| "081"%byte ⇒ N81
| "082"%byte ⇒ N82
| "083"%byte ⇒ N83
| "084"%byte ⇒ N84
| "085"%byte ⇒ N85
| "086"%byte ⇒ N86
| "087"%byte ⇒ N87
| "088"%byte ⇒ N88
| "089"%byte ⇒ N89
| "090"%byte ⇒ N90
| "091"%byte ⇒ N91
| "092"%byte ⇒ N92
| "093"%byte ⇒ N93
| "094"%byte ⇒ N94
| "095"%byte ⇒ N95
| "096"%byte ⇒ N96
| "097"%byte ⇒ N97
| "098"%byte ⇒ N98
| "099"%byte ⇒ N99
| "100"%byte ⇒ N100
| "101"%byte ⇒ N101
| "102"%byte ⇒ N102
| "103"%byte ⇒ N103
| "104"%byte ⇒ N104
| "105"%byte ⇒ N105
| "106"%byte ⇒ N106
| "107"%byte ⇒ N107
| "108"%byte ⇒ N108
| "109"%byte ⇒ N109
| "110"%byte ⇒ N110
| "111"%byte ⇒ N111
| "112"%byte ⇒ N112
| "113"%byte ⇒ N113
| "114"%byte ⇒ N114
| "115"%byte ⇒ N115
| "116"%byte ⇒ N116
| "117"%byte ⇒ N117
| "118"%byte ⇒ N118
| "119"%byte ⇒ N119
| "120"%byte ⇒ N120
| "121"%byte ⇒ N121
| "122"%byte ⇒ N122
| "123"%byte ⇒ N123
| "124"%byte ⇒ N124
| "125"%byte ⇒ N125
| "126"%byte ⇒ N126
| "127"%byte ⇒ N127
| "128"%byte ⇒ N128
| "129"%byte ⇒ N129
| "130"%byte ⇒ N130
| "131"%byte ⇒ N131
| "132"%byte ⇒ N132
| "133"%byte ⇒ N133
| "134"%byte ⇒ N134
| "135"%byte ⇒ N135
| "136"%byte ⇒ N136
| "137"%byte ⇒ N137
| "138"%byte ⇒ N138
| "139"%byte ⇒ N139
| "140"%byte ⇒ N140
| "141"%byte ⇒ N141
| "142"%byte ⇒ N142
| "143"%byte ⇒ N143
| "144"%byte ⇒ N144
| "145"%byte ⇒ N145
| "146"%byte ⇒ N146
| "147"%byte ⇒ N147
| "148"%byte ⇒ N148
| "149"%byte ⇒ N149
| "150"%byte ⇒ N150
| "151"%byte ⇒ N151
| "152"%byte ⇒ N152
| "153"%byte ⇒ N153
| "154"%byte ⇒ N154
| "155"%byte ⇒ N155
| "156"%byte ⇒ N156
| "157"%byte ⇒ N157
| "158"%byte ⇒ N158
| "159"%byte ⇒ N159
| "160"%byte ⇒ N160
| "161"%byte ⇒ N161
| "162"%byte ⇒ N162
| "163"%byte ⇒ N163
| "164"%byte ⇒ N164
| "165"%byte ⇒ N165
| "166"%byte ⇒ N166
| "167"%byte ⇒ N167
| "168"%byte ⇒ N168
| "169"%byte ⇒ N169
| "170"%byte ⇒ N170
| "171"%byte ⇒ N171
| "172"%byte ⇒ N172
| "173"%byte ⇒ N173
| "174"%byte ⇒ N174
| "175"%byte ⇒ N175
| "176"%byte ⇒ N176
| "177"%byte ⇒ N177
| "178"%byte ⇒ N178
| "179"%byte ⇒ N179
| "180"%byte ⇒ N180
| "181"%byte ⇒ N181
| "182"%byte ⇒ N182
| "183"%byte ⇒ N183
| "184"%byte ⇒ N184
| "185"%byte ⇒ N185
| "186"%byte ⇒ N186
| "187"%byte ⇒ N187
| "188"%byte ⇒ N188
| "189"%byte ⇒ N189
| "190"%byte ⇒ N190
| "191"%byte ⇒ N191
| "192"%byte ⇒ N192
| "193"%byte ⇒ N193
| "194"%byte ⇒ N194
| "195"%byte ⇒ N195
| "196"%byte ⇒ N196
| "197"%byte ⇒ N197
| "198"%byte ⇒ N198
| "199"%byte ⇒ N199
| "200"%byte ⇒ N200
| "201"%byte ⇒ N201
| "202"%byte ⇒ N202
| "203"%byte ⇒ N203
| "204"%byte ⇒ N204
| "205"%byte ⇒ N205
| "206"%byte ⇒ N206
| "207"%byte ⇒ N207
| "208"%byte ⇒ N208
| "209"%byte ⇒ N209
| "210"%byte ⇒ N210
| "211"%byte ⇒ N211
| "212"%byte ⇒ N212
| "213"%byte ⇒ N213
| "214"%byte ⇒ N214
| "215"%byte ⇒ N215
| "216"%byte ⇒ N216
| "217"%byte ⇒ N217
| "218"%byte ⇒ N218
| "219"%byte ⇒ N219
| "220"%byte ⇒ N220
| "221"%byte ⇒ N221
| "222"%byte ⇒ N222
| "223"%byte ⇒ N223
| "224"%byte ⇒ N224
| "225"%byte ⇒ N225
| "226"%byte ⇒ N226
| "227"%byte ⇒ N227
| "228"%byte ⇒ N228
| "229"%byte ⇒ N229
| "230"%byte ⇒ N230
| "231"%byte ⇒ N231
| "232"%byte ⇒ N232
| "233"%byte ⇒ N233
| "234"%byte ⇒ N234
| "235"%byte ⇒ N235
| "236"%byte ⇒ N236
| "237"%byte ⇒ N237
| "238"%byte ⇒ N238
| "239"%byte ⇒ N239
| "240"%byte ⇒ N240
| "241"%byte ⇒ N241
| "242"%byte ⇒ N242
| "243"%byte ⇒ N243
| "244"%byte ⇒ N244
| "245"%byte ⇒ N245
| "246"%byte ⇒ N246
| "247"%byte ⇒ N247
| "248"%byte ⇒ N248
| "249"%byte ⇒ N249
| "250"%byte ⇒ N250
| "251"%byte ⇒ N251
| "252"%byte ⇒ N252
| "253"%byte ⇒ N253
| "254"%byte ⇒ N254
| "255"%byte ⇒ N255
end.
End ByteN.
Definition eqb (x y : byte) :=
N.eqb (ByteN.to_N x) (ByteN.to_N y).
Definition compare (x y : byte) :=
N.compare (ByteN.to_N x) (ByteN.to_N y).