def prod_eq

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

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

183# (c / g) (t / (j / g)) == c'
184def prod_eq(+c: Nat, +jp: Nat, +t: Nat, +c1: Nat, +e: {Nat.mul(c1, 1n+jp) == Nat.mul(c, t) : Nat}) -> {Nat.mul(wl(c, jp), sq(c, jp, t, c1)) == c1 : Nat}:
185  +a = wl(c, jp)
186  +b = wr(c, jp)
187  +s = sq(c, jp, t, c1)
188  +h1 = Equal.trans(Nat, Nat.mul(Nat.mul(a, s), b), Nat.mul(a, Nat.mul(s, b)), Nat.mul(c1, b), NA.mul_assoc(a, s, b), Equal.trans(Nat, Nat.mul(a, Nat.mul(s, b)), Nat.mul(a, t), Nat.mul(c1, b), Equal.cong(Nat, Nat, z => Nat.mul(a, z), Nat.mul(s, b), t, Equal.sym(Nat, t, Nat.mul(s, b), t_eq(c, jp, t, c1, e))), cross(c, jp, t, c1, e)))
189  LC.cancel_pos(Nat.mul(a, s), c1, b, wr_pos(c, jp), h1)