def dm_l2

bend-collections-laws-crypto@1.0.0.0 · proofs/math/u64/u64div.bend:32

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend as UD

32def dm_l2(+a: U32, +b: U32, h: UD.dm_type(a, b)) -> {Nat.is_lt(UD.v(U32.mod(a, b)), UD.v(b)) == True{} : Bool}:
33  (e, l) = h
34  l