fact: Definition of_nat (x : nat) : option byte := match x with | 0 => Some x00 | 1 => Some x01 | 2 => Some x02 | 3 => Some x03 | 4 => Some x04 | 5 => Some x05 | 6 => Some x06 | 7 => Some x07 | 8 => Some x08 | 9 => Some x09 | 10 => Some x0a | 11 => Some x0b | 12 => Some x0c | 13 => Some x0d | 14 => Some x0e | 15 => Some x0f | 16 => Some x10 | 17 => Some x11 | 18 => Some x12 | 19 => Some x13 | 20 => Some x14 | 21 => Some x15 | 22 => Some x16 | 23 => Some x17 | 24 => Some x18 | 25 => Some x19 | 26 => Some x1a | 27 => Some x1b | 28 => Some x1c | 29 => Some x1d | 30 => Some x1e | 31 => Some x1f | 32 => Some x20 | 33 => Some x21 | 34 => Some x22 | 35 => Some x23 | 36 => Some x24 | 37 => Some x25 | 38 => Some x26 | 39 => Some x27 | 40 => Some x28 | 41 => Some x29 | 42 => Some x2a | 43 => Some x2b | 44 => Some x2c | 45 => Some x2d | 46 => Some x2e | 47 => Some x2f | 48 => Some x30 | 49 => Some x31 | 50 => Some x32 | 51 => Some x33 | 52 => Some x34 | 53 => Some x35 | 54 => Some x36 | 55 => Some x37 | 56 => Some x38 | 57 => Some x39 | 58 => Some x3a | 59 => Some x3b | 60 => Some x3c | 61 => Some x3d | 62 => Some x3e | 63 => Some x3f | 64 => Some x40 | 65 => Some x41 | 66 => Some x42 | 67 => Some x43 | 68 => Some x44 | 69 => Some x45 | 70 => Some x46 | 71 => Some x47 | 72 => Some x48 | 73 => Some x49 | 74 => Some x4a | 75 => Some x4b | 76 => Some x4c | 77 => Some x4d | 78 => Some x4e | 79 => Some x4f | 80 => Some x50 | 81 => Some x51 | 82 => Some x52 | 83 => Some x53 | 84 => Some x54 | 85 => Some x55 | 86 => Some x56 | 87 => Some x57 | 88 => Some x58 | 89 => Some x59 | 90 => Some x5a | 91 => Some x5b | 92 => Some x5c | 93 => Some x5d | 94 => Some x5e | 95 => Some x5f | 96 => Some x60 | 97 => Some x61 | 98 => Some x62 | 99 => Some x63 | 100 => Some x64 | 101 => Some x65 | 102 => Some x66 | 103 => Some x67 | 104 => Some x68 | 105 => Some x69 | 106 => Some x6a | 107 => Some x6b | 108 => Some x6c | 109 => Some x6d | 110 => Some x6e | 111 => Some x6f | 112 => Some x70 | 113 => Some x71 | 114 => Some x72 | 115 => Some x73 | 116 => Some x74 | 117 => Some x75 | 118 => Some x76 | 119 => Some x77 | 120 => Some x78 | 121 => Some x79 | 122 => Some x7a | 123 => Some x7b | 124 => Some x7c | 125 => Some x7d | 126 => Some x7e | 127 => Some x7f | 128 => Some x80 | 129 => Some x81 | 130 => Some x82 | 131 => Some x83 | 132 => Some x84 | 133 => Some x85 | 134 => Some x86 | 135 => Some x87 | 136 => Some x88 | 137 => Some x89 | 138 => Some x8a | 139 => Some x8b | 140 => Some x8c | 141 => Some x8d | 142 => Some x8e | 143 => Some x8f | 144 => Some x90 | 145 => Some x91 | 146 => Some x92 | 147 => Some x93 | 148 => Some x94 | 149 => Some x95 | 150 => Some x96 | 151 => Some x97 | 152 => Some x98 | 153 => Some x99 | 154 => Some x9a | 155 => Some x9b | 156 => Some x9c | 157 => Some x9d | 158 => Some x9e | 159 => Some x9f | 160 => Some xa0 | 161 => Some xa1 | 162 => Some xa2 | 163 => Some xa3 | 164 => Some xa4 | 165 => Some xa5 | 166 => Some xa6 | 167 => Some xa7 | 168 => Some xa8 | 169 => Some xa9 | 170 => Some xaa | 171 => Some xab | 172 => Some xac | 173 => Some xad | 174 => Some xae | 175 => Some xaf | 176 => Some xb0 | 177 => Some xb1 | 178 => Some xb2 | 179 => Some xb3 | 180 => Some xb4 | 181 => Some xb5 | 182 => Some xb6 | 183 => Some xb7 | 184 => Some xb8 | 185 => Some xb9 | 186 => Some xba | 187 => Some xbb | 188 => Some xbc | 189 => Some xbd | 190 => Some xbe | 191 => Some xbf | 192 => Some xc0 | 193 => Some xc1 | 194 => Some xc2 | 195 => Some xc3 | 196 => Some xc4 | 197 => Some xc5 | 198 => Some xc6 | 199 => Some xc7 | 200 => Some xc8 | 201 => Some xc9 | 202 => Some xca | 203 => Some xcb | 204 => Some xcc | 205 => Some xcd | 206 => Some xce | 207 => Some xcf | 208 => Some xd0 | 209 => Some xd1 | 210 => Some xd2 | 211 => Some xd3 | 212 => Some xd4 | 213 => Some xd5 | 214 => Some xd6 | 215 => Some xd7 | 216 => Some xd8 | 217 => Some xd9 | 218 => Some xda | 219 => Some xdb | 220 => Some xdc | 221 => Some xdd | 222 => Some xde | 223 => Some xdf | 224 => Some xe0 | 225 => Some xe1 | 226 => Some xe2 | 227 => Some xe3 | 228 => Some xe4 | 229 => Some xe5 | 230 => Some xe6 | 231 => Some xe7 | 232 => Some xe8 | 233 => Some xe9 | 234 => Some xea | 235 => Some xeb | 236 => Some xec | 237 => Some xed | 238 => Some xee | 239 => Some xef | 240 => Some xf0 | 241 => Some xf1 | 242 => Some xf2 | 243 => Some xf3 | 244 => Some xf4 | 245 => Some xf5 | 246 => Some xf6 | 247 => Some xf7 | 248 => Some xf8 | 249 => Some xf9 | 250 => Some xfa | 251 => Some xfb | 252 => Some xfc | 253 => Some xfd | 254 => Some xfe | 255 => Some xff | _ => None end.
imports: Coq.Arith.EqNat Coq.NArith.BinNat Coq.NArith.Nnat Coq.Init.Byte