def scale_dvd

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/lcm.bend:61

import Base

61# x == w g gives c x == w (c g)
62def 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}:
63  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))