def up_bez

bend-collections-laws-math@1.0.0.0 · proofs/math/number/egcd.bend:79

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

79# one level up: from the child's identity for (b, r) to the parent's for
80# (a, b), a == q b + r
81def 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}:
82  match c:
83    case NB.EG{+g, +x, +y, +neg}:
84      up_sign(a, b, q, r, ha, g, x, y, neg, ih)