Egcd.up_bez: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/number/egcd.bend as Egcd
Lines 79-84 of bend-collections-laws-math@1.0.0.0/proofs/math/number/egcd.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/egcd.bend&start_line=79&end_line=84

import Base
import bend-collections-laws-math@1.0.0.0/src/math/number.bend as NB
import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN

# one level up: from the child's identity for (b, r) to the parent's for
# (a, b), a == q b + r
def up_bez(+a: Nat, +b: Nat, +q: Nat, +r: Nat, +ha: {a == Nat.add(Nat.mul(q, b), r) : Nat}, c: NB.EGcd, +ih: {SN.eg_pos(b, r, c) == SN.eg_neg(b, r, c) : Nat}) -> {SN.eg_pos(a, b, NB.eg_up(q, c)) == SN.eg_neg(a, b, NB.eg_up(q, c)) : Nat}:
  match c:
    case NB.EG{+g, +x, +y, +neg}:
      up_sign(a, b, q, r, ha, g, x, y, neg, ih)

Uses (8):
  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.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/egcd.bend&name=up_sign
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/number.bend&name=eg_neg
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/number.bend&name=eg_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/number.bend&name=EGcd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/number.bend&name=eg_up