PROOF.pk.u8.c7: def of bend-osdev-pkcs7@0.1.0.0
Import: import bend-osdev-pkcs7@0.1.0.0/PROOF.bend as PROOF
Lines 244-375 of bend-osdev-pkcs7@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&start_line=244&end_line=375

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

# BEGIN GENERATED by gen/pkcs7_proof.py: u8
# the values 224 to 255
def 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}:
  match r:
    case 0n:
      h => {==}
    case 1n+r1:
      match r1:
        case 0n:
          h => {==}
        case 1n+r2:
          match r2:
            case 0n:
              h => {==}
            case 1n+r3:
              match r3:
                case 0n:
                  h => {==}
                case 1n+r4:
                  match r4:
                    case 0n:
                      h => {==}
                    case 1n+r5:
                      match r5:
                        case 0n:
                          h => {==}
                        case 1n+r6:
                          match r6:
                            case 0n:
                              h => {==}
                            case 1n+r7:
                              match r7:
                                case 0n:
                                  h => {==}
                                case 1n+r8:
                                  match r8:
                                    case 0n:
                                      h => {==}
                                    case 1n+r9:
                                      match r9:
                                        case 0n:
                                          h => {==}
                                        case 1n+r10:
                                          match r10:
                                            case 0n:
                                              h => {==}
                                            case 1n+r11:
                                              match r11:
                                                case 0n:
                                                  h => {==}
                                                case 1n+r12:
                                                  match r12:
                                                    case 0n:
                                                      h => {==}
                                                    case 1n+r13:
                                                      match r13:
                                                        case 0n:
                                                          h => {==}
                                                        case 1n+r14:
                                                          match r14:
                                                            case 0n:
                                                              h => {==}
                                                            case 1n+r15:
                                                              match r15:
                                                                case 0n:
                                                                  h => {==}
                                                                case 1n+r16:
                                                                  match r16:
                                                                    case 0n:
                                                                      h => {==}
                                                                    case 1n+r17:
                                                                      match r17:
                                                                        case 0n:
                                                                          h => {==}
                                                                        case 1n+r18:
                                                                          match r18:
                                                                            case 0n:
                                                                              h => {==}
                                                                            case 1n+r19:
                                                                              match r19:
                                                                                case 0n:
                                                                                  h => {==}
                                                                                case 1n+r20:
                                                                                  match r20:
                                                                                    case 0n:
                                                                                      h => {==}
                                                                                    case 1n+r21:
                                                                                      match r21:
                                                                                        case 0n:
                                                                                          h => {==}
                                                                                        case 1n+r22:
                                                                                          match r22:
                                                                                            case 0n:
                                                                                              h => {==}
                                                                                            case 1n+r23:
                                                                                              match r23:
                                                                                                case 0n:
                                                                                                  h => {==}
                                                                                                case 1n+r24:
                                                                                                  match r24:
                                                                                                    case 0n:
                                                                                                      h => {==}
                                                                                                    case 1n+r25:
                                                                                                      match r25:
                                                                                                        case 0n:
                                                                                                          h => {==}
                                                                                                        case 1n+r26:
                                                                                                          match r26:
                                                                                                            case 0n:
                                                                                                              h => {==}
                                                                                                            case 1n+r27:
                                                                                                              match r27:
                                                                                                                case 0n:
                                                                                                                  h => {==}
                                                                                                                case 1n+r28:
                                                                                                                  match r28:
                                                                                                                    case 0n:
                                                                                                                      h => {==}
                                                                                                                    case 1n+r29:
                                                                                                                      match r29:
                                                                                                                        case 0n:
                                                                                                                          h => {==}
                                                                                                                        case 1n+r30:
                                                                                                                          match r30:
                                                                                                                            case 0n:
                                                                                                                              h => {==}
                                                                                                                            case 1n+r31:
                                                                                                                              match r31:
                                                                                                                                case 0n:
                                                                                                                                  h => {==}
                                                                                                                                case 1n+r32:
                                                                                                                                  h => pk.absurd({U32.to_nat(B.byte(U32.from_nat(256n+r32))) == 256n+r32 : Nat}, h)

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=byte
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.absurd