W64est.msmall: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64est.bend as W64est
Lines 170-172 of bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64est.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64est.bend&start_line=170&end_line=172

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

def msmall(+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.mod(hi, d) == hi : U32}:
  +e1 = Equal.trans(Nat, v(U32.mod(hi, d)), Nat.mod(v(hi), v(d)), Nat.mod(v(hi), 1n+bp), UD.mod_nat(hi, d, hd), Equal.cong(Nat, Nat, z => Nat.mod(v(hi), z), v(d), 1n+bp, hb))
  U3.injective(U32.mod(hi, d), hi, Equal.trans(Nat, v(U32.mod(hi, d)), Nat.mod(v(hi), 1n+bp), v(hi), e1, NR.mod_of(0n, bp, v(hi), hl)))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_zero
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mod
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend&name=injective
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend&name=mod_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=mod_of
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64est.bend&name=v