def msmall

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

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

170def 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}:
171  +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))
172  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)))