def impl_mod

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

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

119def impl_mod(+a: WU.U64, +d: U32) -> {X.mod32(a, d) == mod32g(a, d, 65536, 65535) : U32}:
120  %Equal.sym(Nat, X.dig1(X.lo(a)), d1g(X.lo(a), 65536), dig1_eq(X.lo(a))) : {U32.from_nat(X.mod_step(X.mod_step(U32.to_nat(U32.mod(X.hi(a), d)), 65536n, _, U32.to_nat(d)), 65536n, X.dig2(X.lo(a)), U32.to_nat(d))) == mod32g(a, d, 65536, 65535) : U32}
121  {==}