def prod_ok
bend-collections-laws-math@1.0.0.0 · proofs/math/natural/lists.bend:37
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/lists.bend as Lists
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/proofs/math/natural/lcm.bend as LC
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S
37def prod_ok(+xs: List<&2, Nat>) -> {M.prod(xs) == S.lprod(xs) : Nat}:
38 Equal.trans(Nat, M.prod(xs), Nat.mul(1n, S.lprod(xs)), S.lprod(xs), prod_go(xs, 1n), LC.one_mul(S.lprod(xs)))