def dvd_lcm_left

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

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

145def dvd_lcm_left(+a: Nat, +b: Nat) -> {M.lcm(a, b) == Nat.mul(lcm_wl(a, b), a) : Nat}:
146  match a b:
147    case 0n b0:
148      {==}
149    case 1n+ ap 0n:
150      {==}
151    case 1n+ +ap 1n+ +bp:
152      +g = M.gcd(1n+ap, 1n+bp)
153      +la = G.wl(G.ws(1n+bp, 1n+ap, 1n+bp))
154      +lb = G.wr(G.ws(1n+bp, 1n+ap, 1n+bp))
155      %Equal.sym(Nat, M.lcm(1n+ap, 1n+bp), Nat.mul(la, 1n+bp), lcm_pos(ap, bp)) : {_ == Nat.mul(lb, 1n+ap) : Nat}
156      %Equal.sym(Nat, 1n+bp, Nat.mul(lb, g), G.gcd_dvd_right(1n+ap, 1n+bp)) : {Nat.mul(la, _) == Nat.mul(lb, 1n+ap) : Nat}
157      %Equal.sym(Nat, 1n+ap, Nat.mul(la, g), G.gcd_dvd_left(1n+ap, 1n+bp)) : {Nat.mul(la, Nat.mul(lb, g)) == Nat.mul(lb, _) : Nat}
158      swap_cw(la, lb, g)