def mod_of
bend-collections-laws-math@1.0.0.0 · proofs/lib/u32div.bend:217
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as U32div
import Base
217def mod_of(+a: U32, +b: U32, h: dm_type(a, b)) -> {v(U32.mod(a, b)) == Nat.mod(v(a), v(b)) : Nat}:
218 (e, lt) = h
219 %e : {v(U32.mod(a, b)) == Nat.mod(_, v(b)) : Nat}
220 Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(v(U32.div(a, b)), v(b)), v(U32.mod(a, b))), v(b)), v(U32.mod(a, b)), mod_identify(v(U32.div(a, b)), v(b), v(U32.mod(a, b)), lt))