def gcd_all_agrees

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:201

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
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/num.bend as NM
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

201def gcd_all_agrees(+xs: List<&2, U32>) -> SG.GcdAll.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, xs):
202  +z = I.u32_op(NM.ZeroOp{})
203  as_of(G.gcd_all(~U32, ~I.u32_op, ~I.u32_is, xs), M.gcd_all(vals(xs)), Equal.trans(Nat, v(G.gcd_all_go(~U32, ~I.u32_op, ~I.u32_is, xs, z)), M.gcd_all_go(vals(xs), v(z)), M.gcd_all_go(vals(xs), 0n), gall(xs, z), Equal.cong(Nat, Nat, t => M.gcd_all_go(vals(xs), t), v(z), 0n, zero_v())))