def div_t

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend as LC

180def div_t(+c: Nat, +jp: Nat, +t: Nat, +c1: Nat, +e: {Nat.mul(c1, 1n+jp) == Nat.mul(c, t) : Nat}) -> {Nat.div(t, wr(c, jp)) == sq(c, jp, t, c1) : Nat}:
181  LC.div_exact(t, sq(c, jp, t, c1), wr(c, jp), wr_pos(c, jp), t_eq(c, jp, t, c1, e))