def digit_compare
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as Wideimport Base
68def digit_compare(p: Nat, q: Word(p), +r: U32) -> Division<1n+p>:
69 digit_result(p, q, r, U32.is_ge(r, 1000000))
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as Wideimport Base
68def digit_compare(p: Nat, q: Word(p), +r: U32) -> Division<1n+p>:
69 digit_result(p, q, r, U32.is_ge(r, 1000000))