def lt_limbs

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/width.bend:305

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

305def lt_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}) -> {Bool.or(Nat.is_lt(y1, y2), Bool.and(Nat.is_eq(y1, y2), Nat.is_lt(x1, x2))) == Nat.is_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) : Bool}:
306  lt_limbs_c(k, x1, y1, x2, y2, hx1, hx2, Nat.is_lt(y1, y2), Nat.is_eq(y1, y2), {==}, {==})