Lcm.gcd_mul_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 69-92 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=69&end_line=92

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
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend as G

def gcd_mul_pos(+cp: Nat, +a: Nat, +b: Nat) -> {M.gcd(Nat.mul(1n+cp, a), Nat.mul(1n+cp, b)) == Nat.mul(1n+cp, M.gcd(a, b)) : Nat}:
  +c = {1n+cp : Nat}
  +ca = Nat.mul(c, a)
  +cb = Nat.mul(c, b)
  +g = M.gcd(a, b)
  +gc = M.gcd(ca, cb)
  +la = G.wl(G.ws(b, a, b))
  +lb = G.wr(G.ws(b, a, b))
  # c g divides gc
  +eu = G.dvd_gcd(ca, cb, Nat.mul(c, g), la, lb, scale_dvd(c, a, la, g, G.gcd_dvd_left(a, b)), scale_dvd(c, b, lb, g, G.gcd_dvd_right(a, b)))
  # c divides gc: gc == h c
  +eh = G.dvd_gcd(ca, cb, c, a, b, A.mul_comm(c, a), A.mul_comm(c, b))
  +h = G.dw(cb, ca, cb, a, b)
  # gc == h c divides c a and c b, so h divides a and b
  +ma = G.wl(G.ws(cb, ca, cb))
  +mb = G.wr(G.ws(cb, ca, cb))
  +ea2 = unscale(cp, a, ma, h, Equal.trans(Nat, ca, Nat.mul(ma, gc), Nat.mul(ma, Nat.mul(h, c)), G.gcd_dvd_left(ca, cb), Equal.cong(Nat, Nat, z => Nat.mul(ma, z), gc, Nat.mul(h, c), eh)))
  +eb2 = unscale(cp, b, mb, h, Equal.trans(Nat, cb, Nat.mul(mb, gc), Nat.mul(mb, Nat.mul(h, c)), G.gcd_dvd_right(ca, cb), Equal.cong(Nat, Nat, z => Nat.mul(mb, z), gc, Nat.mul(h, c), eh)))
  # so h divides g: g == v h, and c g == v (h c) == v gc
  +ev = G.dvd_gcd(a, b, h, ma, mb, ea2, eb2)
  +v = G.dw(b, a, b, ma, mb)
  +ecg = Equal.trans(Nat, Nat.mul(c, g), Nat.mul(v, Nat.mul(c, h)), Nat.mul(v, gc), scale_dvd(c, g, v, h, ev),
    Equal.cong(Nat, Nat, z => Nat.mul(v, z), Nat.mul(c, h), gc, Equal.trans(Nat, Nat.mul(c, h), Nat.mul(h, c), gc, A.mul_comm(c, h), Equal.sym(Nat, gc, Nat.mul(h, c), eh))))
  dvd_antisymm(gc, Nat.mul(c, g), G.dw(cb, ca, cb, la, lb), v, eu, ecg)

Uses (17):
  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-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend&name=dvd_gcd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend&name=dw
  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=dvd_antisymm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend&name=scale_dvd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend&name=unscale
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend&name=gcd