def gcd_val
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:182
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int.bend as U32int
import Base
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
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/instances.bend as I
182def gcd_val(+a: U32, +b: U32) -> {v(G.gcd(~U32, ~I.u32_op, ~I.u32_is, a, b)) == M.gcd(v(a), v(b)) : Nat}:
183 gcd_val_k(32n, {==}, a, b)