Lcm.scale_dvd: 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 61-63 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=61&end_line=63

import Base

# x == w g gives c x == w (c g)
def scale_dvd(+c: Nat, +x: Nat, +w: Nat, +g: Nat, +e: {x == Nat.mul(w, g) : Nat}) -> {Nat.mul(c, x) == Nat.mul(w, Nat.mul(c, g)) : Nat}:
  Equal.trans(Nat, Nat.mul(c, x), Nat.mul(c, Nat.mul(w, g)), Nat.mul(w, Nat.mul(c, g)), Equal.cong(Nat, Nat, z => Nat.mul(c, z), x, Nat.mul(w, g), e), swap_cw(c, w, g))

Uses (5):
  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.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/math/natural/lcm.bend&name=swap_cw