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

import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

# (1 + m + r) - r = 1 + m
def pk.sub_add_r(+m: Nat, +r: Nat) -> {Nat.sub(1n+Nat.add(m, r), r) == 1n+m : Nat}:
  match r:
    case 0n:
      %UL.nat_add_zero(m) : {Nat.sub(1n+Nat.add(m, 0n), 0n) == 1n+_ : Nat}
      {==}
    case 1n+rp:
      %Equal.sym(Nat, Nat.add(m, 1n+rp), 1n+Nat.add(m, rp), UL.nat_add_succ(m, rp)) : {Nat.sub(1n+_, 1n+rp) == 1n+m : Nat}
      pk.sub_add_r(m, rp)

Uses (6):
  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.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_succ
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_zero