def gg

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

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M

119# g = gcd(c, j), c == wl g, j == wr g for j = 1 + jp
120def gg(+c: Nat, +jp: Nat) -> Nat:
121  M.gcd(c, 1n+jp)