def sq

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend as GC

167# the quotient t / wr
168def sq(+c: Nat, +jp: Nat, +t: Nat, +c1: Nat) -> Nat:
169  GC.dw(Nat.mul(t, wr(c, jp)), Nat.mul(t, wl(c, jp)), Nat.mul(t, wr(c, jp)), c1, t)