def fl

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64bgcd.bend:131

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

131def fl(+l: U32, +h: U32) -> {U32.is_lt(65535, l) == Nat.is_lt(65535n, C.low(32n, v(WU.U64{l, h}))) : Bool}:
132  fl_c(l, h, 65535, {==}, 1n, {==})