def impl_q

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64div.bend:179

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU

179def impl_q(+lo: U32, +hi: U32, +d: U32) -> {X.fst_q(X.div32(WU.U64{lo, hi}, d)) == div32q_g(lo, hi, d, 65536, 65535) : WU.U64}:
180  %Equal.sym(Nat, X.dig1(lo), d1g(lo, 65536), dig1_eq(lo)) : {X.fst_q(X.div32_t1(U32.div(hi, d), lo, X.dig_t(U32.to_nat(U32.mod(hi, d)), 65536n, _), U32.to_nat(d))) == div32q_g(lo, hi, d, 65536, 65535) : WU.U64}
181  {==}