def up_sign

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

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

70def up_sign(+a: Nat, +b: Nat, +q: Nat, +r: Nat, +ha: {a == Nat.add(Nat.mul(q, b), r) : Nat}, +g: Nat, +x: Nat, +y: Nat, +neg: Bool, +ih: {SN.eg_pos(b, r, NB.EG{g, x, y, neg}) == SN.eg_neg(b, r, NB.EG{g, x, y, neg}) : Nat}) -> {SN.eg_pos(a, b, NB.eg_up(q, NB.EG{g, x, y, neg})) == SN.eg_neg(a, b, NB.eg_up(q, NB.EG{g, x, y, neg})) : Nat}:
71  match neg:
72    case False{}:
73      %Equal.sym(Nat, a, Nat.add(Nat.mul(q, b), r), ha) : {Nat.mul(b, Nat.add(x, Nat.mul(q, y))) == Nat.add(g, Nat.mul(_, y)) : Nat}
74      alg_pos(g, x, y, q, b, r, ih)
75    case True{}:
76      %Equal.sym(Nat, a, Nat.add(Nat.mul(q, b), r), ha) : {Nat.mul(_, y) == Nat.add(g, Nat.mul(b, Nat.add(x, Nat.mul(q, y)))) : Nat}
77      alg_neg(g, x, y, q, b, r, ih)