def t_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/combnat.bend:171

import Base
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/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend as GC
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend as LC

171# Euclid: wr | wl t and gcd(wl, wr) == 1 give wr | t
172def t_eq(+c: Nat, +jp: Nat, +t: Nat, +c1: Nat, +e: {Nat.mul(c1, 1n+jp) == Nat.mul(c, t) : Nat}) -> {t == Nat.mul(sq(c, jp, t, c1), wr(c, jp)) : Nat}:
173  +a = wl(c, jp)
174  +b = wr(c, jp)
175  +ea = Equal.trans(Nat, Nat.mul(t, a), Nat.mul(a, t), Nat.mul(c1, b), NA.mul_comm(t, a), cross(c, jp, t, c1, e))
176  +d = GC.dvd_gcd(Nat.mul(t, a), Nat.mul(t, b), b, c1, t, ea, {==})
177  +g1 = Equal.trans(Nat, M.gcd(Nat.mul(t, a), Nat.mul(t, b)), Nat.mul(t, M.gcd(a, b)), t, LC.gcd_mul_left(t, a, b), Equal.trans(Nat, Nat.mul(t, M.gcd(a, b)), Nat.mul(t, 1n), t, Equal.cong(Nat, Nat, z => Nat.mul(t, z), M.gcd(a, b), 1n, coprime(c, jp)), NA.mul_one(t)))
178  Equal.trans(Nat, t, M.gcd(Nat.mul(t, a), Nat.mul(t, b)), Nat.mul(sq(c, jp, t, c1), b), Equal.sym(Nat, M.gcd(Nat.mul(t, a), Nat.mul(t, b)), t, g1), d)