DivisionValue.actual: 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_value.bend as DivisionValue
Lines 70-72 of bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_value.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_value.bend&start_line=70&end_line=72

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

# Public native divisor identity is discharged here, with no external premise.
def actual(+n: Nat, word: Word(n)) -> {value(n, W.div_million(n, word), 1000000) == S.unsigned(n, word) : Nat}:
  conservation(n, word, 1000000, {==})

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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_value.bend&name=conservation
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_value.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=unsigned
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend&name=div_million