def gcd_mul_pos

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
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

69def gcd_mul_pos(+cp: Nat, +a: Nat, +b: Nat) -> {M.gcd(Nat.mul(1n+cp, a), Nat.mul(1n+cp, b)) == Nat.mul(1n+cp, M.gcd(a, b)) : Nat}:
70  +c = {1n+cp : Nat}
71  +ca = Nat.mul(c, a)
72  +cb = Nat.mul(c, b)
73  +g = M.gcd(a, b)
74  +gc = M.gcd(ca, cb)
75  +la = G.wl(G.ws(b, a, b))
76  +lb = G.wr(G.ws(b, a, b))
77  # c g divides gc
78  +eu = G.dvd_gcd(ca, cb, Nat.mul(c, g), la, lb, scale_dvd(c, a, la, g, G.gcd_dvd_left(a, b)), scale_dvd(c, b, lb, g, G.gcd_dvd_right(a, b)))
79  # c divides gc: gc == h c
80  +eh = G.dvd_gcd(ca, cb, c, a, b, A.mul_comm(c, a), A.mul_comm(c, b))
81  +h = G.dw(cb, ca, cb, a, b)
82  # gc == h c divides c a and c b, so h divides a and b
83  +ma = G.wl(G.ws(cb, ca, cb))
84  +mb = G.wr(G.ws(cb, ca, cb))
85  +ea2 = unscale(cp, a, ma, h, Equal.trans(Nat, ca, Nat.mul(ma, gc), Nat.mul(ma, Nat.mul(h, c)), G.gcd_dvd_left(ca, cb), Equal.cong(Nat, Nat, z => Nat.mul(ma, z), gc, Nat.mul(h, c), eh)))
86  +eb2 = unscale(cp, b, mb, h, Equal.trans(Nat, cb, Nat.mul(mb, gc), Nat.mul(mb, Nat.mul(h, c)), G.gcd_dvd_right(ca, cb), Equal.cong(Nat, Nat, z => Nat.mul(mb, z), gc, Nat.mul(h, c), eh)))
87  # so h divides g: g == v h, and c g == v (h c) == v gc
88  +ev = G.dvd_gcd(a, b, h, ma, mb, ea2, eb2)
89  +v = G.dw(b, a, b, ma, mb)
90  +ecg = Equal.trans(Nat, Nat.mul(c, g), Nat.mul(v, Nat.mul(c, h)), Nat.mul(v, gc), scale_dvd(c, g, v, h, ev),
91    Equal.cong(Nat, Nat, z => Nat.mul(v, z), Nat.mul(c, h), gc, Equal.trans(Nat, Nat.mul(c, h), Nat.mul(h, c), gc, A.mul_comm(c, h), Equal.sym(Nat, gc, Nat.mul(h, c), eh))))
92  dvd_antisymm(gc, Nat.mul(c, g), G.dw(cb, ca, cb, la, lb), v, eu, ecg)