def dm_type

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32div.bend:209

import Base

209def dm_type(+a: U32, +b: U32) -> Type:
210  {Nat.add(Nat.mul(v(U32.div(a, b)), v(b)), v(U32.mod(a, b))) == v(a) : Nat} & {Nat.is_lt(v(U32.mod(a, b)), v(b)) == True{} : Bool}