Number.eg_up: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/src/math/number.bend as Number
Lines 40-46 of bend-collections-laws-math@1.0.0.0/src/math/number.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/src/math/number.bend&start_line=40&end_line=46

import Base

# From the child (b, a mod b) to the parent (a, b): with q = a div b the
# coefficients become (y', x' + q*y') and the sign flips (Knuth 4.5.2,
# algorithm X, in magnitudes).
def eg_up(+q: Nat, r: EGcd) -> EGcd:
  match r:
    case EG{+g, +x, +y, neg}:
      EG{g, y, Nat.add(x, Nat.mul(q, y)), Bool.not(neg)}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  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/src/math/number.bend&name=EGcd