Combnat.cross: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend as Combnat
Lines 158-165 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend&start_line=158&end_line=165

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

# with c' (1 + jp) == c t: wl t == c' wr
def 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}:
  +g = gg(c, jp)
  +a = wl(c, jp)
  +b = wr(c, jp)
  +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))))))
  +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))))
  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))))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend&name=cancel_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend&name=e_c
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend&name=e_j
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend&name=g_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend&name=gg
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend&name=wl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend&name=wr