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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
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/gcd.bend as G

def lcm_dvd_pos(+ap: Nat, +bp: Nat, +m: Nat, +x: Nat, +y: Nat, +ex: {m == Nat.mul(x, 1n+ap) : Nat}, +ey: {m == Nat.mul(y, 1n+bp) : Nat}) -> {m == Nat.mul(lcm_dw(1n+ap, 1n+bp, m, x, y), M.lcm(1n+ap, 1n+bp)) : Nat}:
  +a = {1n+ap : Nat}
  +b = {1n+bp : Nat}
  +g = M.gcd(a, b)
  +l = M.lcm(a, b)
  +ab = Nat.mul(a, b)
  +t = lcm_dw(a, b, m, x, y)
  +la = G.wl(G.ws(b, a, b))
  +ea = Equal.trans(Nat, Nat.mul(m, a), Nat.mul(Nat.mul(y, b), a), Nat.mul(y, ab), Equal.cong(Nat, Nat, z => Nat.mul(z, a), m, Nat.mul(y, b), ey),
    Equal.trans(Nat, Nat.mul(Nat.mul(y, b), a), Nat.mul(y, Nat.mul(b, a)), Nat.mul(y, ab), A.mul_assoc(y, b, a), Equal.cong(Nat, Nat, z => Nat.mul(y, z), Nat.mul(b, a), ab, A.mul_comm(b, a))))
  +eb = Equal.trans(Nat, Nat.mul(m, b), Nat.mul(Nat.mul(x, a), b), Nat.mul(x, ab), Equal.cong(Nat, Nat, z => Nat.mul(z, b), m, Nat.mul(x, a), ex), A.mul_assoc(x, a, b))
  +e2 = G.dvd_gcd(Nat.mul(m, a), Nat.mul(m, b), ab, y, x, ea, eb)
  +e1 = gcd_mul_left(m, a, b)
  +e3 = Equal.sym(Nat, Nat.mul(g, l), ab, gcd_mul_lcm(a, b))
  +emg = Equal.trans(Nat, Nat.mul(m, g), M.gcd(Nat.mul(m, a), Nat.mul(m, b)), Nat.mul(t, Nat.mul(g, l)), Equal.sym(Nat, M.gcd(Nat.mul(m, a), Nat.mul(m, b)), Nat.mul(m, g), e1),
    Equal.trans(Nat, M.gcd(Nat.mul(m, a), Nat.mul(m, b)), Nat.mul(t, ab), Nat.mul(t, Nat.mul(g, l)), e2, Equal.cong(Nat, Nat, z => Nat.mul(t, z), ab, Nat.mul(g, l), e3)))
  +emg2 = Equal.trans(Nat, Nat.mul(m, g), Nat.mul(t, Nat.mul(g, l)), Nat.mul(Nat.mul(t, l), g), emg,
    Equal.trans(Nat, Nat.mul(t, Nat.mul(g, l)), Nat.mul(t, Nat.mul(l, g)), Nat.mul(Nat.mul(t, l), g), Equal.cong(Nat, Nat, z => Nat.mul(t, z), Nat.mul(g, l), Nat.mul(l, g), A.mul_comm(g, l)), Equal.sym(Nat, Nat.mul(Nat.mul(t, l), g), Nat.mul(t, Nat.mul(l, g)), A.mul_assoc(t, l, g))))
  cancel_pos(m, Nat.mul(t, l), g, gcd_pos(ap, la, g, G.gcd_dvd_left(a, b)), emg2)

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend&name=dvd_gcd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend&name=gcd_dvd_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend&name=wl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend&name=ws
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend&name=cancel_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend&name=gcd_mul_lcm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend&name=gcd_mul_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend&name=gcd_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend&name=lcm_dw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=gcd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=lcm