Egcd.bez_go: 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 90-97 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=90&end_line=97

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

def bez_go(+f: Nat, +a: Nat, +b: Nat) -> {SN.eg_pos(a, b, NB.egcd_go(f, a, b)) == SN.eg_neg(a, b, NB.egcd_go(f, a, b)) : Nat}:
  match f b:
    case 0n _:
      base(a, b)
    case 1n+ +g 0n:
      base(a, 0n)
    case 1n+ +g 1n+ +bp:
      up_bez(a, 1n+bp, Nat.div(a, 1n+bp), Nat.mod(a, 1n+bp), split(a, bp), NB.egcd_go(g, 1n+bp, Nat.mod(a, 1n+bp)), bez_go(g, 1n+bp, Nat.mod(a, 1n+bp)))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/egcd.bend&name=base
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/egcd.bend&name=split
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/egcd.bend&name=up_bez
  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_go