def gcd_go

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

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
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

21def gcd_go(+f: Nat, +a: Nat, +b: Nat) -> {SN.eg_gcd(NB.egcd_go(f, a, b)) == M.gcd_go(f, a, b) : Nat}:
22  match f b:
23    case 0n _:
24      {==}
25    case 1n+ +g 0n:
26      {==}
27    case 1n+ +g 1n+ +bp:
28      %Equal.sym(Nat, SN.eg_gcd(NB.eg_up(Nat.div(a, 1n+bp), NB.egcd_go(g, 1n+bp, Nat.mod(a, 1n+bp)))), SN.eg_gcd(NB.egcd_go(g, 1n+bp, Nat.mod(a, 1n+bp))), up_gcd(Nat.div(a, 1n+bp), NB.egcd_go(g, 1n+bp, Nat.mod(a, 1n+bp)))) : {_ == M.gcd_go(1n+g, a, 1n+bp) : Nat}
29      gcd_go(g, 1n+bp, Nat.mod(a, 1n+bp))