def internal_div_fin
bend-mathlib@0.8.1.0 · u32.bend:924
import bend-mathlib@0.8.1.0/u32.bend as U32
import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat
924def internal_div_fin(+b: U32, -a: Nat, hb: MNat.lt(0n, U32.to_nat(b)), qr: Word(32n) & U32, inv: internal_dm_inv(32n, U32.to_nat(b), a, qr)) -> {U32.to_nat(U32.div.fin(qr)) == Nat.div(a, U32.to_nat(b)) : Nat}:
925 match qr:
926 case (q, r):
927 match inv:
928 case (e, h):
929 internal_div_unique(Word.to_nat(32n, q), U32.to_nat(b), U32.to_nat(r), a, hb, e, h)