Lcm.lcm_dvd: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend as Lcm
Lines 221-229 of bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend&start_line=221&end_line=229

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

# every common multiple of a and b is a multiple of lcm(a, b)   (Mathlib Nat.lcm_dvd)
def lcm_dvd(+a: Nat, +b: Nat, +m: Nat, +x: Nat, +y: Nat, +ex: {m == Nat.mul(x, a) : Nat}, +ey: {m == Nat.mul(y, b) : Nat}) -> {m == Nat.mul(lcm_dw(a, b, m, x, y), M.lcm(a, b)) : Nat}:
  match a b:
    case 0n b0:
      Equal.trans(Nat, m, Nat.mul(x, 0n), 0n, ex, A.mul_zero(x))
    case 1n+ ap 0n:
      Equal.trans(Nat, m, Nat.mul(y, 0n), 0n, ey, A.mul_zero(y))
    case 1n+ +ap 1n+ +bp:
      lcm_dvd_pos(ap, bp, m, x, y, ex, ey)

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend&name=lcm_dvd_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend&name=lcm_dw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend&name=lcm