def dvd_lcm_all

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/lists.bend:157

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M

157# every element divides lcm_all(xs) (1 past the end)   (Mathlib Finset.dvd_lcm)
158def dvd_lcm_all(+xs: List<&2, Nat>, +i: Nat) -> {M.lcm_all(xs) == Nat.mul(lw_nth(xs, 1n, i), nth0(xs, i, 1n)) : Nat}:
159  l_nth(xs, 1n, i)