Lcm.lcm_pos: 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 120-124 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=120&end_line=124

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 lcm_pos(+ap: Nat, +bp: Nat) -> {M.lcm(1n+ap, 1n+bp) == Nat.mul(G.wl(G.ws(1n+bp, 1n+ap, 1n+bp)), 1n+bp) : Nat}:
  +g = M.gcd(1n+ap, 1n+bp)
  +la = G.wl(G.ws(1n+bp, 1n+ap, 1n+bp))
  +ea = G.gcd_dvd_left(1n+ap, 1n+bp)
  Equal.cong(Nat, Nat, z => Nat.mul(z, 1n+bp), Nat.div(1n+ap, g), la, div_exact(1n+ap, la, g, gcd_pos(ap, la, g, ea), ea))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  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=wl
  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=div_exact
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend&name=gcd_pos
  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