PROOF.pk.sub_succ: def of bend-osdev-pkcs7@0.1.0.0
Import: import bend-osdev-pkcs7@0.1.0.0/PROOF.bend as PROOF
Lines 77-86 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=77&end_line=86

import Base

# r <= q gives (1 + q) - r = 1 + (q - r)
def pk.sub_succ(+r: Nat, +q: Nat) -> {Nat.is_le(r, q) == True{} : Bool} -> {Nat.sub(1n+q, r) == 1n+Nat.sub(q, r) : Nat}:
  match r q:
    case 0n _:
      h => %Equal.sym(Nat, Nat.sub(q, 0n), q, pk.sub_zero(q)) : {1n+q == 1n+_ : Nat}
        {==}
    case 1n+rp 0n:
      h => pk.absurd({Nat.sub(1n, 1n+rp) == 1n+Nat.sub(0n, 1n+rp) : Nat}, h)
    case 1n+rp 1n+qp:
      h => pk.sub_succ(rp, qp)(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=Equal.sym
  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=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.absurd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.sub_zero