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

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

# a + (1 + q - (a mod (1 + q))) is a multiple of 1 + q
def pk.mod_pad(+a: Nat, +m: Nat, +d: Nat, +r: Nat, +q: Nat) -> {Nat.add(m, r) == q : Nat} -> {Pair.snd(Nat, Nat, Nat.divmod.go(Nat.add(a, Nat.sub(1n+q, Pair.snd(Nat, Nat, Nat.divmod.go(a, m, d, r)))), m, d, r)) == 0n : Nat}:
  match a:
    case 0n:
      inv => %inv : {Pair.snd(Nat, Nat, Nat.divmod.go(Nat.sub(1n+_, r), m, d, r)) == 0n : Nat}
        %Equal.sym(Nat, Nat.sub(1n+Nat.add(m, r), r), 1n+m, pk.sub_add_r(m, r)) : {Pair.snd(Nat, Nat, Nat.divmod.go(_, m, d, r)) == 0n : Nat}
        %UL.nat_add_zero(m) : {Pair.snd(Nat, Nat, Nat.divmod.go(1n+_, m, d, r)) == 0n : Nat}
        %Equal.sym(Nat & Nat, Nat.divmod.go(1n+Nat.add(m, 0n), m, d, r), Nat.divmod.go(0n, Nat.add(m, r), 1n+d, 0n), pk.go_skip(m, 0n, d, r)) : {Pair.snd(Nat, Nat, _) == 0n : Nat}
        {==}
    case 1n+ap:
      match m:
        case 0n:
          inv => pk.mod_pad(ap, r, 1n+d, 0n, q)(Equal.trans(Nat, Nat.add(r, 0n), r, q, UL.nat_add_zero(r), inv))
        case 1n+mp:
          inv => pk.mod_pad(ap, mp, d, 1n+r, q)(Equal.trans(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), q, UL.nat_add_succ(mp, r), inv))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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.divmod.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.go_skip
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.sub_add_r
  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