def lt32

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix32.bend:196

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U3

196def lt32(+s: U32) -> {U32.is_lt(s, 32) == Nat.is_lt(vs(s), 32n) : Bool}:
197  U3.is_lt_nat(s, 32)