def div_of
bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32div.bend:212
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend as U32div
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend as DQ
212def div_of(+a: U32, +b: U32, h: dm_type(a, b)) -> {v(U32.div(a, b)) == Nat.div(v(a), v(b)) : Nat}:
213 (e, lt) = h
214 %e : {v(U32.div(a, b)) == Nat.div(_, v(b)) : Nat}
215 Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(v(U32.div(a, b)), v(b)), v(U32.mod(a, b))), v(b)), v(U32.div(a, b)), DQ.identify(v(U32.div(a, b)), v(b), v(U32.mod(a, b)), lt))