def lcm_dvd_pos

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend as G

201def lcm_dvd_pos(+ap: Nat, +bp: Nat, +m: Nat, +x: Nat, +y: Nat, +ex: {m == Nat.mul(x, 1n+ap) : Nat}, +ey: {m == Nat.mul(y, 1n+bp) : Nat}) -> {m == Nat.mul(lcm_dw(1n+ap, 1n+bp, m, x, y), M.lcm(1n+ap, 1n+bp)) : Nat}:
202  +a = {1n+ap : Nat}
203  +b = {1n+bp : Nat}
204  +g = M.gcd(a, b)
205  +l = M.lcm(a, b)
206  +ab = Nat.mul(a, b)
207  +t = lcm_dw(a, b, m, x, y)
208  +la = G.wl(G.ws(b, a, b))
209  +ea = Equal.trans(Nat, Nat.mul(m, a), Nat.mul(Nat.mul(y, b), a), Nat.mul(y, ab), Equal.cong(Nat, Nat, z => Nat.mul(z, a), m, Nat.mul(y, b), ey),
210    Equal.trans(Nat, Nat.mul(Nat.mul(y, b), a), Nat.mul(y, Nat.mul(b, a)), Nat.mul(y, ab), A.mul_assoc(y, b, a), Equal.cong(Nat, Nat, z => Nat.mul(y, z), Nat.mul(b, a), ab, A.mul_comm(b, a))))
211  +eb = Equal.trans(Nat, Nat.mul(m, b), Nat.mul(Nat.mul(x, a), b), Nat.mul(x, ab), Equal.cong(Nat, Nat, z => Nat.mul(z, b), m, Nat.mul(x, a), ex), A.mul_assoc(x, a, b))
212  +e2 = G.dvd_gcd(Nat.mul(m, a), Nat.mul(m, b), ab, y, x, ea, eb)
213  +e1 = gcd_mul_left(m, a, b)
214  +e3 = Equal.sym(Nat, Nat.mul(g, l), ab, gcd_mul_lcm(a, b))
215  +emg = Equal.trans(Nat, Nat.mul(m, g), M.gcd(Nat.mul(m, a), Nat.mul(m, b)), Nat.mul(t, Nat.mul(g, l)), Equal.sym(Nat, M.gcd(Nat.mul(m, a), Nat.mul(m, b)), Nat.mul(m, g), e1),
216    Equal.trans(Nat, M.gcd(Nat.mul(m, a), Nat.mul(m, b)), Nat.mul(t, ab), Nat.mul(t, Nat.mul(g, l)), e2, Equal.cong(Nat, Nat, z => Nat.mul(t, z), ab, Nat.mul(g, l), e3)))
217  +emg2 = Equal.trans(Nat, Nat.mul(m, g), Nat.mul(t, Nat.mul(g, l)), Nat.mul(Nat.mul(t, l), g), emg,
218    Equal.trans(Nat, Nat.mul(t, Nat.mul(g, l)), Nat.mul(t, Nat.mul(l, g)), Nat.mul(Nat.mul(t, l), g), Equal.cong(Nat, Nat, z => Nat.mul(t, z), Nat.mul(g, l), Nat.mul(l, g), A.mul_comm(g, l)), Equal.sym(Nat, Nat.mul(Nat.mul(t, l), g), Nat.mul(t, Nat.mul(l, g)), A.mul_assoc(t, l, g))))
219  cancel_pos(m, Nat.mul(t, l), g, gcd_pos(ap, la, g, G.gcd_dvd_left(a, b)), emg2)