def dsmall

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64est.bend:165

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U3
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD

165# a high word below the divisor: quotient 0, remainder itself
166def dsmall(+hi: U32, +d: U32, +hd: {U32.is_zero(d) == False{} : Bool}, +bp: Nat, +hb: {v(d) == 1n+bp : Nat}, +hl: {Nat.is_lt(v(hi), 1n+bp) == True{} : Bool}) -> {U32.div(hi, d) == 0 : U32}:
167  +e1 = Equal.trans(Nat, v(U32.div(hi, d)), Nat.div(v(hi), v(d)), Nat.div(v(hi), 1n+bp), UD.div_nat(hi, d, hd), Equal.cong(Nat, Nat, z => Nat.div(v(hi), z), v(d), 1n+bp, hb))
168  U3.injective(U32.div(hi, d), 0, Equal.trans(Nat, v(U32.div(hi, d)), Nat.div(v(hi), 1n+bp), 0n, e1, NR.div_of(0n, bp, v(hi), hl)))