def actual

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/division_value.bend:70

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

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