Lists.lcm_all_dvd: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lists.bend as Lists
Lines 184-186 of bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lists.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lists.bend&start_line=184&end_line=186

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M

# lcm_all(xs) divides every common multiple of the elements   (Mathlib Finset.lcm_dvd)
def lcm_all_dvd(+m: Nat, +xs: List<&2, Nat>, +ks: List<&2, Nat>, h: mul_with(m, xs, ks)) -> {m == Nat.mul(lw_mul(m, xs, ks, 1n, m), M.lcm_all(xs)) : Nat}:
  l_mul(m, xs, ks, 1n, m, Equal.sym(Nat, Nat.mul(m, 1n), m, A.mul_one(m)), h)

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_one
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lists.bend&name=l_mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lists.bend&name=lw_mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lists.bend&name=mul_with
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend&name=lcm_all