def cross

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

import Base
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/lcm.bend as LC

158# with c' (1 + jp) == c t: wl t == c' wr
159def cross(+c: Nat, +jp: Nat, +t: Nat, +c1: Nat, +e: {Nat.mul(c1, 1n+jp) == Nat.mul(c, t) : Nat}) -> {Nat.mul(wl(c, jp), t) == Nat.mul(c1, wr(c, jp)) : Nat}:
160  +g = gg(c, jp)
161  +a = wl(c, jp)
162  +b = wr(c, jp)
163  +l = Equal.trans(Nat, Nat.mul(Nat.mul(a, t), g), Nat.mul(a, Nat.mul(t, g)), Nat.mul(c, t), NA.mul_assoc(a, t, g), Equal.trans(Nat, Nat.mul(a, Nat.mul(t, g)), Nat.mul(a, Nat.mul(g, t)), Nat.mul(c, t), Equal.cong(Nat, Nat, z => Nat.mul(a, z), Nat.mul(t, g), Nat.mul(g, t), NA.mul_comm(t, g)), Equal.trans(Nat, Nat.mul(a, Nat.mul(g, t)), Nat.mul(Nat.mul(a, g), t), Nat.mul(c, t), Equal.sym(Nat, Nat.mul(Nat.mul(a, g), t), Nat.mul(a, Nat.mul(g, t)), NA.mul_assoc(a, g, t)), Equal.cong(Nat, Nat, z => Nat.mul(z, t), Nat.mul(a, g), c, Equal.sym(Nat, c, Nat.mul(a, g), e_c(c, jp))))))
164  +r = Equal.trans(Nat, Nat.mul(Nat.mul(c1, b), g), Nat.mul(c1, Nat.mul(b, g)), Nat.mul(c1, 1n+jp), NA.mul_assoc(c1, b, g), Equal.cong(Nat, Nat, z => Nat.mul(c1, z), Nat.mul(b, g), 1n+jp, Equal.sym(Nat, 1n+jp, Nat.mul(b, g), e_j(c, jp))))
165  LC.cancel_pos(Nat.mul(a, t), Nat.mul(c1, b), g, g_pos(c, jp), Equal.trans(Nat, Nat.mul(Nat.mul(a, t), g), Nat.mul(c, t), Nat.mul(Nat.mul(c1, b), g), l, Equal.sym(Nat, Nat.mul(Nat.mul(c1, b), g), Nat.mul(c, t), Equal.trans(Nat, Nat.mul(Nat.mul(c1, b), g), Nat.mul(c1, 1n+jp), Nat.mul(c, t), r, e))))