def add_lt

bend-collections-laws-math@1.0.0.0 · proofs/math/u64/u64.bend:183

import Base

183# the low-limb wrap test is the low-limb carry
184def add_lt(+x: U32, +y: U32) -> {U32.is_lt(U32.add(x, y), x) == carry32(x, y) : Bool}:
185  add_lt1(1n, {==}, x, y)