def digit

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/division_candidate.bend:27

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W

27# Link directly to the recurrence used by actual div_million. This equation is
28# still modular; the reachable remainder range must be discharged separately.
29def digit(+p: Nat, +bit: Bool, +q: Word(p), +r: U32) -> {W.digit(p, bit, W.Div{q, r}) == W.digit_compare(p, q, U32.add(U32.shl(r), W.bit_u32(bit))) : W.Division<1n+p>}:
30  Equal.cong(U32, W.Division<1n+p>, x => W.digit_compare(p, q, U32.add(x, W.bit_u32(bit))), U32.mul(r, 2), U32.shl(r), multiplication_is_shift(r))