def pk.u8.c7
import bend-osdev-pkcs7@0.1.0.0/PROOF.bend as PROOFimport Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
244# BEGIN GENERATED by gen/pkcs7_proof.py: u8
245# the values 224 to 255
246def pk.u8.c7(r: Nat) -> {Nat.is_le(224n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(224n+r))) == 224n+r : Nat}:
247 match r:
248 case 0n:
249 h => {==}
250 case 1n+r1:
251 match r1:
252 case 0n:
253 h => {==}
254 case 1n+r2:
255 match r2:
256 case 0n:
257 h => {==}
258 case 1n+r3:
259 match r3:
260 case 0n:
261 h => {==}
262 case 1n+r4:
263 match r4:
264 case 0n:
265 h => {==}
266 case 1n+r5:
267 match r5:
268 case 0n:
269 h => {==}
270 case 1n+r6:
271 match r6:
272 case 0n:
273 h => {==}
274 case 1n+r7:
275 match r7:
276 case 0n:
277 h => {==}
278 case 1n+r8:
279 match r8:
280 case 0n:
281 h => {==}
282 case 1n+r9:
283 match r9:
284 case 0n:
285 h => {==}
286 case 1n+r10:
287 match r10:
288 case 0n:
289 h => {==}
290 case 1n+r11:
291 match r11:
292 case 0n:
293 h => {==}
294 case 1n+r12:
295 match r12:
296 case 0n:
297 h => {==}
298 case 1n+r13:
299 match r13:
300 case 0n:
301 h => {==}
302 case 1n+r14:
303 match r14:
304 case 0n:
305 h => {==}
306 case 1n+r15:
307 match r15:
308 case 0n:
309 h => {==}
310 case 1n+r16:
311 match r16:
312 case 0n:
313 h => {==}
314 case 1n+r17:
315 match r17:
316 case 0n:
317 h => {==}
318 case 1n+r18:
319 match r18:
320 case 0n:
321 h => {==}
322 case 1n+r19:
323 match r19:
324 case 0n:
325 h => {==}
326 case 1n+r20:
327 match r20:
328 case 0n:
329 h => {==}
330 case 1n+r21:
331 match r21:
332 case 0n:
333 h => {==}
334 case 1n+r22:
335 match r22:
336 case 0n:
337 h => {==}
338 case 1n+r23:
339 match r23:
340 case 0n:
341 h => {==}
342 case 1n+r24:
343 match r24:
344 case 0n:
345 h => {==}
346 case 1n+r25:
347 match r25:
348 case 0n:
349 h => {==}
350 case 1n+r26:
351 match r26:
352 case 0n:
353 h => {==}
354 case 1n+r27:
355 match r27:
356 case 0n:
357 h => {==}
358 case 1n+r28:
359 match r28:
360 case 0n:
361 h => {==}
362 case 1n+r29:
363 match r29:
364 case 0n:
365 h => {==}
366 case 1n+r30:
367 match r30:
368 case 0n:
369 h => {==}
370 case 1n+r31:
371 match r31:
372 case 0n:
373 h => {==}
374 case 1n+r32:
375 h => pk.absurd({U32.to_nat(B.byte(U32.from_nat(256n+r32))) == 256n+r32 : Nat}, h)