def fh

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

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

121def fh(+l: U32, +h: U32) -> {U32.is_lt(h, 65536) == Nat.is_lt(C.high(32n, v(WU.U64{l, h})), 65536n) : Bool}:
122  fh_c(l, h, 65536, {==}, 1n, {==})