def gcd_greatest

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/gcd.bend:98

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as R

98def gcd_greatest(fuel: Nat, +a: Nat, +b: Nat, +hb: {Nat.is_le(b, fuel) == True{} : Bool}, +d: Nat, +ka: Nat, +kb: Nat, +ea: {a == Nat.mul(ka, d) : Nat}, +eb: {b == Nat.mul(kb, d) : Nat}) -> {M.gcd_go(fuel, a, b) == Nat.mul(dw(fuel, a, b, ka, kb), d) : Nat}:
99  match fuel b:
100    case 0n 0n:
101      ea
102    case 0n 1n+bp:
103      Empty.absurd({M.gcd_go(0n, a, 1n+bp) == Nat.mul(dw(0n, a, 1n+bp, ka, kb), d) : Nat}, L.false_true(hb))
104    case 1n+f 0n:
105      ea
106    case 1n+ +f 1n+ +bp:
107      gcd_greatest(f, 1n+bp, Nat.mod(a, 1n+bp), N.le_trans(Nat.mod(a, 1n+bp), bp, f, N.lt_succ_le(Nat.mod(a, 1n+bp), bp, R.dm_lt(bp, a)), hb), d, kb, Nat.sub(ka, Nat.mul(Nat.div(a, 1n+bp), kb)), eb, dvd_mod(bp, a, d, ka, kb, ea, eb))