def dvd_lcm_right

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

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

160def dvd_lcm_right(+a: Nat, +b: Nat) -> {M.lcm(a, b) == Nat.mul(lcm_wr(a, b), b) : Nat}:
161  match a b:
162    case 0n b0:
163      Equal.sym(Nat, Nat.mul(0n, b0), 0n, {==})
164    case 1n+ ap 0n:
165      Equal.sym(Nat, Nat.mul(0n, 0n), 0n, {==})
166    case 1n+ +ap 1n+ +bp:
167      lcm_pos(ap, bp)