def cmp_limbs

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natcmp.bend:112

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

112def cmp_limbs(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +hx1: {C.fits(k, x1) == True{} : Bool}, +hx2: {C.fits(k, x2) == True{} : Bool}) -> {Nat.cmp(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) == lex(Nat.cmp(y1, y2), Nat.cmp(x1, x2)) : Cmp}:
113  cl_c(k, x1, y1, x2, y2, hx1, hx2, Nat.cmp(y1, y2), {==})