def lt64

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix64.bend:172

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

172def lt64(+s: U32) -> {U32.is_lt(s, 64) == Nat.is_lt(vs(s), 64n) : Bool}:
173  U3.is_lt_nat(s, 64)