DivisionCandidate.digit: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate.bend as DivisionCandidate
Lines 27-30 of bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate.bend&start_line=27&end_line=30

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

# Link directly to the recurrence used by actual div_million. This equation is
# still modular; the reachable remainder range must be discharged separately.
def 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>}:
  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))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shl
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate.bend&name=multiplication_is_shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend&name=Division
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend&name=bit_u32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend&name=digit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend&name=digit_compare