def bez_go

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

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

90def 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}:
91  match f b:
92    case 0n _:
93      base(a, b)
94    case 1n+ +g 0n:
95      base(a, 0n)
96    case 1n+ +g 1n+ +bp:
97      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)))