Lcm.dvd_lcm_left: 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 145-158 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=145&end_line=158

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

def dvd_lcm_left(+a: Nat, +b: Nat) -> {M.lcm(a, b) == Nat.mul(lcm_wl(a, b), a) : Nat}:
  match a b:
    case 0n b0:
      {==}
    case 1n+ ap 0n:
      {==}
    case 1n+ +ap 1n+ +bp:
      +g = M.gcd(1n+ap, 1n+bp)
      +la = G.wl(G.ws(1n+bp, 1n+ap, 1n+bp))
      +lb = G.wr(G.ws(1n+bp, 1n+ap, 1n+bp))
      %Equal.sym(Nat, M.lcm(1n+ap, 1n+bp), Nat.mul(la, 1n+bp), lcm_pos(ap, bp)) : {_ == Nat.mul(lb, 1n+ap) : Nat}
      %Equal.sym(Nat, 1n+bp, Nat.mul(lb, g), G.gcd_dvd_right(1n+ap, 1n+bp)) : {Nat.mul(la, _) == Nat.mul(lb, 1n+ap) : Nat}
      %Equal.sym(Nat, 1n+ap, Nat.mul(la, g), G.gcd_dvd_left(1n+ap, 1n+bp)) : {Nat.mul(la, Nat.mul(lb, g)) == Nat.mul(lb, _) : Nat}
      swap_cw(la, lb, g)

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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/math/natural/gcd.bend&name=gcd_dvd_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend&name=gcd_dvd_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend&name=wl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend&name=wr
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend&name=ws
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend&name=lcm_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend&name=lcm_wl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend&name=swap_cw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend&name=gcd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend&name=lcm