def eg_pos

bend-collections-laws-math@1.0.0.0 · spec/math/number.bend:41

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

41# the signed Bezout identity a*x - b*y == g (neg false) or b*y - a*x == g
42# (neg true), stated without subtraction: the positive side equals g plus
43# the negative side
44def eg_pos(+a: Nat, +b: Nat, r: NB.EGcd) -> Nat:
45  match r:
46    case NB.EG{g, +x, +y, neg}:
47      match neg:
48        case True{}:
49          Nat.mul(b, y)
50        case False{}:
51          Nat.mul(a, x)