def impl

bend-collections-laws-crypto@1.0.0.0 · proofs/math/u64/u64div.bend:102

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as U

102def impl(+a: U.U64, +d: U32) -> {U.div_small(a, d) == gdiv(a, d, 1048576, 4096, 256, 4095, 255) : U.U64}:
103  match a:
104    case U.U64{lo, hi}:
105      {==}