def lcm_pos

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

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

120def 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}:
121  +g = M.gcd(1n+ap, 1n+bp)
122  +la = G.wl(G.ws(1n+bp, 1n+ap, 1n+bp))
123  +ea = G.gcd_dvd_left(1n+ap, 1n+bp)
124  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))